Formally proving FizzBuzz for fun and profit, part 1.

FizzBuzz is a programming problem often used as a trivial coding interview challenge to filter out the programming job candidates who can’t program. It is defined as follows:

Write a program that prints the numbers from 1 to 100. But for multiples of three print “Fizz” instead of the number and for the multiples of five print “Buzz”. For numbers which are multiples of both three and five print “FizzBuzz”.

A quick and dirty solution in Python would look like this:

for i in range(1, 101):
     if i % 3 == 0 and i % 5 == 0:
         print("fizzbuzz")
     elif i % 3 == 0:
         print("fizz")
     elif i % 5 == 0:
         print("buzz")
     else:
         print(i)

But what if you don’t want the ‘quick and dirty’ solution?

What if you want the ‘ludicrously over-engineered‘ solution?

Then read on and perhaps learn how to prove your programs correct on the way.

Idris and Formal Proofs

Idris is a functional programming language with dependent types and a Haskell-like syntax. In Idris types are first-class constructs, you can treat them just like any other value. Among other things, this means that you can mix and match runtime values and types. For example, the type of a Vector in Idris includes in its definition the length of the Vector, which means you can define Vector concatenation like this:

vectConcat: Vect n a -> Vect m a -> Vect (n+m) a

The function vectConcat takes a Vector of length n and a Vector of length m and returns a Vector of length (n+m). If your implementation of the function can’t prove to the compiler that this is what happens, it won’t compile, no testing required. Because Idris lets you have arbitrary calculations in type definitions, the only limit on what runtime properties can be specified is programmer skill. For example:

  • A sort function which proves that the list contents are sorted
  • Functions where the number of parameters depends on the runtime value of the first one, e.g. a type safe printf.
  • Finite state machines where no invalid state transition is possible.
  • FizzBuzz

FizzBuzz in Idris

We’re going to build up our formally proven FizzBuzz step-by-step, starting with the Idris equivalent of the Python code above.

fizzBuzzSimple: (x: Nat) -> String
fizzBuzzSimple x with (modNat x (the Nat 3), modNat x (the Nat 5))
  | (Z, Z) = "fizzbuzz"
  | (Z, _) = "fizz"
  | (_, Z) = "buzz"
  | _ = show x

Instead of if…else statements Idris uses pattern matching. The logic goes:

  1. Define the function fizzBuzzSimple as a function which takes a natural number (non-negative integer) x and returns a String.
  2. Get the modulo of x with 3 and 5
  3. If both modulos are zero (x is divisible by 3 and 5) then return “fizzbuzz”
  4. If x is only divisible by 3, return “fizz”
  5. If x is only divisible by 5, return “buzz”
  6. Otherwise, convert x to a string then return it.

Partial and Total functions

This works (I hope) but has a few problems. The function will crash when x is 0, as modNat isn’t defined for 0. This makes the function partial, as it will crash on some inputs. A function which is guaranteed to return for any input is total. The Idris compiler is smart enough that it can normally tell if a function is total or not, it can’t do it all the time as that would mean solving the halting problem. Knowing that a program absolutely will not crash is obviously pretty good, (I’m looking at you Python). What totality won’t tell you is if the program does the right thing. For that you need to lean on the type system.

Engaging the type system

The next problem with our function is that it is stringly typed. As far as Idris can tell, all the return paths return the same thing, there’s nothing for the type system to hang onto. We’re merging the FizzBuzz logic with the code for presenting the output into one. Once everything has been converted into strings it is much harder to reason about what is happening, better to delay conversion to strings as late as possible.

Next Time…

In the next post, we’ll make Idris FizzBuzz v2.0, and start to really use the power of types.

Code Coverage Considered Harmful

Code coverage is a measure of what proportion of a code base is executed as part of test suite. At best it is useful tool for writing tests, but at worse it falls victim to Goodhart’s law and incentivises bad or useless tests just to get the number higher.

