## Idris FizzBuzz Part I: Monads, Comments, and `assert_smaller`

idris
monad
totality
My journey of learning the Idris programming language continues! This article
will start a tutorial series detailing how to write FizzBuzz in Idris. As
before, my goal is to write without the assumption that all Idris learners
already know Haskell. We will start by implementing `modulo`

in Idris, and
toward that goal we will go painfully slow because frankly this stuff is hard.

For an overview of why I'm so excited about Idris as well as a little information on totality checking and some basic syntax, I recommend my previous article.

### An overview of the problem: FizzBuzz

If you're not familiar with FizzBuzz, it's the name of a common entry-level programming interview problem. The requirements go like this:

From one to 100 (or 1000 or so on), print each number, with a couple modifications:

- For every number evenly divisible by three, print "Fizz" instead of the number.
- For every number evenly divisible by five, print "Buzz" instead of the number.
- For every number evenly divisible by both three and five, print "FizzBuzz" instead of the number.

There are a couple reasons why this problem is so popular. The requirements are very simple and widely known, so they aren't likely to trip up a good candidate who made a small mistake. Even so, for such a simple problem, you're testing for:

- numeric range generation
- basic arithmetic
- conditional logic
- iteration

That's *just enough* to show you know the syntax of a language without having
to know the standard library off the top of your head. These are all good
reasons why I think it will be a good example from which to learn Idris. By
the end of this multi-part tutorial, we should know enough of the
Idris programming language to be productive or
know enough that the learning starts to come a little easier.

### Understanding modulus

In order to know if a number is easily divisible by three or five, we need to
be able to take the modulus of that number. Usually, this is pure syntax, the
`%`

operator, but Idris is a little more complicated.

I say that because there are a lot of numeric types in Idris, and for this
program, I think the most sensible one is `Nat`

, the set of natural numbers, or
the set of zero and the positive integers. I recommend reading the
documentation for `Nat`

before proceeding, though you don't have to fully understand it all.

So we will be implementing our own modulus that is defined for the natural
numbers, but there's a catch. Modulus isn't really defined for zero, so we need
a **monad**. You can think of a monad like a box. The box is an abstraction
around whether or not something inside it exists. Whether the box is empty or
full, it's still box-shaped, which makes it easy to work with when we're
expecting a value but might not have one.

In this case, we need a monad that either does or doesn't contain the result of
the `modulo`

function. Idris has a monad for such an occasion called a
`Maybe`

monad.
In most cases, we will get a `Just`

with a remainder inside. if the divisor
is zero, however, we will get a `Nothing`

. Either way, we'll be getting a
monad back, so we know we won't have to deal with errors, which is what makes
monads so appealing as a solution.

### Thinking about modulo

There are a number of ways we could set up `modulo`

