Ahh, summer! A time for backyard barbeques, ice cold beer, baseball games, and
playing with experimental Haskell type system extensions. Or in my case, just
the latter. In this article I'll show you how to compute factorials using
Haskell's type system, *i.e.* at compile time.

Why would we want to do this? you may well ask. The real reason is "because
it's neat". This is a really beautiful construction; it took my breath away
when I figured it out. But another reason is that the techniques I'll
illustrate are useful in many other contexts. For instance, you can use
something like this to define a data type of a list which carries its length
around with it (so that *e.g.* taking the head of an empty list is a
compile-time error). This is very powerful; the more errors you can check at
compile-time, the better.

Nothing in this article is even remotely original. The direct inspiration for it came from a blog post by Brent Yorgey, which I've shamelessly stolen from and extended (thanks, Brent!). The indirect inspiration was from some comments on my previous blog post on Scala, which suggested that I look at a paper on embedding object-oriented programming in Haskell. That paper, called Haskell's Overlooked Object System, by Oleg Kiselyov and Ralf Lammel, is an amazing piece of work. In order to understand it fully, though, you first have to read another paper called Strongly Typed Heterogeneous Collections, by Oleg, Ralf and Keean Schupke. So that's what I did, and in the process learned quite a bit, which I'll use to good effect below. Both of these papers are strongly recommended if you're ready for them and if you enjoy having your mind blown.