The Map Is Not The Territory

Code coverage is a very easy concept to explain and display to management. This makes it beguiling to use as metric for test quality and coverage, but just because code is executed by a test, that doesn’t mean the code is being tested. All that code coverage actually guarantees is the proportion of the code base which doesn’t crash the test runner, everything else isn’t captured by code coverage.

Code is only tested when the expected behaviour is checked against the actual behaviour. Just running code without checking what it actually does is almost useless, yet that is what code coverage measures.

Code coverage vs quality tests

When a measure becomes a target, it ceases to be a good measure.

Marilyn Strathern, ‘Improving Ratings’ Audit In The British University System

Above I explained why code coverage doesn’t tell you much about test quality, but it is worse than that, code coverage incentivises bad tests.

First off, what makes a good test? A good test:

  • Is tied directly to specific project requirements, preferably only one.
  • Tests as small a slice of the code base as possible, to make tracking down bugs easier.
  • Checks the actual behaviour of the code against expected behaviour, failing if they don’t match.

Code coverage encourages the exact opposite kind of tests. The bigger the bite of the code base each test takes, the faster code coverage goes up. In addition, code coverage doesn’t take into account actually testing code in a test, all it measures is if the code is run.

Obviously code coverage doesn’t prevent good tests from being written, but test engineers are almost human and if your performance is being measured in code coverage not test quality then the temptation is always there.

How to use code coverage, and what to use instead.

Despite all this, code coverage does have its uses. The important information from code coverage tools is exactly which parts of the code base are yet to be tested at all, not the overall percentage. Knowing what parts of the code base haven’t been touched by tests is useful for people writing tests.

As alternative to measuring test coverage, I propose tracking requirements coverage. That is, what percentage of the requirements have associated tests. This requirements coverage can then be combined with code coverage to reveal missing or implicit requirements and unnecessary code. Tracking requirements coverage isn’t a straightforward as code coverage but tagging each test with the associated requirement(s) would work.

Conclusions

  1. Never use code coverage as a measure of test quality
  2. Hide the actual percentage covered from anyone too pointy-haired to understand the limitations of what code coverage tells you.
  3. Instead of tracking code coverage, track requirements coverage.

Formally proving FizzBuzz for fun and profit, part 6.

Last time we made a function for determining which FizzBuzz variant is needed for a single number. Now we need calculate FizzBuzz for all the numbers between 1 and 100, then print them out.

Note, Idris uses monads to perform IO such as printing to stdout. If you don’t know what monads are, good luck. This will not be a monad tutorial, there are already too many bad ones out there, no need to add another. For our purposes all you need to know is that functions which return IO can do IO such as printing to the stdout and the do notation lets us sequence IO actions. For everything else monad, here is a good place to start

Who needs loops?

Idris doesn’t have for loops so we’re going to use recursion.

We’ll keep calling our fizzbuzz function with increasing numbers, starting from 1, until we get to 100.

fizzbuzz_loop: (n: Nat) -> (end: Nat) -> IO ()
fizzbuzz_loop n end = case n == end of
   True => pure ()
   False => do
     putStrLn $ show $ fizzbuzz n
     fizzbuzz_loop (S n) end

main: IO ()
main = fizzbuzz_loop 1 101

The pure function creates an empty IO action.

The end, no really

We now have a formally proven implementation of FizzBuzz. Hopefully if you’ve stuck with me to then you’ve learnt a few things about Idris and formal methods along the way. Strong, expressive type systems are the future.

The full source code can be found on github here. If you do attempt to make this version of FizzBuzz in an interview, comment below on how it went.

Formally proving FizzBuzz for fun and profit, part 5.

Last time we created a formally proven version of FizzBuzz, but it had some problems. Our proofs weren’t strong enough to prevent us making the version below, where anything divisible by five returns Buzz and everything else returns Normal.

wrongfizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
wrongfizzbuzz x = case (divisbleby3 x, divisbleby5 x) of
   (_,  Just buzz_prf) => Buzz buzz_prf
   (_, _) => Normal

The problem is that we create proofs that a number is divisible but not proofs that a number isn’t.

This is an important lesson. Just because you’ve proved something about your code, doesn’t mean you’ve proved what you need to. Proof types need to be crafted carefully so they actually prove what you think they do.

Proving a negative

Idris has a type to represent something which can’t exist, Void.

data Void : Type where

Void has no constructors, so it is impossible to create values of the type. If a function returns Void then one of its arguments must also be impossible to construct. In other words, if we can create a function which takes a single input and returns Void, then we have a proof that the input is impossible.

For FizzBuzz we want to be able to make proofs that a given number isn’t divisible by three or five. Something like:

DivisiblebyX 3 x -> Void
DivisiblebyX 5 x -> Void

Adding requirements for these negative proofs to our FizzBuzzProofSimple type gives:

data FizzBuzzProof: Nat -> Type where
   Fizz: DivisiblebyX 3 x -> (DivisiblebyX 5 x -> Void) -> FizzBuzzProof x
   Buzz: DivisiblebyX 5 x -> (DivisiblebyX 3 x -> Void) -> FizzBuzzProof x
   FizzBuzz: DivisiblebyX 3 x -> DivisiblebyX 5 x -> FizzBuzzProof x
   Normal: (x: Nat) -> (DivisiblebyX 3 x -> Void) ->(DivisiblebyX 5 x -> Void) -> FizzBuzzProof x

With the addition of these proofs it is impossible to use the wrong FizzBuzz variant for a number. Now we just need a way to make the proofs.

Will it divide?

We need to check each input number to see if it is divisible by three or five. Previously the divisibleby3 and divisibleby5 functions returned Nothing if the input didn’t divide, now we need to return a negative proof instead. Returning either a proof something is true or a proof it isn’t, is common enough pattern Idris provides the Dec wrapper type:

data Dec : Type -> Type where
  Yes : (prf: prop) -> Dec prop
  No : (contra : prop -> Void) -> Dec prop

Dec has a Yes and a No constructor, created with an instance of the wrapped type or a proof that the type is impossible to construct values of.

Adding these new features to our old divisibleby3 function gives:

divisibleby3: (y: Nat) -> Dec (DivisiblebyX 3 y)
divisibleby3 Z = No zeroNotDivisible3
divisibleby3 (S Z) = No oneNotDivisible3
divisibleby3 (S (S Z)) = No twoNotDivisible3
divisibleby3 (S (S (S Z))) = Yes Base
divisibleby3 (S (S (S (S y)))) = case divisibleby3 (S y) of
   Yes prf => Yes (Multiple prf)
   No notdiv => No (threeLessNotDivisible3 notdiv)

Instead of a catchall clause for numbers which aren’t divisible we now have separate clauses for when the input number is:

  • 0
  • 1
  • 2
  • 3
  • some number in the form (n+3)

Collectively these clauses cover all possible inputs (Idris will tell us if they don’t). If the input is divisible then the code is basically the same as before, each of the other clauses requires their own proof function.

Impossible

The proof functions for zero, one and two are almost identical and Idris will auto-generate most of the code.

zeroNotDivisible3 : DivisiblebyX 3 0 -> Void
zeroNotDivisible3 Base impossible
zeroNotDivisible3 (Multiple _) impossible

oneNotDivisible3 : DivisiblebyX 3 1 -> Void
oneNotDivisible3 Base impossible
oneNotDivisible3 (Multiple _) impossible

twoNotDivisible3 : DivisiblebyX 3 2 -> Void
twoNotDivisible3 Base impossible
twoNotDivisible3 (Multiple _) impossible

The function types are in the form for negative proofs we’ve seen above. To implement the function bodies we split the input argument into the two possible constructors, Base and Multiple. Idris can then determine that inputs of the required form are impossible.

