FizzBuzzing At The Type Level
It seems like the FizzBuzz meme has resurfaced, thanks to this reply to Raganwald’s post on the subject. Since I didn’t get on the bandwagon last time, I thought I’d take a crack at implementing with a bit of a twist: using the Haskell type system! This is my first moderately large type level program, so it’s probably not quite as elegant as it could be, but it does work and is fairly readable.
As you may know, the FizzBuzz task is to output a list of length 100 that contains a “fizz” whenever the associated index is divisible by 3, a “buzz” if it is divisible by 5, and the concatenation of the two if the index satisfies both of those conditions.
Let’s take a look at how we can build up a monstrous abuse of the GHC type system to implement this specification piece by piece. First, we need to turn on a crapload of options to make the compiler accept the twisted program we are going to give it:
Now, we need some notion of numbers in the type system so we can actually compute divisibility. The standard trick here is to use the Peano numerals, and since it’s quite a common need there are actually existing libraries for this: for instance, I could use Oleg’s amazing code that even does things like type level logarithm and factorial. However I want the example to be self contained so I will just implement the restricted arithmetic system that I need for FizzBuzz here:
That’s all very well, but we also need to be able to do operations on these numbers at the type level. To do this, we encode type level functions as type classes with associated instance declarations: one for each recursive case. We also mix is some magic pixie dust by using appropriate functional dependencies to make sure that we restrict the instance to be really functional, rather than relational.
Here’s an example of this, for the subtraction function:
This definition should not be too surprising to you if you’ve seen Peano arithmetic or Church numerals before: it’s pretty standard recursive style. However, the modulus function is rather more interesting:
Eeep! The essential trick here is to use a helper type class, ModIter, to loop repeatedly through the range from the modulus we are using down to 0, where on every iteration we subtract one from the thing we want to find the modular reduction of. When we can no longer decrement that number any further (i.e. it hits zero) we exit the loop. The result is just the modulus minus the current iteration number in the inner loop, which gives us exactly the remainder we need. To help you put this in the context of the definition above, the type variable a is the current number we want the modular reduction of, i is the inner loop index, b is the (constant) modular base and c is the eventual result.
Whew. Not too simple! That’s probably the most complicated bit of the program however, it’s easy going from here on out! First, let’s have some helper functions for computing various mod operations:
Now we get onto the actual business of FizzBuzz: we’re going to need yet more types. We start with some to represent the possible values in our output list:
Of course, there isn’t really any such thing is as a type level list yet! Let’s have one of those too:
Great. Now, we need to be able to work out the current fizzbuzziness of any particular index. This is pretty straightforward with the following definitions:
It’s all a bit tortured to ensure that we can prove to the compiler that the functional dependency on AnswerAt is respected, but it otherwise quite basic. We have a type class each for both fizziness and buzziness that, given the modular reduction of the index, outputs either the appropriate “noise” type if the mod is 0 (and hence we have divisibility) or the Boring type otherwise. These results are then laboriously munged together by the FizzBuzziness type class in the obvious way, and AnswerAt just serves to tie the knot between all of the components we have defined so far.
Lastly, we can generate the list of results using a trivial (!) type level for loop/map style of thing:
Now, the moment you’ve all been waiting for! Let’s actually get the answer to all our FizzBuzz woes!
Just load this puppy up in GHCi (this may take a while to compile!) and ask for the type of answer:
IT LIVES!
Come on, using 100 applications of S is not pretty. How about
In my opinion
instance (Sub b Z a) => ModIter Z Z b Z where
should be
instance ModIter Z Z b Z where
as for i=0 there is no subtraction required for concluding that (b-i) mod b = 0. This is also demonstrated by the fact that the subtraction result 'a' is never used in ModIter Z Z b Z.
FizzBuzz makes a nice example half way from trivial 'natural numbers in the type system' to complicated 'enforce balanced trees with the type system' problems. Thank you!
Get back to work/lectures/sleeping/getting pissed young man. Where will this functional obsession end? It will surely come to no good ;-)