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) aThe 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 xInstead of if…else statements Idris uses pattern matching. The logic goes:
- Define the function fizzBuzzSimple as a function which takes a natural number (non-negative integer) x and returns a String.
- Get the modulo of x with 3 and 5
- If both modulos are zero (x is divisible by 3 and 5) then return “fizzbuzz”
- If x is only divisible by 3, return “fizz”
- If x is only divisible by 5, return “buzz”
- 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.