For example, in zeroNotDivisible3 the input argument has to have the type DivisiblebyX 3 0. The Base constructor requires the two type arguments to be the same, which 3 and 0 aren’t. The Multiple constructor would require as an input an instance of DivisiblebyX 3 (0-3). Since natural numbers can’t be negative, this clause is also impossible.

threeLessNotDivisible3 is slightly different.

threeLessNotDivisible3 : (notdiv : DivisiblebyX 3 (S y) -> Void) -> DivisiblebyX 3 (3 + (S y)) -> Void
threeLessNotDivisible3 notdiv (Multiple x) = notdiv x

It is a proof that, given a non-zero number y is not divisible by three, y+3 is also not divisible by three. We split DivisiblebyX 3 (3 + (S y)) into the only applicable constructor, Multiple, which gives us a value of DivisiblebyX 3 (S y), calling notdiv with this value returns Void which completes the functions.

divisibleby5 is the same structure, with extra clauses for values of three and four.

A formally proven FizzBuzz (at last)

We now have functions for creating proofs that a number is or isn’t divisible by three or five. Plugging these functions into our fizzbuzz function gives:

fizzbuzz: (x: Nat) -> FizzBuzzProof x
fizzbuzz x = case (divisibleby3 x, divisibleby5 x) of
   (No not_fizz, No not_buzz) => Normal x not_fizz not_buzz
   (Yes fizz_prf, Yes buzz_prf) => FizzBuzz fizz_prf buzz_prf
   (No not_fizz, Yes buzz_prf) => Buzz buzz_prf not_fizz
   (Yes fizz_prf, No not_buzz) => Fizz fizz_prf not_buzz

Unlike our last attempt at FizzBuzz, there is now no way to return the wrong FizzBuzz variant.

The end?

We have a function for generating FizzBuzz for any single number, but FizzBuzz actually needs to be generated for all numbers between one and one hundred. Next time we’ll look at how to do this in Idris.

Formally proving FizzBuzz for fun and profit, part 4.

Last time we created the data type FizzBuzzProofSimple, which represents possible FizzBuzz values and created a few instances of it by hand. The next step is to write a function for generating FizzBuzzProofSimple instances from any number automatically.

Making Proofs

First we’re going to need functions to make DivisiblebyX instances. These functions need to:

  1. Take a natural number as an input
  2. If the number is divisible then return a proof that it is
  3. Else return nothing.

Before we get to defining these functions some groundwork.

Representing nothing

Not all numbers are divisible by three or five, so we won’t be able to generate DivisiblebyX instances for all inputs. The way to repesent something or nothing in Idris is with the Maybe type.

data Maybe : (a : Type) -> Type
    Nothing : Maybe a
    Just : (x : a) -> Maybe a

Maybe is a wrapper around any type and can either be Nothing or Just x where x is a value of the wrapped type. In our case, if the input number is divisible then we’ll return a DivisiblebyX wrapped in a Just, otherwise we’ll return Nothing.

Peano Numbers

To write our functions we’re going to need to work more closely with natural numbers. Previously we’ve used integer literals, but under the hood Idris has been converting these to Peano numbers, which are simple way of representing natural numbers.

data Peano = Z | S Peano

A Peano number is defined as either zero, Z, or the successor, n+1, of another Peano number, S n. So the number one is the successor to zero, S Z, two is the successor to one, S (S Z)), and so on.

In lots of places, Idris lets use integer literals in place of writing out the Peano number in full, but not everywhere.

But will it divide?

We’re now ready to make some proofs.

divisbleby3: (y: Nat) -> Maybe (DivisiblebyX 3 y)
divisbleby3  (S (S (S Z))) = Just Base
divisbleby3 (S (S (S x))) = case divisbleby3 x of
   Nothing => Nothing
   Just y => Just (Multiple y)
