webbureaucrat

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 Maybes 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.