To understand this article you need to know Haskell up to and including polymorphic types and (single parameter) type classes. I'll explain everything else as we go. If you want to run the examples you'll need the GHC Haskell compiler (Hugs may also work, but I haven't tried it). I used GHC version 6.12.1 to test this code.

## Step 1: Factorial using integers

Everybody knows that you can trivially define the factorial function on integers as follows:

```
factorial :: Integer -> Integer
factorial 0 = 1
factorial n = n * factorial (n - 1)
```

Let's test this using `ghci`

:

```
ghci> factorial 0
1
ghci> factorial 10
3628800
ghci> factorial 100
93326215443944152681699238856266700490715968264381621468592963895
21759999322991560894146397615651828625369792082722375825118521091
6864000000000000000000000000
```

OK, cool. I could easily generalize this to work on any argument whose type is
an instance of the `Num`

type class, but that won't be necessary in what
follows.

## Step 2: Factorial using natural numbers

One problem with the above definition is that it will go into an infinite loop
if the argument to `factorial`

is less than 0. You can always add an `error`

clause:

```
factorial :: Integer -> Integer
factorial n | n < 0 = error "invalid argument"
factorial 0 = 1
factorial n = n * factorial (n - 1)
```

but an alternative approach is to come up with a data definition for natural
numbers *i.e.* integers that cannot be less than zero. One way to do this is to
define naturals in terms of a zero value and a successor function. We can do
this as follows:

```
data Nat = Zero | Succ Nat
deriving (Show)
```

This states that a `Nat`

value is either `Zero`

or the successor (`Succ`

) of
another `Nat`

. The `deriving (Show)`

part is just to allow it to be printable
at the `ghci`

prompt. Let's test it:

```
ghci> Zero
Zero
ghci> Succ Zero
Succ Zero
ghci> Succ (Succ Zero)
Succ (Succ Zero)
```

Let's add some functions to convert back and forth between `Integer`

s and
`Nat`

s:

```
natToInteger :: Nat -> Integer
natToInteger Zero = 0
natToInteger (Succ n) = 1 + natToInteger n
integerToNat :: Integer -> Nat
integerToNat n | n < 0 = error "invalid argument"
integerToNat 0 = Zero
integerToNat n = Succ $ integerToNat (n - 1)
```

Now we can write:

```
ghci> natToInteger (Succ (Succ (Succ Zero)))
3
ghci> integerToNat 7
Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))
```

This encoding of natural numbers is called a "unary" encoding. As you can imagine, it's not terribly efficient, but it does work.

To define a factorial function in terms of `Nat`

s, we need to have `Nat`

equivalents of the integer functions used in the factorial definition. We can't
just re-use *e.g.* the `*`

operator:

```
ghci> Succ Zero * Succ Zero
<interactive>:1:0:
No instance for (Num Nat)
arising from a use of `*' at <interactive>:1:0-20
Possible fix: add an instance declaration for (Num Nat)
In the expression: Succ Zero * Succ Zero
In the definition of `it': it = Succ Zero * Succ Zero
```

As the error message states, we could fix this by making `Nat`

s an instance of
the `Num`

type class, but there is a simpler way: just define the necessary
operations directly on `Nat`

s.

Let's start with addition of `Nat`

s:

```
plus :: Nat -> Nat -> Nat
plus Zero n = n
plus (Succ m) n = Succ (plus m n)
```

The first clause states that adding `Zero`

to any `Nat`

`n`

gives back `n`

.
Let's see:

```
ghci> plus Zero (Succ (Succ Zero))
Succ (Succ Zero)
```

The second clause states that adding the successor of the `Nat`

`m`

to another
`Nat`

`n`

is equivalent to the successor of the sum of `m`

and `n`

. In other
words: `(m + 1) + n = 1 + (m + n)`

. Let's check:

```
ghci> plus (Succ (Succ Zero)) (Succ (Succ Zero))
Succ (Succ (Succ (Succ Zero)))
```

As George Orwell states:

Freedom is the freedom to say that two plus two make four. If that is granted, all else follows.

Nice to see that Haskell doesn't violate Orwell's prime directive. Also, since every recursive call (in the second clause) reduces the first argument by one, this function will always terminate.

From here, it's a simple matter to define multiplication on `Nat`

s:

```
mult :: Nat -> Nat -> Nat
mult Zero n = Zero
mult (Succ m) n = plus n (mult m n)
```

The first clause is obvious, and the second just says that `(m + 1) * n = n + (m * n)`

.

And with this, it's easy to define factorial on `Nat`

s:

```
fact :: Nat -> Nat
fact Zero = Succ Zero
fact (Succ n) = mult (Succ n) (fact n)
```

You should be able to figure out why this works. Let's check it:

```
ghci> fact Zero
Succ Zero
ghci> fact (Succ (Succ (Succ Zero)))
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))
```

We can use our `natToInteger`

and `integerToNat`

functions to test larger
numbers conveniently:

```
ghci> natToInteger $ fact $ integerToNat 8
40320
```

This just says that the factorial of 8 is 40320, which is the case.

This unary way of doing factorials is what we are going to compute using Haskell's type system. But first, I need to show you how to rewrite this in a new and (probably) unfamiliar way.

## Step 3: Rewriting into relational style

We normally write a function definition with the function name and arguments on the left-hand side and the result on the right-hand side. But we don't have to do it that way (at least not in theory; in Haskell we do have to write it that way). We could write it in "relational style" where the arguments and return values are treated the same syntactically. (The logic programming language Prolog uses a relational style, so if you hate this, you know what to avoid.) Let's go back to our original factorial function:

```
factorial :: Integer -> Integer
factorial 0 = 1
factorial n = n * factorial (n - 1)
```

In relational style, this would look something like this:

```
-- factorial in relational style
-- NOTE: This is not legal Haskell syntax!
factorialR :: Integer, Integer -- factorial relates two integers
factorialR 0 1 -- factorial of 0 is 1
factorialR n (n * r) -- factorial of n is n * r for some r
where factorialR (n - 1) r -- r is the factorial of (n - 1)
```

You would use this to compute a factorial as follows:

```
factorialR 10 n
```

and then `n`

would get bound to the correct result, which is `3628800`

.

This is critical; if you don't understand this, the rest of the article will be
incomprehensible. When using relational style you can't write inline function
calls; each "relational call" has to have its result bound to a specific name
(for instance, `r`

in the last line of `factorialR`

), and that name can be used
elsewhere (for instance, in the second-last line of `factorialR`

). Getting the
hang of writing functions in this style takes some practice.

We can also write out our functions on `Nat`

s in relational style. As I said
above, this is not Haskell syntax, though I hope it's clear what I'm trying to
do.

Addition:

```
-- functional style:
plus :: Nat -> Nat -> Nat
plus Zero n = n
plus (Succ m) n = Succ (plus m n)
-- relational style, not Haskell syntax:
plusR :: Nat, Nat, Nat -- plusR relates three natural numbers
plusR Zero n n -- 0 plus any n is n
plusR (Succ m) n (Succ r) -- (m + 1) + n is (r + 1)
where (plusR m n r) -- where r is m + n
```

Multiplication:

```
-- functional style:
mult :: Nat -> Nat -> Nat
mult Zero n = Zero
mult (Succ m) n = plus n (mult m n)
-- relational style, not Haskell syntax:
multR :: Nat, Nat, Nat -- multR relates three natural numbers
multR Zero n Zero -- 0 times any n is 0
multR (Succ m) n s -- (m + 1) * n is s
where plusR n r s -- where s is n + r
where multR m n r -- where r is m * n
```

Factorial:

```
-- functional style:
fact :: Nat -> Nat
fact Zero = Succ Zero
fact (Succ n) = mult (Succ n) (fact n)
-- relational style, not Haskell syntax:
factR :: Nat, Nat -- factR relates two natural numbers
factR Zero (Succ Zero) -- factorial of 0 is 1
factR (Succ n) s -- factorial of (n + 1) is s
where multR (Succ n) r s -- where s is (n + 1) * r
where factR n r -- where r is factorial of n
```

Well, that was a bit of a pain, but the good news is that if you've understood everything so far, the rest will be comparatively easy.

## Multi-parameter type classes

When encountering Haskell's type classes for the first time, you probably saw
what are called "single-parameter type classes". For instance, let's look at
the `Eq`

type class, which is used for data types which can support equality
comparisons:

```
class Eq a where
(==) :: a -> a -> Bool
(/=) :: a -> a -> Bool
```

Note the `a`

in `Eq a`

. This refers to the type for which equality is to be
defined. For instance, you might have:

```
instance Eq Integer where
-- Integer-specific definitions of == and /=
```

So here `Integer`

is the single parameter of the type class `Eq`

. If you think
about it, what `Eq`

does is specify that certain types are equality-comparable,
and any single-parameter type class separates the set of all types into two
groups: those which are instances of that type class and those which aren't.
You can also think of single-parameter type classes as defining a predicate on
types: those types which have instances of that type class are the ones
satisfying the predicate.

It seems logical that if there are single-parameter type classes, there might be
situations that call for multi-parameter type classes. For instance, a
hypothetical type class `Foo`

with two parameters might look like this:

```
class Foo a b where
-- some functions involving types a and b
```

To instantiate this, you would need to give two classes:

```
instance Foo Integer Integer where
-- some definition of Foo for Integers as types a and b
instance Foo Double Double where
-- some definition of Foo for Doubles
instance Foo Integer Double where ...
```

etc. You can think of `Foo`

(and other multi-parameter type classes) as
defining not predicates on types, but relations between types. This will become
important below.

## Step 4: Natural numbers at the type level

Let's say we want to define natural numbers at the type level. At the value level, we defined an algebraic data type:

```
data Nat = Zero | Succ Nat
```

What would the type equivalent of this be? We would need one type for each
value. So we have to have a type corresponding to `Zero`

and, for every
type-level natural number `N`

, then something like `Succ N`

would have to be a
type-level natural too. Let's do this.

First, defining a zero value at the type level is not hard. For instance, you could write something like this:

```
data Z = ZeroVal
```

`Z`

will be our type-level zero. It turns out that we won't care about the
value `ZeroVal`

of the type `Z`

at all, so the `ZeroVal`

constructor is
redundant (it'll never be used). That being the case, we can just write:

```
data Z
```

For this to work, we have to enable the `ghc`

extension `EmptyDataDecls`

, which
stands for "empty data declarations". The `data Z`

above is an empty data
declaration; it defines a type `Z`

which has no constructors. You might think
that this makes the type completely useless because it has no corresponding
values, but (a) a type doesn't have to have values in order to be useful, and
(b) there is one special value called `undefined`

which is a value of every
possible type. (In type theory, `undefined`

is called "bottom"). You can't use
`undefined`

for anything at the value level, because evaluating it sends Haskell
into an infinite loop, but you can use it for type hacking as we'll see.

You can actually see the `Z`

type in `ghci`

:

```
ghci> :t undefined :: Z
undefined :: Z :: Z
```

The compiler is telling you "`undefined`

, which you are telling me is of type
`Z`

, is computed to be of type `Z`

". Nice job, compiler! This may seem totally
useless, but it will end up being the way we can check our type-level
computations later on, and the results will not be trivial.

By the way, inside a Haskell source code file, here's how to specify the extension:

```
{-# LANGUAGE EmptyDataDecls #-}
```

This is normally placed at the top of the file. You can have multiple
extensions specified one after another *e.g.*

```
{-# LANGUAGE EmptyDataDecls,
MultiParamTypeClasses,
UndecidableInstances,
FlexibleInstances #-}
```

This is what I used to get the code in this article to work. The need for
`MultiParamTypeClasses`

should be obvious; the other two are more subtle and I'd
rather you just take it on faith for now.

We still haven't finished defining natural numbers at the type level. So far, all we have is a type-level version of zero:

```
data Z
```

What about the successor type? It's pretty easy too:

```
data S n
```

This is another empty data declaration, though here `S`

is a polymorphic type:
you need to give it a type `n`

for `S n`

to be a type. Another way to think
about this is that `S`

is like a function on types: it takes a type as an
argument and returns another type. I have to fight to keep myself from going
into a long digression on "kinds" here, but I will.

This means that the following are all going to be types:

```
Z -- type version of Zero (0)
S Z -- type version of (Succ Zero) (1)
S (S Z) -- type version of (Succ (Succ Zero)) (2)
S (S (S Z)) -- type version of (Succ (Succ (Succ Zero))) (3)
-- etc.
```

Cool! So with very little work, we have defined natural numbers at the type
level. We can ask `ghci`

to convert the `undefined`

value to our types:

```
ghci> :t undefined :: S (S (S Z))
undefined :: S (S (S Z)) :: S (S (S Z))
```

Once again, we haven't accomplished anything except verifying that `ghci`

does
indeed consider these type-level naturals to be valid types.

## Step 5: Addition at the type level

Okeedokee. Let's see if we can do some math on our type-level natural numbers.
It's natural to start with addition. Recall the definition of addition for our
`Nat`

type (natural numbers at the value level):

```
-- functional style:
plus :: Nat -> Nat -> Nat
plus Zero n = n
plus (Succ m) n = Succ (plus m n)
```

And let's not forget the relational version of this:

```
-- relational style, not Haskell syntax:
plusR :: Nat, Nat, Nat -- plusR relates three natural numbers
plusR Zero n n -- 0 plus any n is n
plusR (Succ m) n (Succ r) -- (m + 1) + n is (r + 1)
where (plusR m n r) -- where r is m + n
```

To do a computation on types, we are going to do something a bit weird. For every type-level operation we want to have, we will define a (multi-parameter) type class. This type class will contain one parameter for each type argument and one for the type result (in other words, it will be written in a relational manner; I told you this would turn out to be useful!). Here we will have:

```
class Plus m n r where
-- no methods!
```

As I said above, a multi-parameter type class defines a relation on types. A
function on types can be viewed as a relation on types (using the relational
style). But this is a very weird type class, since it has no methods! What use
could this have? All it does is assert that types `m`

, `n`

, and `r`

(whatever
they get instantiated to be) have some kind of relation that we're calling
`Plus`

. Conceptually, the type `r`

is the type-level sum of types `m`

and `n`

.
This is an empty class declaration, so you can leave out the `where`

:

```
class Plus m n r
-- no methods!
```

As we'll see in the next section, this is not quite adequate, but let's run with it for a while.

You can think of empty class definitions of this sort as defining the "type
signature" of our type-level addition function. To this, we have to add a
single instance declaration for every clause in the definition of `plus`

(or,
more accurately, `plusR`

). Let's translate the relational style `plusR`

to the
type level:

```
instance Plus Z n n
-- no method definitions!
```

This line says that adding the `Zero`

type to any type-level natural number `n`

just gives back `n`

. Notice that this defines an entire family of instances,
one for each type `n`

. This is the type level analog of:

```
-- functional style:
plus Zero n = n
-- relational style, not Haskell syntax:
plusR Zero n n
```

The next line is this:

```
instance (Plus m n r) => Plus (S m) n (S r)
-- no method definitions!
```

The context symbol `=>`

says that *if* the types `m`

, `n`

, and `r`

together are
an instance of the type class `Plus`

, *then* the types `S m`

, `n`

, and `S r`

together also are. So if Haskell is required to check that `Plus (S m) n (S r)`

is a valid instance for some `m`

and `n`

, all it has to do is check that ```
Plus m
n r
```

is a valid instance.

Compare this to:

```
-- functional style:
plus (Succ m) n = Succ (plus m n)
-- relational style, not Haskell syntax:
plusR (Succ m) n (Succ r) -- (m + 1) + n is (r + 1)
where (plusR m n r) -- where r is m + n
```

Notice that the instance declaration is an almost exact copy of the addition
function in relational style, modulo the syntax changes. Notice also that the
instance definitions have no method definitions, because there are no methods in
the `Plus`

type class.

You may feel like what we are doing is completely abusing the type class mechanism to do something it was never intended to do. Perhaps that's true, but a happier way to think about it is that we are showing that the type class mechanism has more uses than were previously suspected.

We are *almost* at a point where we can do addition at the type level, but there
is one crucial detail I have to cover first.

## Functional dependencies

If the type-level addition function is truly a relation on types that preserves the addition property, it should be possible to define things like:

```
instance Plus Z Z Z -- 0 + 0 = 0
instance Plus Z (S Z) (S Z) -- 0 + 1 = 1
instance Plus (S Z) Z (S Z) -- 1 + 0 = 1
instance Plus (S Z) (S Z) (S (S Z)) -- 1 + 1 = 2
-- etc.
```

All of these are derivable from the two instance equations for `Plus`

given
above. For instance:

```
instance Plus Z n n
-- let n = Z, so:
instance Plus Z Z Z
-- let n = (S Z), so:
instance Plus Z (S Z) (S Z)
instance (Plus m n r) => Plus (S m) n (S r)
-- let m = Z, n = Z:
instance (Plus Z Z r) => Plus (S Z) Z (S r)
-- from (instance Plus Z Z Z), we know that r can equal Z, so:
instance (Plus Z Z Z) => Plus (S Z) Z (S Z)
-- let m = Z, n = (S Z):
instance (Plus Z (S Z) r) => Plus (S Z) (S Z) (S r)
-- from (instance Plus Z (S Z) (S Z)), we know that r can equal (S Z), so:
instance (Plus Z (S Z) (S Z)) => Plus (S Z) (S Z) (S (S Z))
```

This is cool, but unfortunately, it's not sufficiently constrained. So far,
all we've shown is that all valid additions of natural numbers will have a
corresponding instance of the `Plus`

type class. We haven't shown that
*invalid* instances of the `Plus`

type class are *not* allowed. So far, there
is nothing preventing us from defining *e.g.*

```
instance Z Z (S (S (S Z))) -- 0 + 0 = 3 ???
```

For addition at the type level to mean anything, we must be able to forbid
instances of this kind. This leads us to the notion of a *functional
dependency*. We would like to say, in effect, that the third type parameter to
the `Plus`

type class is uniquely determined by the first two type parameters.
This makes sense, since we are trying to define `Plus`

as a type-level function,
and the crucial characteristic of a function is that the arguments (here, the
first two type parameters) uniquely determine the result (here, the last type
parameter). Haskell's type classes allow you to specify functional
dependencies. In this case, we change the class definition of `Plus`

to:

```
class Plus m n r | m n -> r
```

The functional dependency stuff is the `| m n -> r`

part. What this does is
tell the compiler "for any two specific types `m`

and `n`

, only allow one type
`r`

in instances of this class". This will solve the bogus instance problem.
Since the compiler already knows that there is an instance for `m = Z, n = Z`

(that being `instance Plus Z Z Z`

, derived from the rule `instance Plus Z n n`

),
it will not allow an instance like `instance Z Z (S (S (S Z)))`

. In effect, it
will say "Whoa there! You already have an instance for `m = Z, n = Z`

; you
can't have another!" And that's what functional dependencies do, and that's
*all* that they do. You can imagine that once you define the instance rules
above, all possible instances that conform to those rules are instantaneously
created, and so you can't add any more instances that violate the functional
dependency.

With this updated class definition, we can now do addition at the type level:

```
-- 1 + 1 = 2, type level:
ghci> :t undefined :: (Plus (S Z) (S Z) a) => a
undefined :: (Plus (S Z) (S Z) a) => a :: S (S Z)
-- 2 + 2 = 4, type level:
ghci> :t undefined :: (Plus (S (S Z)) (S (S Z)) a) => a
undefined :: (Plus (S (S Z)) (S (S Z)) a) => a :: S (S (S (S Z)))
```

The result in each case is the type of `a`

. Take that, George Orwell! ;-)

It's worth spending a bit of time going through what's happening here. Since we
don't care about values, and our type-level natural numbers don't have specific
values anyway, we are using the `undefined`

value as our only value (because it
can have any type whatsoever). When we type something like:

```
ghci> :t undefined :: (Plus (S Z) (S Z) a) => a
```

we are saying to `ghci`

: "What is the type of `undefined`

, given that I'm
telling you that its type is `a`

, where the three types `(S Z)`

, `(S Z)`

, and
`a`

together are a valid instance of the type class `Plus`

?" Or at least,
that's what `ghci`

thinks we're asking it. What we are really asking is: "Given
a type `a`

such that the three types `(S Z)`

, `(S Z)`

, and `a`

together are a
valid instance of the type class `Plus`

, what does the type `a`

have to be?"
This is a valid question, since the type `a`

must be uniquely determined by the
other two types due to the functional dependency; without the functional
dependency, there would be no way to compute a unique value for `a`

. Haskell
will then compute the type `a`

by applying the applicable rules until a unique
value for `a`

is derived; in this case, it will be the type `S (S Z)`

, which is
the type-level analog of the number 2.

Parenthetically, this reminds me a lot of a Sidney Harris cartoon where two people are looking on as a scientist has written on a large blackboard:

```
1
+ 1
-----
```

and is staring intently at the board. One onlooker says to the other: "He's
working on very, very, *very* basic research!" This is my all-time favorite
cartoon, and I've never been able to track it down in any of Harris' cartoon
collections; if anyone knows where I can find it please send me an email. I
guess I never realized that it wasn't a joke.

From here on, it's smooth sailing all the way.

## Step 6: Multiplication at the type level

Recall how we defined multiplication for (value-level) natural numbers:

```
-- functional style:
mult :: Nat -> Nat -> Nat
mult Zero n = Zero
mult (Succ m) n = plus n (mult m n)
-- relational style, not Haskell syntax:
multR :: Nat, Nat, Nat -- multR relates three natural numbers
multR Zero n Zero -- 0 times any n is 0
multR (Succ m) n s -- (m + 1) * n is s
where plusR n r s -- where s is n + r
where multR m n r -- where r is m * n
```

Multiplication on type-level naturals is essentially the same as the relational-style version:

```
class Mult m n r | m n -> r
-- No methods!
instance Mult Z n Z
instance (Mult m n r, Plus n r s) => Mult (S m) n s
```

Let's test it:

```
ghci> :t undefined :: (Mult (S (S Z)) (S (S (S Z))) a) => a
undefined :: (Mult (S (S Z)) (S (S (S Z))) a) => a
:: S (S (S (S (S (S Z)))))
```

We've just computed `2 * 3 = 6`

at the type level.

## Step 7: Factorial at the type level

Now for the *piece de resistance*. If you've understood everything so far, this
should be easy. Recall the versions for (value-level) natural numbers:

```
-- functional style:
fact :: Nat -> Nat
fact Zero = Succ Zero
fact (Succ n) = mult (Succ n) (fact n)
-- relational style, not Haskell syntax:
factR :: Nat, Nat -- factR relates two natural numbers
factR Zero (Succ Zero) -- factorial of 0 is 1
factR (Succ n) s -- factorial of (n + 1) is s
where multR (Succ n) r s -- where s is (n + 1) * r
where factR n r -- where r is factorial of n
```

Now look at the type-level factorial implementation:

```
class Fact n r | n -> r
-- No methods!
instance Fact Z (S Z)
instance (Fact n r, Mult (S n) r s) => Fact (S n) s
```

Note that the `Fact`

class has only two parameters (since factorial is a
function of one argument) and so the functional dependency specifies that the
result type `r`

depends on the argument type `n`

.

Let's test it:

```
ghci> :t undefined :: (Fact (S (S (S Z))) a) => a
undefined :: a :: (Fact (S (S (S Z))) a) => a :: S (S (S (S (S (S Z)))))
```

We've just shown that `factorial(3) = 6`

at the type level. But wait, why not
try this:

```
ghci> :t undefined :: (Fact (S (S (S (S (S (S Z)))))) a) => a
undefined :: (Fact (S (S (S (S (S (S Z)))))) a) => a
:: 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
(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
(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
(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
(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
(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
(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
(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))
```

This clearly shows that the factorial of 6 is 720. I hope you're satisfied.

## Wrapping up

This is a pretty cool construction, but one thing that really struck me while working on it is that it seemed very similar to what I understand is possible with C++ template metaprogramming. I'm no C++ guru, but I'm sure I've seen examples of factorials computed at compile-time in C++.

If you like this, I again urge you to read the papers by Ralf Lammel, Oleg Kiselyov, and Keann Schupke referred to above, and check out Brent Yorgey's excellent blog.