divisbleby3 _ = Nothing

Unsurprisingly the function to generate a DivisiblebX proof follows the same recursive pattern as the type definition. Let’s go through each clause:

  1. If the input is 3 (remember Peano numbers) then we can just use the Base variant of DivisiblebyX.
  2. If the input can be represented as 3 more than some number x, then recursively call divisbleby3 with x. If x is divisible by 3 then we can construct an instance DivisiblebyX for our original number using the proof for x we just calculated and the Multiple constructor. Otherwise our input isn’t divisible and we return Nothing.
  3. If none of the other function clauses matched, (Idris checks clauses from top to bottom), then we return Nothing.

divisibleby5 is almost identical:

divisbleby5: (y: Nat) -> Maybe (DivisiblebyX 5 y)
divisbleby5 (S (S (S (S (S Z))))) = Just(Base)
divisbleby5 (S (S (S (S (S x))))) = case divisbleby5 x of
   Nothing => Nothing
   Just y => Just (Multiple y)
divisbleby5 _ = Nothing

Putting it all together

We can now generate proofs of divisibility by 3 or 5 programmatically. So here is what you’ve been waiting for, a formally proven FizzBuzz.

fizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
fizzbuzz x = case (divisbleby3 x, divisbleby5 x) of
   (Nothing, Nothing) => Normal
   (Just fizz_prf, Just buzz_prf) => FizzBuzz fizz_prf buzz_prf
   (Nothing, Just buzz_prf) => Buzz buzz_prf
   (Just fizz_prf, Nothing) => Fizz fizz_prf

For the given number we attempt to generate proofs that it is divisible by three and five. If it isn’t divisible by either then we return Normal if it divides by three but not five we return Fizz etc.

Assuming we’ve defined DivisiblebyX correctly, there is no way to return Fizz, Buzz or FizzBuzz without knowing that the input number is divisible by what it is supposed to.

The last step is to update our Show interface from before.

Show (FizzBuzzProofSimple x) where
   show (Fizz x) = "fizz"
   show (Buzz x) = "buzz"
   show (FizzBuzz x y) = "fizzbuzz"
   show (Normal {x}) = show x

Nothing much has changed except for the Normal clause. The actual value that the type is wrapping is now part of the type instead of being associated with Normal directly. Idris let’s us pull the value in the type into a clause with curly brackets.

The end?

So we’ve got a formally proven version of FizzBuzz. If we implement it wrongly the compiler will tell us. Right? Not quite, the function below also compiles but definitely doesn’t do what we want. Next time we’ll look at fixing the escape hatch in our proof.

wrongfizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
wrongfizzbuzz x = case (divisbleby3 x, divisbleby5 x) of
   (_,  Just buzz_prf) => Buzz buzz_prf
   (_, _) => Normal

Formally proving FizzBuzz for fun and profit, part 3.

Last time we created a custom FizzBuzz data type and implemented the Show interface.

The problem with our previous code was that the compiler wasn’t enforcing any correctness, so today we’re going to do that.

Types are Proofs

Types are proofs, being able to create an instance of a type, tells you something about the value which has that type. This holds true even for basic type systems, a value with an Integer type tells you it isn’t a string. But Idris has a much more powerful type system.

Lots of languages have a concept of Generics, functions and data structures which are defined for arbitrary types. Idris takes this one step further and allows generics over runtime values.

data Divisibleby3 : Nat -> Type where
   Three: Divisibleby3 3
   ThreeMultiple: Divisibleby3 x -> Divisibleby3 (3+x)

Divisibleby3 is a data structure which is generic over a natural number. It has two constructors, ways of making an instance of the type, Three and ThreeMultiple.

The Three constructor says that an instance of Divisibleby3 can be constructed from the value 3. i.e. three is divisible by 3.