. We could, for example,
compare the dividend with the product of the divisor and the integer quotient,
but (for reasons I won't get into) that's just not that appealing right now.
what I'm going to do instead is something like this:

*pseudocode*

`function modulo(dividend: Nat, divisor: Nat): Maybe<Nat>`

{

if (divisor == 0) { return new Nothing(); }

if (dividend == 0) { return new Just(0); }

while (dividend >= divisor)

{

dividend = dividend - divisor;

}

return new Just(dividend);

}

The idea here is to subtract off divisor as many times as I can, and whatever is left over is the remainder.

I'm including this code because the unusual, Haskell-like syntax can be intimidating for people who aren't used to it, and learning a whole new programming paradigm is plenty hard enough without an added language barrier.

### Setting up the problem

So we need a function `modulo`

that takes a dividend and a divisor and returns
the remainder. Recall from the "Hello world" example that Idris puts type
signatures on top and separates function parameters and the return type with
arrows. Then, on the next line, the definition begins.

*src/Division.idr*

`module Division`

modulo : Nat -> Nat -> Maybe Nat

modulo dividend divisor = Nothing

### Type signatures in Idris

Idris supports case matching in function definitions, meaning that we can
supply different definitions for different possible inputs. With `Nat`

numbers, that enables us to handle the zero case effectively by case-matching
it against the type `Z`

.

When the divisor is zero, it means it's safe to ignore the dividend because we
know the result will be `Nothing`

(because we can't divide by zero) so we can
use the `_`

to mean "ignore this parameter in this case."

With that, let's split up our function:

*src/Division.idr*

`module Division`

modulo : Nat -> Nat -> Maybe Nat

modulo _ Z = Nothing

modulo Z dividend = Nothing

modulo dividend divisor = Nothing

### Types of comments in Idris

Again, no shame if you're fighting with the sytax. In fact, let's take the
opportunity to put in some comments. Three bars (`|||`

) represent a
documentation comment which will show up in generated documentation or even
the IDE, while comments enclosed in `{-`

/ `-}`

or beginning with
`--`

are for the reader of the function itself.

*src/Division.idr*

`module Division`

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

||| divisor is zero.

modulo : Nat -> Nat -> Maybe Nat

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

modulo Z _ = Nothing --this case is a placeholder

modulo dividend divisor = Nothing --this case is a placeholder

{- What we have here is a type signature followed by three different cases. In

the first case, we throw away the dividend argument (_) and match on the

divisor when the divisor is zero and return `Nothing` because you can't

divide by zero. The second case matches on the divisor when the divisor is

zero. The last will catch all other cases.

-}

### Case matching in Idris

Cases match from top to bottom, so we can assume that in the second and third cases, the divisor is not zero because it will always match with the first case. Let's fill in the next case, which is also trivial because if the dividend is zero and the divisor is not, we can assume the remainder is zero.

Recall, though, that we can't just return zero. We are using `Maybe`

, so
we will wrap our result in a `Just`

.

*src/Division.idr*

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

||| divisor is zero.

modulo : Nat -> Nat -> Maybe Nat

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

modulo Z _ = Just 0 -- if the dividend is zero return zero wrapped in Just.

modulo dividend divisor = Nothing -- this is a placeholder

Now we're almost there with just one more case to cover. Just like our while loop in typescript-like pseudocode above, we will subtract until dividend is less than divisor. However, unlike the while loop above, we're writing functional code, so let's use recursion instead.

*src/Division.idr*

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

||| divisor is zero.

modulo : Nat -> Nat -> Maybe Nat

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

modulo Z _ = Just 0 -- if the dividend is zero return zero wrapped in Just.

modulo dividend divisor =

if dividend >= divisor

then modulo (minus dividend divisor) divisor

else Just dividend

Every time the dividend is greater than the divisor, subtract off the divisor again and try again, just like above. Make sense?

### Using `assert_smaller`

to help check totality in Idris

Now there's just one more matter to attend to: totality checking! (I always get so excited about this part!)

Unfortunately, if we check this for totality, we get an error.

`Error: modulo is not total, possibly not terminating due to recursive`

path Division.modulo -> Division.modulo

The key word here is "possibly." Actually, this is a total function, and we can prove it.

- The case where the divisor is zero is covered elsewhere, and therefore, the divisor is not zero.
- If we subtract a positive
`Nat`

from a larger positive`Nat`

, we get a smaller`Nat`

.

However, Idris is having some trouble seeing that in our code. Let's give it a
little help with `assert_smaller`

.

`assert_smaller`

takes two arguments and always returns the second, but it also
tells the compiler that the second argument is always going to be smaller than
the first. Since we're doing that subtraction, we can make that assertion
safely. Then we can add `total`

to the front of our function to tell
the compiler to check the totality of this function. Let's do that now.

*src/Division.idr*

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

modulo Z dividend = Just 0

modulo dividend divisor =

if dividend >= divisor

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

else Just dividend

This does exactly the same thing as the previous, but now we have totality. 🎉

### Wrapping up `modulo`

for natural numbers

In conclusion, I hope this has been helpful. I set out to try to explain Idris for non-Haskellers and guess what? It turns out it's really hard! And I know these tutorials alone won't be enough to teach someone everything they need to know about Idris, but it's my hope that having just a few more resources out there will make things just a little easier and pave the way for a few more resources until Idris is broadly accessible to learn.

Stay tuned! In the next tutorial, I plan to cover case matching monads and more.

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