## DEV Community

webbureaucrat

Posted on • Originally published at webbureaucrat.gitlab.io on

# Idris FizzBuzz Part II: Maybes, Infix Notation, and Idris Holes

Let's conntinue on our journey of writing FizzBuzz in the Idris programming language. If you haven't already, I encourage you to read Part I for an introduction to the problem as well as some basic syntax, and, importantly, information on totality checking.

### Setting up the problem: calling `modulo`

In the previous post, we wrote a `modulo` function that takes two `Nat`numbers and returns a `Maybe` monad of the remainder. We defined it as follows:

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

Recall the reason why we needed this: because for FizzBuzz, we need to define whether or not a number is divisible by three, five, or both, so in this article, we will write a `divides` function that tells us just that by calling our `modulo` function.

Consistent with Idris's type-driven development, let's start by thinking about types. Whenever we call on a function that uses a `Maybe` monad, we have to decide: will we also return a monad, or will we handle the conditional internally to our new function?

For the purposes of FizzBuzz, I'm going to make a simplifying assumption about`divides`, which is that `divides` is defined where the divisor is zero, and the answer is just `False`. Mathematicians, feel free to get in my mentions, but I'm going to say that zero doesn't evenly divide anything because division isn't defined there at all.

### Type Signatures and Holes in Idris

Since I'm saying that `divides` is defined (as `False`) for zero (`Z`), this simplifies our type signature. The type signature for divides will be a`Nat` divisor and a `Nat` dividend, returning a `Bool`. This is written as`Nat -> Nat -> Bool`.

Let's start to write our function with an Idris `?hole`. Holes are an Idris feature I haven't mentioned yet, but they are useful in development. They're a feature of the syntax that serve as placeholders for logic that hasn't been written yet. This means that we can write:

``````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.
divides : Nat -> Nat -> Bool
divides divisor dividend = ?thisIsAHole
``````

...and it type checks. (Though, clearly, this isn't a total function.)

### Handling `Maybe`s with `case` / `of` syntax in Idris

We know we'll be calling our `modulo` function and getting back our `Maybe`monad. Then we need to determine whether or not our `Maybe` actually contains a value (`Just`) or whether it returned `Nothing`

We can handle union types like `Maybe` using a special Idris syntax using `case` and `of` keywords. Let's fill in a little with that syntax now.

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.
divides : Nat -> Nat -> Bool
divides divisor dividend =
case modulo dividend divisor of
Nothing => ?nothingCase
Just remainder => ?somethingCase
``````

Did you catch all that? We're calling `modulo` on `dividend` and `divisor`(sort of like `modulo(dividend, divisor)` in some other languages) and then wrapping that function call in `case` ... `of`. Then we see the possible cases listed below, sort of like a `switch` statement in languages that support`switch`. In the `Just` case, we get access to a value we've named`remainder` that we can access on the other side of the arrow.

### Infix notation in Idris

Idris allows functions to be called by infix notation, meaning we can put the function call after the first argument by using backticks.

A good example of such a function call is the `modulo` function. We could say, "modulo of dividend and divisor" but that's awkward. In a mathematics class, it would feel more natural to say "dividend modulo divisor." Let's rearrange our `modulo` call accordingly:

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.
total
divides : Nat -> Nat -> Bool
divides divisor dividend =
case dividend `modulo` divisor of
Nothing => ?nothingCase
Just remainder => ?somethingCase
``````

Most of the time, I'm not crazy about this syntax, but for arithmetic it does make sense.

### Replacing the last Idris holes

Both cases in our `case` expression should evaluate to our return type. Since we're saying that `divides` is `False` where `modulo` is not defined, we can say that the first case is `False`, and the second depends on whether or not the `remainder` is `0`.

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.
total
divides : Nat -> Nat -> Bool
divides divisor dividend =
case dividend `modulo` divisor of
Nothing => False
Just remainder => remainder == 0
``````

As you can see above, I also took the liberty of labeling this a `total`function because for all possible values of `divisor` and `dividend`, this program will terminate with an answer of `True` or `False` in finite time, and the compiler knows this.

### Wrapping up Maybe monads, infix notation, and holes

At this point, I'm starting to read and write Idris a little easier, and I hope you are, too. Hopefully, you're also starting to see the value constructs like monads, which are like succinct, generically-typed null-object design patterns that make sure you're accounting for potential missing data (without introducing "NullPointerExceptions" or some such horror). If you're struggling to follow, let me know! Again, my goal is to make Idris accessible to non-Haskellers. If you're still excited about total programming, get ready! In our next example, we're going to create our own FizzBuzz-specific type.