# 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.

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.

``````  -- 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.

• #### Yet Another Monad Tutorial (part 8: more on state monads)

In the previous article, we learned what state monads were and how they worked. In this article we'll work through a complete (though very simple)…

• #### Yet Another Monad Tutorial (part 6: more on error-handling monads)

In the previous article we discussed error-handling strategies in Haskell and derived the Either e monad for structured error handling. In this…

• #### Error

Anonymous comments are disabled in this journal

default userpic