Idris FizzBuzz Part II: Maybes, Infix Notation, and Idris Holes
Tags: functional, idris
Published: 2023-05-11 14:37:34

---
series: "Idris FizzBuzz"
title: Idris FizzBuzz Part II: Maybes, Infix Notation, and Idris Holes
published: true
date: 2023-05-03 00:00:00 UTC
tags: ["functional", "idris"]
canonical_url: https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-ii-maybes-infix-notation-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](https://webbureaucrat.gitlab.io/articles/idris-fizzbuzz-part-i-monads-comments-assert-smaller/) 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_

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

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:

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

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

```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 => ?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_

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

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.