## Idris FizzBuzz Part III: Defining Types and Importing Modules

idris variantThis is Part III of my attempt to explain how to use the Idris programming language through a tutorial on FizzBuzz, the common software development hiring interview problem. If you're new to Idris and haven't read Part I and Part II, I recommend doing that now. This article will go over defining our own types and importing our own modules as well as recap what we've learned about case-matching and basic syntax.

Just to recap, here's what we have so far:

`module Division`

||| Returns a `Just of the remainder of two numbers, or `Nothing` if the

||| divisor is zero.

total

modulo : Nat -> Nat -> Maybe Nat

modulo _ Z = Nothing --can't divide by zero, so Nothing

modulo Z _ = Just 0

modulo dividend divisor =

if dividend >= divisor

then modulo (assert_smaller dividend (minus dividend divisor)) divisor

else Just dividend

||| Returns `True` if the first number divides the second evenly, otherwise

||| returns `False`. Also returns `False` if the divisor is zero.

total

divides : Nat -> Nat -> Bool

divides divisor dividend =

case dividend `modulo` divisor of

Nothing => False

Just remainder => remainder == 0

We have completed our Divides module, which holds all of the basic arithmetic we need for our program, so now we get to work on FizzBuzz specific logic. Let's put that logic in a different module and call it FizzBuzz.

When we think about what we need for FizzBuzz, one of the first things we
should notice is that we're classifying numbers and specifying different
behavior based on their properties. In object orientation, we might define a
`Printable`

interface and have `Fizz`

`Buzz`

, `FizzBuzz`

and regular `Number`

implementations, but in Idris we can simply define a union type like so:

*src/FizzBuzz.idr*

`module FizzBuzz`

data FizzBuzzNumber = FizzBuzz | Fizz | Buzz | Number Nat

Note that `Number`

has a `Nat`

data member just like `Just`

had a `Nat`

data
member in our previous article.

This is a little terse, though. We can do better.

### Idris documentation comments in type definitions

Recall that a comment defined with three bars (`|||`

) is a documentation
comment in Idris, meaning it can show up in the Idris tooling and help the
user as well as the reader of the source. Let's fix this union type up with
documentation comments.

*src/FizzBuzz.idr*

`module FizzBuzz`

data FizzBuzzNumber = ||| Represents a number divisible by both 3 and 5.

FizzBuzz

| ||| Represents a number divisible by 3.

Fizz

| ||| Represents a number divisible by 5.

Buzz

| ||| Represents a number divisible by neither 3 nor 5.

Number Nat

### Importing modules in the Idris programming language

Next we need a way of getting from `Nat`

numbers to `FizzBuzzNumber`

s, which
means we need our `divides`

function from the previous post. To start, let's
export just the `divides`

function from the `Division`

module by decorating
the `divides`

function with the `export`

keyword.

*src/Division.idr*

`module Division`

||| Returns a `Just of the remainder of two numbers, or `Nothing` if the

||| divisor is zero.

total

modulo : Nat -> Nat -> Maybe Nat

modulo _ Z = Nothing --can't divide by zero, so Nothing

modulo Z _ = Just 0

modulo dividend divisor =

if dividend >= divisor

then modulo (assert_smaller dividend (minus dividend divisor)) divisor

else Just dividend

||| Returns `True` if the first number divides the second evenly, otherwise

||| returns `False`. Also returns `False` if the divisor is zero.

export total

divides : Nat -> Nat -> Bool

divides divisor dividend =

case dividend `modulo` divisor of

Nothing => False

Just remainder => remainder == 0

Now, we can go ahead and import the `Division`

module by using the `import`

keyword in the `FizzBuzz`

module.

`module FizzBuzz`

import Division --imports the `divides` function

data FizzBuzzNumber = ||| Represents a number divisible by both 3 and 5.

FizzBuzz

| ||| Represents a number divisible by 3.

Fizz

| ||| Represents a number divisible by 5.

Buzz

| ||| Represents a number divisible by neither 3 nor 5.

Number Nat

I went ahead and put in a comment explaining exactly what we're importing
because a peculiar thing about the Idris language is that, by default, Idris
exposes all `expose`

d modules.

