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

idris monadLet'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.

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