The ThreeMultiple says, if you already have an instance of Divisibleby3 for a number x, then you can construct an instance of Divisibleby3 for the value (x+3). i.e. every number divisible by 3, is 3 more than another number divisible by 3.

You may have noticed that this sounds alot like recursion. Three is the base case and ThreeMultiple effectively ‘calls’ Divisibleby3 recursively. This is a very common pattern for constructing proofs.

Let’s construct a few instances of Divisibleby3

divBy3: Divisibleby3 3
divBy3 = Three

divBy6: Divisibleby3 6
divBy6 = ThreeMultiple Three

divBy9: Divisibleby3 9
divBy9 = ThreeMultiple (ThreeMultiple Three)

divBy3 is straighforward, just a single use of the Three constructor. divBy6 starts with an instance of Three then passes that to ThreeMultiple to make a Divisibleby3 6 instance, and divBy9 continues the pattern.

It could get pretty tedious to write out divBy360, luckily Idris can do some of the leg work for you with its automated proof search feature.

If you can construct a instance of Divisibleby3 for a value you know it is divisible by 3. Instances of Divisibleby3 cannot be made for values not divisible by three using the two available constructors. As an example, let’s try to construct an instance of Divisibleby3 5.

divBy5: Divisibleby3 5
divBy5: ThreeMultiple (ThreeMultiple ?divByMinus3)

We can’t directly use the Three constructor (5 isn’t 3), so we start with ThreeMultiple but that requires an instance of Divisibleby3 (5-3), so we go add another ThreeMultiple and now we need a Divisibleby3 (-3) and since Divisibleby3 takes a positive number we’re stuck.

DivisibleByX

FizzBuzz requires checking divisibility by three and five. Instead of constructing a separate data type for dividing by five, we’re going to make a generic proof type for being divisible by any number.

data DivisiblebyX : Nat -> Nat -> Type where
   Base: DivisiblebyX x x
   Multiple: DivisiblebyX x y -> DivisiblebyX x (x+y)

DivisiblebyX has an identical structure to Divisibleby3 except now the type takes two numbers, the number to check divisiblilty against and the number we’re dividing.

As an example, proofs that 15 is divisible by 5 and 3 would look like:

divBy5_15: DivisiblebyX 5 15
divBy5_15 = Multiple (Multiple Base)

divBy3_15: DivisiblebyX 3 15
divBy3_15 = Multiple (Multiple (Multiple (Multiple Base)))

Proving FizzBuzz (finally)

We now have a way of proving that a given value is divisible by three and/or five. We can use these types to constrain which variants of our FizzBuzz return type can be returned for a given value.

data FizzBuzzProofSimple: Nat -> Type where
   Fizz: DivisiblebyX 3 x -> FizzBuzzProofSimple x
   Buzz: DivisiblebyX 5 x -> FizzBuzzProofSimple x
   FizzBuzz: DivisiblebyX 3 x -> DivisiblebyX 5 x -> FizzBuzzProofSimple x
   Normal: FizzBuzzProofSimple x

FizzBuzzProofSimple is a modification of FizzBuzzReturn from last time. Unlike FizzBuzzReturn, the Fizz, Buzz and FizzBuzz variants now need inputs in order to be instantiated.

To take the Fizz constructor as an example:

Fizz: DivisiblebyX 3 x -> FizzBuzzProofSimple x

If you want to construct a Fizz variant of FizzBuzzProofSimple x, then you need to have an instance of DivisiblebyX 3 x. The presence of x in both the input and output types ties them together.

There is now no way to return a Fizz, Buzz or FizzBuzz for a number without a proof that the number is divisible by everything it ought to be,

proof5: FizzBuzzProofSimple 5
proof5 = Buzz Base

proof3: FizzBuzzProofSimple 3
proof3 = Fizz Base

proof15: FizzBuzzProofSimple 15
proof15 = FizzBuzz (Multiple (Multiple (Multiple (Multiple Base)))) (Multiple (Multiple Base))

