webbureaucrat

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.