GHC 6.10.1 and above have a feature called type families. These are basically functions in the type system; they're even Turing complete.

You can run this blog post directly; save this text to a file ending in .lhs and run ghci -optL -q foo.lhs.

We need seven bucketfuls of language extensions to start off with.

> {-# LANGUAGE EmptyDataDecls       #-}
> {-# LANGUAGE TypeFamilies         #-} 
> {-# LANGUAGE TypeOperators        #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE ScopedTypeVariables  #-}
> {-# LANGUAGE FlexibleInstances    #-}

Now let's define the natural numbers.

> data Z   = Z
> data S n = S n
> 
> class             N n
> instance          N Z
> instance (N n) => N (S n)

Note that Z and S are separate types; in the type system, we couldn't distinguish the two if they were just constructors of the same type.

This is pretty bog standard stuff so far. Here's a polymorphic value, infer, that constructs a value appropriate to its type. So infer :: Z is Z, infer :: S Z is S Z, and so on.

> class        (N n) => Infer n     where infer :: n
> instance              Infer Z     where infer  = Z
> instance (Infer n) => Infer (S n) where infer  = S (infer::n)

Now we'll define a Show instance for our naturals. To do this, we need a function that turns a natural into a regular Haskell number.

> class                 (N n) => ToNum n     where toNum  :: (Num m) => n -> m
> instance                       ToNum Z     where toNum _ = 0
> instance (Infer n, ToNum n) => ToNum (S n) where toNum _ = 1 + toNum (infer::n)

Note that we use infer here instead of examining the actual value; we never look at the actual value because it doesn't matter.

Now we can define show using toNum. (Actually I broke this at some point, so it just makes show fail all the time with an overlapping instances error. Sorry. Patches welcome.)

> instance (ToNum n) => Show n where show n = "type " ++ show (toNum n)

Let's write our first type-level function: addition.

> type family   n   :+ m
> type instance Z   :+ m = m
> type instance S n :+ m = S (n :+ m)

Try infer :: S Z :+ S (S Z) in GHCi. Hopefully, you should get type 3 back. That was actually computed while type-checking!

Next we'll define subtraction and multiplication. The only interesting part is how we can simply omit the instance for Z :- m; a pattern matching failure in a type family translates to a type error.

> type family   n   :- m
> type instance n   :- Z   = n
> type instance S n :- S m = n :- m
> 
> type family   n   :* m
> type instance Z   :* m = Z
> type instance S n :* m = m :+ (n :* m)

And now, what you've all been waiting for: factorial and the Fibonacci sequence.

> type family   Fact n
> type instance Fact Z     = S Z
> type instance Fact (S n) = S n :* Fact n
> 
> type family   Fib n
> type instance Fib Z         = Z
> type instance Fib (S Z)     = S Z
> type instance Fib (S (S n)) = Fib (S n) :+ Fib n

You can now run infer :: Fib (Fact (S (S (S Z)))). If all goes well, GHCi will dutifully respond type 8. Congratulations, you've evaluated fib(3!) in the type system. Just like I promised.

For a final bit of fun, try this:

> foo :: (N n) => n -> Fact n -> ()
> foo _ _ = ()

foo (infer :: S (S (S Z))) takes a value of type Fact (S (S (S Z))), i.e. S (S (S (S (S (S Z))))), i.e. type-level 6, and returns (). It won't accept any other natural.

Cool, huh?