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 aboutdivides
, 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 aNat
divisor and a Nat
dividend, returning a Bool
. This is written asNat -> 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 supportswitch
. In the Just
case, we get access to a value we've namedremainder
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.
Top comments (0)