webbureaucrat

This 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 FizzBuzzNumbers, 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 exposed 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 exposeing 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.