Next time, we’ll look at how to construct FizzBuzzProofSimple instances programmatically.

Formally proving FizzBuzz for fun and profit, part 2.

Last time we introduced FizzBuzz and the Idris language.

The problem with our last solution (shown below) was that it combined determining what the output should be with actually creating the output strings. This time we’ll be fixing this by add Algebraic Data types and Interfaces.

fizzBuzzSimple: (x: Nat) -> String
fizzBuzzSimple x with (modNat x (the Nat 3), modNat x (the Nat 5))
  | (Z, Z) = "fizzbuzz"
  | (Z, _) = "fizz"
  | (_, Z) = "buzz"
  | _ = show x

Algebraic Data Types

Algebraic data types are types composed of other types. Think structs and enums on steroids. We want the type system to differentiate between the different possible return types (fizz, buzz, fizzbuzz and normal numbers). We acheive this in Idris with:

data FizzBuzzReturn =
   Fizz
   | Buzz
   | FizzBuzz
   | Normal Nat

This defines a new data type FizzBuzzReturn, with four cases. The Fizz, Buzz and FizzBuzz cases are just tags with no associated data. As we don’t want to have to make a case for every single non FizzBuzz number there is a Normal case which also has a single natural number associated with it. Plugging this new data type into our previous function gives:

fizzBuzzReturn: (x: Nat) -> FizzBuzzReturn
fizzBuzzReturn x with (modNat x (the Nat 3), modNat x (the Nat 5))
   | (Z, Z) = FizzBuzz
   | (Z, _) = Fizz   
   | (_, Z) = Buzz
   | _ = Normal x

By converting the different return values into different return types we’ve made the FizzBuzz logic explicit in the type system. However we’ve also created a problem, FizzBuzz expects us to print out strings, not internal data types. For that we’ll need to convert FizzBuzzReturn to strings.

Interfaces

We could just write a function to convert FizzBuzzReturns to strings, but that’s not the ludicrously over-engineered way, so we’re going to use interfaces.

Interfaces are similar to type classes in Haskell or traits in Rust. Each interface is a collection of one or more overloadable functions. Instead of specifying concrete types, functions can specify that their inputs implement a given Interface. Any type which has an implementation of that interface can then be used. Examples of interfaces are:

  • Eq, which provides functions for comparing values for equality
  • Ord, for a standard way of comparing values.
  • Show, which is the interface we’ll be implementing.

The Show interface is the interface for converting data types to strings. It only has one function, show, defined as follows:

show : a -> String

The implementation of Show for FizzBuzzReturn is below, note the use of show for the number in normal (Show is already implemented for builtin types).

Show FizzBuzzReturn where
   show Fizz = "fizz"
   show Buzz = "buzz"
   show FizzBuzz = "fizzbuzz"
   show (Normal x) = show x

Implementing against interfaces instead of writing custom functions makes intent clear and allows easier reuse.

Putting it all together

We have successfully split the main and display logic, now to put them back together.

fizzBuzzReturnString: (x: Nat) -> String
fizzBuzzReturnString x = show(fizzBuzzReturn x)

Note how implementing the Show interface has given us a show function to use.

But does it work?

The code above (hopefully), implements FizzBuzz correctly, but we’re doing ludicrous over-engineering, “hopefully” won’t cut it. There’s nothing stopping the implementation of fizzBuzzReturn returning FizzBuzz for everything:

fizzBuzzReturn: (x: Nat) -> FizzBuzzReturn
fizzBuzzReturn x with (modNat x (the Nat 3), modNat x (the Nat 5))
  | (_, _) = FizzBuzz

The normal way to catch these kinds of bugs is by writing tests, but fizzBuzzReturn has literally infinite possible different inputs. We could write a handful of test and call it a day but that’s not the point of this series.

Next time we’ll look at making the Idris compiler do our testing for us, not just for a handful of inputs, but for all possible inputs.