(Frankly, I'm not crazy about that as a default, so a comment is a good practice.)

### Nested conditional logic in Idris

I admit I'm torn on using the infix notation from the previous article. I'm not crazy about filling up my code with a bunch of backticks, but for mathematical expressions where the English really lends itself to saying something like, "if 3 evenly divides n then..." I think infix makes sense.

`module FizzBuzz`

import Division --imports the `divides` function

data FizzBuzzNumber = ||| Represents a number divisible by both 3 and 5.

FizzBuzz

| ||| Represents a number divisible by 3.

Fizz

| ||| Represents a number divisible by 5.

Buzz

| ||| Represents a number divisible by neither 3 nor 5.

Number Nat

||| Given a number, returns a Fizzbuzz representation of the number depending

||| on whether it is divisible by three, five, or both, using the `divides`

||| function from the `Division` module.

total

classify : Nat -> FizzBuzzNumber

classify n =

if 15 `divides` n

then FizzBuzz

else if 3 `divides` n

then Fizz

else if 5 `divides` n then Buzz else Number n

Note again that we don't have to specify `Division.divides`

in our code, though
in most cases I think I would, anyway.

As you can see, nested conditionals in Idris work a lot like they do in other
languages, or more precisely, like the ternary (`?:`

) operators do in other
languages since both clauses evaluate to the return type.

### Converting a number to a `String`

type in Idris

Now we can pattern match on the type `FizzBuzzNumber`

as we have before.

*src/FizzBuzz.idr*

`module FizzBuzz`

import Division --imports the `divides` function

data FizzBuzzNumber = ||| Represents a number divisible by both 3 and 5.

FizzBuzz

| ||| Represents a number divisible by 3.

Fizz

| ||| Represents a number divisible by 5.

Buzz

| ||| Represents a number divisible by neither 3 nor 5.

Number Nat

||| Given a number, returns a Fizzbuzz representation of the number depending

||| on whether it is divisible by three, five, or both, using the `divides`

||| function from the `Division` module.

total

classify : Nat -> FizzBuzzNumber

classify n =

if 15 `divides` n

then FizzBuzz

else if 3 `divides` n

then Fizz

else if 5 `divides` n then Buzz else Number n

total

fbnToString : FizzBuzzNumber -> String

fbnToString FizzBuzz = "FizzBuzz"

fbnToString Fizz = "Fizz"

fbnToString Buzz = "Buzz"

fbnToString (Number n) = show n

As you can see, for most numbers, I'm using the `show`

function, which converts
a `Nat`

to a `String`

in Idris.

### Modular encapsulation in Idris

Clearly, we're pretty close to being able to use our `FizzBuzz`

module. It
would be great, though, if we we could hide the `FizzBuzzNumber`

type entirely
by `expose`

ing a function to convert a number to a FizzBuzz `String`

directly.

Let's do that now:

*src/FizzBuzz.idr*

`module FizzBuzz`

import Division --imports the `divides` function

data FizzBuzzNumber = ||| Represents a number divisible by both 3 and 5.

FizzBuzz

| ||| Represents a number divisible by 3.

Fizz

| ||| Represents a number divisible by 5.

Buzz

| ||| Represents a number divisible by neither 3 nor 5.

Number Nat

||| Given a number, returns a Fizzbuzz representation of the number depending

||| on whether it is divisible by three, five, or both, using the `divides`

||| function from the `Division` module.

total

classify : Nat -> FizzBuzzNumber

classify n =

if 15 `divides` n

then FizzBuzz

else if 3 `divides` n

then Fizz

else if 5 `divides` n then Buzz else Number n

||| Converts a `FizzBuzzNumber` value to a `String`.

total

fbnToString : FizzBuzzNumber -> String

fbnToString FizzBuzz = "FizzBuzz"

fbnToString Fizz = "Fizz"

fbnToString Buzz = "Buzz"

fbnToString (Number n) = show n

||| Converts a `Nat` to a `String` according to the standard requirements of

||| FizzBuzz, displaying "Fizz" if the number is divisible by 3, "Buzz" if the

||| number is divisible by 5, or "Fizzbuzz" if the number is divisible by both

||| 3 and five.

export total

numberToFBNString : Nat -> String

numberToFBNString n = fbnToString (classify n)

What we now have is effectively a small library that exports two functions:
`Division.divides`

and `FizzBuzz.numbertoFBNString`

. In the next article, we'll
set up a *.ipkg* package file and make the function available on our system.

### In conclusion

In this tutorial, I hope you've learned the basics of declaring a union type and how importing modules works in Idris. Let me know if there's anything I can make any clearer. In the next module, we'll be looking at setting up our main function and trying our hands at defining our own types!

*I write to learn, so I welcome your constructive criticism. Report issues on GitLab.
*