Welcome! We notice you're using an outdated browser, which will result in a degraded experience on this site. Please consider a modern, fully supported browser.

# webbureaucrat

The articles are just window-dressing for code snippets I want to keep.

## Idris FizzBuzz Part III: Defining 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 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.totalmodulo : Nat -> Nat -> Maybe Natmodulo _ Z = Nothing --can't divide by zero, so Nothingmodulo Z _ = Just 0modulo 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. totaldivides : Nat -> Nat -> Booldivides 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 FizzBuzzdata 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 FizzBuzzdata 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.totalmodulo : Nat -> Nat -> Maybe Natmodulo _ Z = Nothing --can't divide by zero, so Nothingmodulo Z _ = Just 0modulo 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 -> Booldivides 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 FizzBuzzimport Division --imports the `divides` functiondata 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 FizzBuzzimport Division --imports the `divides` functiondata 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.totalclassify : Nat -> FizzBuzzNumberclassify 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 FizzBuzzimport Division --imports the `divides` functiondata 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.totalclassify : Nat -> FizzBuzzNumberclassify n =   if 15 `divides` n   then FizzBuzz  else if 3 `divides` n        then Fizz        else if 5 `divides` n then Buzz else Number n totalfbnToString : FizzBuzzNumber -> StringfbnToString 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 FizzBuzzimport Division --imports the `divides` functiondata 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.totalclassify : Nat -> FizzBuzzNumberclassify 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`. totalfbnToString : FizzBuzzNumber -> StringfbnToString 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 totalnumberToFBNString : Nat -> StringnumberToFBNString 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.

← Home