Stupid Haskell Trick: Factorials in the Type System
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 Integers and Nats:
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 Nats, 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 :1:0: No instance for (Num Nat) arising from a use of `*' at :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 Nats an instance of the Num type class, but there is a simpler way: just define the necessary operations directly on Nats.
Let's start with addition of Nats:
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 Nats:
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 Nats:
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 Nats 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.