Idris FizzBuzz Part III: Defining Types and Importing Modules
Tags: functional, idris
Published: 2023-05-16 15:05:24

---
series: "Idris FizzBuzz"
title: Idris FizzBuzz Part III: Defining Types and Importing Modules
published: true
date: 2023-05-10 00:00:00 UTC
tags: [ "functional", "idris" ]
canonical_url: https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-iii-types-and-importing-modules/
---


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](https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-i-monads-comments-assert-smaller/) and [Part II](https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-ii-maybes-infix-notation-idris-holes/), 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: 

```idris
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*
```idris
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*
```idris
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*
```idris
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. 

```idris
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. 

```idris
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*
```idris
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*
```idris
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 dependent types!