Some time ago, I published a post discussing how we solve the now-notorious FizzBuzz problem with computation in the type system. In the interests of flogging this horse well and truly to death, I’ve since adapted the code to make use of an upcoming GHC feature: type families. These are essentially a form of function at the type level: just what we need to make our FizzBuzz program a little more sane!

If you’re playing along at home, you’ll need a HEAD version of GHC and the following options pragma:

{-# OPTIONS_GHC -XEmptyDataDecls -XTypeOperators -XTypeFamilies -fallow-undecidable-instances
    -XMultiParamTypeClasses -XFunctionalDependencies #-}

As you can see, the extension doesn’t do anything to mitigate our “undecidability” problems. I’m also still making use of some type class extensions, but as we will see later that’s just necessary in one place, for quite an interesting reason.

Preliminaries are pretty much as before:

module Main where

data S a
data Z

data Negative

type Zero = Z
type One = S Z
type Three = S (S (S Z))
type Five = S (S (S (S (S Z))))
type OneHundred = (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S
                  (S (S (S (S (S (S (S (S (S (S Z)
                  )))))))))))))))))))))))))))))))))
                  )))))))))))))))))))))))))))))))))
                  )))))))))))))))))))))))))))))))))

Now, we reach our first type family: the subtraction function!

type family Sub a b
type instance Sub a Z = a
type instance Sub Z (S b) = Negative
type instance Sub (S a) (S b) = Sub a b

Woah, that’s it? Let’s remind ourselves of what it looked like last time:

class Sub a b c | a b -> c, c b -> a where
instance Sub a Z a where
instance (Sub a b c) => Sub (S a) (S b) c where

As you may guess, the function-ness of Sub is now enforced by the type families, rather than the functional dependencies. Apart from that it really just looks like I swapped some keywords around (and added a clause for negative numbers). However, the modulus finding code is a hell of a lot more readable:

type family Mod a b
-- Need -fallow-undecidable-instances for nested applications
type instance Mod a b = ModIter a b (Sub a b)

type family ModIter a b next
type instance ModIter a b Negative = a
type instance ModIter a b Z = Z
type instance ModIter a b (S next) = Mod (S next) b

In fact, it’s so readable it almost looks like a real programming language :-)! The rest of the translated code is similarly improved, though we still need to define distinct type functions if we want to do some sort of case split, which bulks out the program a bit:

type family IfZero test true false
type instance IfZero Z true false = true
type instance IfZero (S a) true false = false

data Boring
data Fizz
data Buzz
data FizzBuzz

type family FizzBuzziness fizz buzz
type instance FizzBuzziness Boring Boring = Boring
type instance FizzBuzziness Boring Buzz = Buzz
type instance FizzBuzziness Fizz Boring = Fizz
type instance FizzBuzziness Fizz Buzz = FizzBuzz

type family AnswerAt i
-- Need -fallow-undecidable-instances for nested applications
type instance AnswerAt i = FizzBuzziness (IfZero (Mod i Three) Fizz Boring) (IfZero (Mod i Five) Buzz Boring)

data Nil
data a :+: b

type family AnswerIter i
type instance AnswerIter Z = Nil
type instance AnswerIter (S a) = AnswerIter a :+: AnswerAt (S a)

Here’s where we come to a somewhat interesting issue. If you recall, when we wanted to actually compute the type-level answer last time we just wrote something like this:

tAnswerIter :: AnswerIter i a => i -> a
tAnswerIter = undefined

answer = tAnswerIter (undefined :: OneHundred)

In resolving the AnswerIter constraint the compiler was forced into evaluating our huge stack of type classes. You might expect that we could write something like this and then ask for it’s type in GHCi to get the same effect with type families:

answer = (undefined :: AnswerIter OneHundred)

Unfortunately (and entirely consistently, when you think about it) type families are lazily evaluated! This means that GHCi just tells us that answer has the type AnswerIter OneHundred: this is no help at all! In order to force evaluation of the function I had to define a “deep seq” style operation by dropping back into type classes:

answer = deepSeq (undefined :: AnswerIter OneHundred)

class DeeqSeq a b | a -> b where
    deepSeq :: a -> b

instance DeeqSeq Nil Nil where
    deepSeq = id

instance DeeqSeq (x :+: y) (x :+: y) where
    deepSeq = id

Now we get the expected result, just as before:

    
Prelude Main> :t answer
answer :: (…(Nil :+: Boring) :+: Boring) :+: Fizz) :+: Boring) :+: Buzz)
       :+: Fizz) :+: Boring) :+: Boring) :+: Fizz) :+: Buzz) :+: Boring)
       :+: Fizz) :+: Boring) :+: Boring) :+: FizzBuzz) :+: …)

IT LIVES! AGAIN!

I’ve yet to actually do anything useful with type families, but they seem like a powerful extension. Haskell users will be able to get their sweaty hands on them when the next release of GHC rolls around, which I’ve heard will be ICFP08 time.

Now, I promise not to write the word “FizzBuzz” again for at least three months ;-).