Some lambda calculus examples

Syntax

In a previous blog entry I described a simple evaluator and type checker for the lambda cube, i.e., various forms of lambda calculus.

Here I'm going to show some examples of code in pure typed λ-calculus. All the examples are typable in F_ω; the full lambda cube is not necessary.

Before doing any examples we'd better have some syntax that is not too painful, because writing λ-expression in raw Haskell is tedious. The syntax for variables, * kind, and application is easy, I'll just use Haskell syntax. For λ-expressions the Haskell syntax doesn't allow explicit type annotations, but various Haskell compiler implement that extension, so I'll just pick that. So a λ will be written, "\ (var::type) -> expr". And as in Haskell I'll allow multiple variables between the "\" and "->"; it's just a shorthand for multiple lambdas.

So what about the dependent function type? The syntax (x:t)→u suggests (x::t)->u, so I'll use that. And when the variable doesn't occur we'll write t->u as usual. For type variables Haskell (well, not Haskell 98, but extensions) uses forall (a::*) . t, so I'll allow that too.

An example, the identity function:

\ (a::*) (x::a) -> x

with type

forall (a::*) . a->a

And using it

id Int 5

Writing a pretty printer and parser for this is pretty straight forward so I'll skip that and just point you to the code. BTW, instead of using Parsec for the parser like everyone else I used ReadP. The ReadP library is very nice, partly because the alternative operator is actually commutative (unlike Parsec). But the error messages suck.

Enter let

Now if we want to use, say, the identity function more than once we need to name it. There is a mechanism for that, namely λ. But it looks awkward. Look:

(\ (id :: forall (a::*) . a->a) -> ... id ... id ... id ...) (\ (a::*) (x::a) -> x)

What makes it awkward is that the name, id, is far away from the body, \ (a::*) (x::a) -> x. From Haskell we are more used the let and where expressions. So let's add that let. Instead of what we have above we'll write

let id :: forall (a::*) . a->a = \ (a::*) (x::a) -> x
in  ... id ... id ... id ...

The let construct could be just be syntactic suger for a lambda and an application, but I've decided to add it as a constructor to the expression type instead.

    | Let Sym Type Expr Expr

Adding a new constructor means that we have to modify all the functions operating on Expr, and it's extra much work because Let is a variable binding construct. For substitution we just cheat a little and use the expansion into an application and λ

    sub (Let i t e b) = let App (Lam i' t' b') e' = sub (App (Lam i t b) e)
                        in  Let i' t' e' b'

And for normal form we use the same trick.

    spine (Let i t e b) as = spine (App (Lam i t b) e) as

And for now, let's extend the type checker in the same way.

To make definitions a little less verbose I'll allow multiple bindings. E.g.

let x :: Int = g a; y :: Int = f x in h x y

It's just multiple nested Lets in the obvious way. Another shorthand. I'll allow the identity function to be written

let id (a::*) (x::a) :: a = x
in ...

The translation is pretty easy

let f (x1::t1) ... (xn::tn) :: t = b in e

is

let f :: forall (x1::t1) ... (xn::tn) . t = \ (x1::t1) ... (xn::tn) -> b in e

And finally, to make it even more like Haskell, I'll allow the type signature to be on a line of its own, omitting types on the bound variables.

let id :: forall (a::*) . a -> a;
    id a x = x;
in  ...

It's pretty easy to translate to the bare expression type. Why all these little syntactic extras? Well, remember Mary Poppins "A spoonful of sugar makes the medicine go down." Phew! Enough syntax, on to the examples.

Bool

We could start by throwing in all kinds of primitive types into our little language, but who knows what might happen then. All the nice properties that have been shown about the language might not hold anymore. So instead we'll code all the types we need with what we already have.

The Bool type has two values: False and True. So we need to find a type that has exactly two different values. Fortunately that's easy: a->a->a (I'll be a bit sloppy and leave off top level quantifier sometimes, just like Haskell; That should be forall (a::*) . a->a->a).

Why does that have two possible values? Well, we have a function type that must return an a for any possible a that it's given, so it can't conjure up the return value out of thin air. It has to return one of it's arguments. And there are two arguments to choose from, so there are two different values in that type. Here's Bool, False, True:

Bool :: *;
Bool = forall (a::*) . a->a->a;

False :: Bool;
False = \ (a::*) (x::a) (y::a) -> x;

True  :: Bool;
True = \ (a::*) (x::a) (y::a) -> y;

If the definition for Bool was written in Haskell it would be

type Bool = forall a . a->a->a

false :: Bool
false = \ x y -> x

true :: Bool
true = \ x y -> y

It would be easy to add more sugar and allow type which just means you're defining something of type *. And you could also make an omitted type in a forall mean type *. But I've not added these little extras.

Defining the if function is trivial; it's just a matter of permuting the arguments a little, because the boolean values come with the "if" built in.

if :: forall (a::*) . Bool -> a -> a -> a;
if a b t f = b a t f;

Note how the type signature is exactly the same as you'd find in Haskell. A difference is that we have explicit type abstraction and type application. For instance, if takes a first argument that is the type of the branches. So when using if we must pass in a type.

Given this we can try to type check some simple code:

let Bool :: *;
    Bool = forall (a::*) . a->a->a;
    False :: Bool;
    False = \ (a::*) (x::a) (y::a) -> x;
in  False

Here is what happens:

*CubeExpr> typeCheck $ read "let Bool :: *; Bool = forall (a::*) . a->a->a; False :: Bool;False = \\ (a::*) (x::a) (y::a) -> x; in False"
*** Exception: Type error:
Bad function argument type:
Function: \ (False :: Bool) -> False
argument: \ (a :: *) (x :: a) (y :: a) -> x
expected type: Bool
     got type: forall (a :: *) . a->a->a

What is it whining about? Expected Bool, got forall (a :: *) . a->a->a. But it says right there in the code that Bool is exactly that. What's going on?
Well, the type checker knows the type of everything, but not the value of anything. So the type checker knows that type of Bool is *, but it doesn't know what it is equal to.

The problem is that when we have a let binding we know the value of the defined variable and to be able to do dependent type checking the type checker needs to know it too. We need to change the type checking of let. Here's a simple solution:

tCheck r (Let s t a e) = do
    tCheck r t
    ta <- tCheck r a
    when (not (betaEq ta t)) $ throwError $ "Bad let def\n" ++ show (ta, t)
    te <- tCheck r (subst s a e)
    tCheck r (Pi s t te)
    return te

Note how we substitute the value of the definition (a) in the body before type checking it. This is a sledge hammer approach. A better one would be to change the environment in the type checker to carry values when they are known. These values could then be used when computing the normal form of an expression. But let's keep it simple for now.

Let's try again:

*CubeExpr> typeCheck' $ read "let Bool :: *; Bool = forall (a::*) . a->a->a; False :: Bool;False = \\ (a::*) (x::a) (y::a) -> x; in False"
forall (a :: *) . a->a->a

That worked!

A simple top level

To make experimentation easier I've added a simple top level where you can evaluate expression, make definitions, load files, etc. The files are just a bunch of definitions the way they would go inside a let.

Sample session:

Welcome to the Cube.
Use :help to get help.
Cube> \ (a::*) (x::a) -> x
\ (a :: *) (x :: a) -> x
  ::
forall (a :: *) . a->a
Cube> 

When evaluating an expression it will first print the value, then ::, and finally the type.
Let's try some more. Here's the file bool.cube.

-- The Bool type.

Bool :: *;
Bool = forall (boolT::*) . boolT->boolT->boolT;

False :: Bool;
False = \ (boolT::*) (false::boolT) (true::boolT) -> false;

True  :: Bool;
True = \ (boolT::*) (false::boolT) (true::boolT) -> true;

if :: forall (a::*) . Bool -> a -> a -> a;
if a b t f = b a f t;

not :: Bool -> Bool;
not b = if Bool b False True;

and :: Bool -> Bool -> Bool;
and x y = if Bool x y False;

or :: Bool -> Bool -> Bool;
or x y = if Bool x True y;

Note how I've named some of the type variables with more suggestive names. More about that in a moment.

Cube> :load bool.cube
Cube> True
\ (boolT :: *) (false :: boolT) (true :: boolT) -> true
  ::
forall (boolT :: *) . boolT->boolT->boolT
Cube> and True False
\ (boolT :: *) (false :: boolT) (true :: boolT) -> false
  ::
forall (boolT :: *) . boolT->boolT->boolT

By staring carefully at these you can convince yourself that it's right. What's making it a little hard to read are all those leading lambdas (and the corresponding function types). But there's an option to suppress the printing of them.

Cube> :skip
Cube> True
true
  ::
boolT
Cube> and True False
false
  ::
boolT

Look, it got deceptively readable.

Characters

So we can define booleans. What about something like characters? You can define those too. What is the ASCII type? It's a type with 128 different values. We saw how we can make a type with two values (Bool); we can do the same for 128. Since that takes a lot of room, I'll do it for just four values.

Char :: *;
Char = forall (charT::*) . charT->charT->charT->charT->charT;

'a' :: Char;
'a' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'a';
'b' :: Char;
'b' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'b';
'c' :: Char;
'c' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'c';
'd' :: Char;
'd' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'d';

eqChar :: Char -> Char -> Bool;
eqChar x y = x Bool (y Bool True False False False)
                    (y Bool False True False False)
                    (y Bool False False True False)
                    (y Bool False False False True);

Since single quotes are allowed in identifiers in my little language the 'a' is just an identifier as usual. Some sample use:

Cube> :load char.cube
Cube> 'a'
_'a'
  ::
charT
Cube> eqChar 'a' 'a'
true
  ::
boolT
Cube> eqChar 'a' 'b'
false
  ::
boolT

A different way to use characters is just to assume that there is some character type and that is has some values. How can we do that? By using a lambda expression.

\ (Char :: *) -> \ ('a' :: Char) ('b' :: Char) ... -> ...

One final little syntactic sugar is to allow lambda expressions to be written with let. So

let x :: T;
in  e

is the same as

\ (x :: T) -> e

So for Char we can write

Char :: *;
'a' :: Char;
'b' :: Char;
'c' :: Char;
'd' :: Char;
eqChar :: Char -> Char -> Bool;

This is a very handy notation during program development, btw. Inside i let you can first just write the type of something and then use it freely. This something will then be lambda abstracted until such a time that you provide the definition.

Let's try the "fake" characters.

Cube> :load extchar.cube
Cube> 'a'
'a'
  ::
Char
Cube> :skip
Cube> 'a'
\ (Char :: *) ('a' :: Char) ('b' :: Char) ('c' :: Char) ('d' :: Char)
  (eqChar :: Char->Char->forall (boolT :: *) . boolT->boolT->boolT)
  -> 'a'
  ::
forall (Char :: *) .
       Char->Char->Char->Char->
       (Char->Char->forall (boolT :: *) . boolT->boolT->boolT)->
       Char
Cube> :skip
Cube> eqChar 'a' 'b'
eqChar 'a' 'b'
  ::
forall (boolT :: *) . boolT->boolT->boolT

Now eqChar no longer gets evaluated, naturally, because it has no definition; it's λ bound.

Now we know how the Char type could be implemented (or supplied from the outside). It would then be all right to add it as a primitive (with the same behavior), because it will not ruin any properties. (Speaking of ruining properties, the seq function in Haskell is an example of a function that cannot be defined in the λ-calculus. And sure enough, adding it to Haskell ruined the validity of η-reduction.)

It's not difficult to extend the Expr type with some Prim constructor for primitive functions, and adding some special cases in the syntax and type checking for them. But since this is not intended to be a usable language I'll resist the temptation (for now).

Pairs

OK, booleans and characters were pretty easy. Let's do pairs next. The Pair type is parameterized over two types; the type of the first and the second component. As with booleans the representation of pairs come with the case analysis "build in". (Case analysis on pairs is flip uncurry in Haskell.) If we can correctly implement building pairs, fst, and snd we are done.

Pair :: * -> * -> *;
Pair a b = forall (pairT::*) . (a->b->pairT) -> pairT;

PairC :: forall (a::*) (b::*) . a -> b -> Pair a b;
PairC a b x y = \ (pairT::*) (pair :: a->b->pairT) -> pair x y;

fst :: forall (a::*) (b::*) . Pair a b -> a;
fst a b p = p a (\ (x::a) (y::b) -> x);

snd :: forall (a::*) (b::*) . Pair a b -> b;
snd a b p = p b (\ (x::a) (y::b) -> y);

So the type is called Pair and the constructor PairC. Since they live in the same name space we can't use Haskell's convention of giving them the same name (which is (,) in Haskell.).

Again, in Haskell the first definition would be

type Pair a b = forall pairT . (a->b->pairT) -> pairT

Staring at these definitions makes it obvious(?) that they work. But we can test it too.

Cube> :let S :: *; s :: S; T :: *; t :: T
Cube> :load pair.cube
Cube> :let p :: Pair S T; p = PairC S T s t
Cube> p
pair s t
  ::
pairT
Cube> fst S T p
s
  ::
S
Cube> snd S T p
t
  ::
T

The :let command is used to make bindings without having to load them from a file. The first :let just introduces some values to play with.

Again, the big difference compared to Haskell is that all types are explicit. (But users of templates in C++ or generics in Java/C# might appeciate it?)

Maybe

We can follow the same pattern and define Haskell's Maybe type. In fact any non-recursive Haskell data type has a mechanical translation and easy into lambda calculus. We've seen boolean, characters, and pairs above.

Maybe :: * -> *;
Maybe a = forall (maybeT::*) . maybeT->(a->maybeT)->maybeT;

Nothing :: forall (a::*) . Maybe a;
Nothing a = \ (maybeT::*) (nothing::maybeT) (just::a->maybeT) -> nothing;

Just :: forall (a::*) . a -> Maybe a;
Just a x = \ (maybeT::*) (nothing::maybeT) (just::a->maybeT) -> just x;

maybe :: forall (a::*) (r::*) . r -> (a->r) -> Maybe a -> r;
maybe a r nothing just s = s r nothing just;

Natural numbers

Let's carry on with some natural numbers. Natural numbers are trickier because it's a recursive type. In Haskell:

data Nat = Zero | Succ Nat

Let's try the cube version:

Cube> :load nat.cube
Cube> 2
succ (succ zero)
  ::
natT
Cube> add 2 3
succ (succ (succ (succ (succ zero))))
  ::
natT

What does the definitions for natural numbers look like?

Nat :: *;
Nat = forall (natT::*) . natT -> (natT->natT) -> natT;

0 :: Nat;
0 = \ (natT::*) (zero::natT) (succ::natT->natT) -> zero;

Succ :: Nat -> Nat;
Succ n = \ (natT::*) (zero::natT) (succ::natT->natT) -> succ (n natT zero succ);

natprim :: forall (r::*) . (r->r) -> r -> Nat -> r;
natprim r succ zero n = n r zero succ;

add :: Nat -> Nat -> Nat;
add x y = x Nat y Succ;

mul :: Nat -> Nat -> Nat;
mul x y = x Nat 0 (add y);

power :: Nat -> Nat -> Nat;
power x y = y Nat (Succ 0) (mul x);

isZero :: Nat -> Bool;
isZero n = n Bool True (\ a::Bool -> False);

1 :: Nat;
1 = Succ 0;
2 :: Nat;
2 = Succ 1;
3 :: Nat;
3 = Succ 2;

The natprim function corresponds to foldr for list and is our means of recursion. This type for natural numbers come with primitive recursion built in, just as the non-recursive data types earlier came with case analysis built in.

I'll skip defining subtraction&co, they are possible, but a little tedious (and very inefficient).

Lists

Lists are like a hybrid of natural numbers and the Maybe type. They follow the same pattern as before.

List :: * -> *;
List e = forall (listT::*) . listT -> (e->listT->listT) -> listT;

Nil :: forall (e::*) . List e;
Nil e = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> nil;

Cons :: forall (e::*) . e -> List e -> List e;
Cons e x xs = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> cons x (xs listT nil cons);

And some sample functions.

foldr :: forall (a::*) (b::*) . (a->b->b) -> b -> List a -> b;
foldr a b f z xs = xs b z f;

map :: forall (a::*) (b::*) . (a->b) -> List a -> List b;
map a b f xs = foldr a (List b) (\ (x::a) (r::List b) -> Cons b (f x) r) (Nil b) xs;

append :: forall (a::*) . List a -> List a -> List a;
append a xs ys = foldr a (List a) (Cons a) ys xs;

foldl :: forall (a::*) (b::*) . (b->a->b) -> b -> List a -> b;
foldl a b f z xs = foldr a (b->b) (\ (x::a) (g::b->b) (v::b) -> g (f v x)) (\ (x::b) -> x) xs z;

reverse :: forall (a::*) . List a -> List a;
reverse a xs = foldl a (List a) (\ (r :: List a) (x :: a) -> Cons a x r) (Nil a) xs;

And a test:

Welcome to the Cube.
Use :help to get help.
Cube> :load bool.cube
Cube> :load nat.cube
Cube> :load list.cube
Cube> :load pair.cube    
Cube> :load listmisc.cube
Cube> :load extchar.cube
Cube> :skip
Cube> replicate Char 3 'b'
cons 'b' (cons 'b' (cons 'b' nil))
  ::
listT
Cube> :quit

And with that, I'll quit too for now.

Simpler, Easier!

In a recent paper, Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus), the authors argue that type checking a dependently typed language is easy. I agree whole-heartedly, it doesn't have to be difficult at all. But I don't think the paper presents the easiest way to do it. So here is my take on how to write a simple dependent type checker. (There's nothing new here, and the authors of the paper are undoubtedly familiar with all of it.)

First, the untyped lambda calculus.

I'll start by implementing the untyped lambda calculus. It's a very simple language with just three constructs: variables, applications, and lambda expressions, i.e.,

x e e λx.e

For example, (λx.λy.x)(λz.z). In Haskell I'll use strings to represent variables names; it's simple and easy.

type Sym = String

data Expr
        = Var Sym
        | App Expr Expr
        | Lam Sym Expr
        deriving (Eq, Read, Show)

The example above represented by App (Lam "x" $ Lam "y" $ Var "x") (Lam "z" $ Var "z"). What do we want to do with the Expr type? Well, evaluating an expression seems like the thing we need. Now, there are many degrees of evaluation to choose from, Weak Head Normal Form, Head Normal Form, Normal Form, etc., etc. They differ in exactly where there might be reducible expression lingering. To evaluate lambda expression the most important step is β-reduction. A β-reduction step can be performed anywhere a function meets an argument, i.e., an application where the function is on λ form, a.k.a. a redex.

(λx.e)a reduces to e[x:=a]

Where the e[x:=a] notation means that all (free) occurrences of the variable x in the expression e are replaced by a. The example above has one redex, and doing a β step yields λy.λz.z. The other kind of reduction we will make use of is α-substitution, which is simply renaming a bound variable, e.g., λx.x can be changed to λy.y. Let's start with an easy evaluation strategy, normal order to WHNF. In WHNF we only need to make sure there the there's no redex along the "spine" of the expression, i.e., starting from the root and following the left branch in applications. Doing normal order reduction means that we do not evaluate anything inside the argument of a β redex before doing the reduction. It's sometimes called lazy evaluation, but I prefer to use that term for an implementation strategy for normal order reduction. We implement normal order WHNF by walking down the spine collecting arguments (i.e., the right branch of a applications) until we reach a lambda or a variable. If we reach a variable we already have WHNF so we just reconstitute the applications again. If we hit a lambda we get to the crux of evaluation. We need to perform a β-reduction, i.e., if we have App (Lam v e) a we need to replace all (free) occurrences of the variable v by the argument a inside the lambda body e. That's what the subst function does.

whnf :: Expr -> Expr
whnf ee = spine ee []
  where spine (App f a) as = spine f (a:as)
        spine (Lam s e) (a:as) = spine (subst s a e) as
        spine f as = foldl App f as

The subst function is the only tricky part, so let's relax by first defining something easy, namely getting the free variables from an expression. The free variables are those variables that occur in an expression, but are not bound in it. We simply collect the variables in a set (using a list as a set here), removing anything bound.

freeVars :: Expr -> [Sym]
freeVars (Var s) = [s]
freeVars (App f a) = freeVars f `union` freeVars a
freeVars (Lam i e) = freeVars e \\ [i]

Back to substitution.

subst :: Sym -> Expr -> Expr -> Expr
subst v x b = sub b
  where sub e@(Var i) = if i == v then x else e
        sub (App f a) = App (sub f) (sub a)
        sub (Lam i e) =
            if v == i then
                Lam i e
            else if i `elem` fvx then
                let i' = cloneSym e i
                    e' = substVar i i' e
                in  Lam i' (sub e')
            else
                Lam i (sub e)
        fvx = freeVars x
        cloneSym e i = loop i
           where loop i' = if i' `elem` vars then loop (i ++ "'") else i'
                 vars = fvx ++ freeVars e

substVar :: Sym -> Sym -> Expr -> Expr
substVar s s' e = subst s (Var s') e

The subst function will replace all free occurrences of v by b inside x, i.e., b[v:=x]. The Var case is easy. If it's the variable we are replacing then replace else leave it alone. The App case is also easy, just recurse in both branches. The Lam case has three alternative. First, if the bound variable is the same as the one we are replacing then there can be no free occurrences inside it, so just return the lambda as is. Second, if the lambda bound variable is among the free variables in x we have a problem (see below). Third case, just recurse in the body. So, what about the case when the lambda bound variable occurs in x? Well, if we just blindly continue substitution the variable v inside x will no longer refer to the same thing; it will refer to the variable bound in the lambda. That's no good. For example, take the expression λx.((λy.λx.y)x), the β reduction gives λx.λx'.x (or similar), whereas doing the substitution blindly would give λx.λx.x. Which is wrong! But it's easy to fix, just conjure up a variable, i' that will not clash with anything (cloneSym does that). How do we come up with a good variable? Well, we don't want to pick one that is free in the expression x because that would lead to the same problem again. Nor do we want to pick a variable that is free in e because that would accidentally bind something in e. So we take the original identifier and tack on "'" until it fulfills our requirements. (OK, efficiency affectionados are allowed to complain a little here, but this isn't that bad actually.) Once we have a new variable we can do an α-conversion to rename the offending variable to something better. The substVar function is a utility when we want to replace one variable with another. Another useful thing to be able to do is to compare lambda expression for equality. We already have syntactic equality derived for Expr, but it is also very useful to be able to compare expressions modulo α-conversions. That is, we'd like λx.x to compare equal to λy.y. Let's call that function alphaEq.

alphaEq :: Expr -> Expr -> Bool
alphaEq (Var v)   (Var v')    = v == v'
alphaEq (App f a) (App f' a') = alphaEq f f' && alphaEq a a'
alphaEq (Lam s e) (Lam s' e') = alphaEq e (substVar s' s e')
alphaEq _ _ = False

Variables and applications just proceed along the structure of the expression. When we hit a lambda the variables might be different, so we do an α-conversion of the second expression to make them equal. As the final functions, we will do reduction to Normal Form (i.e., to a form where no redexes remain) and comparison of expressions via their normal forms.

nf :: Expr -> Expr
nf ee = spine ee []
  where spine (App f a) as = spine f (a:as)
        spine (Lam s e) [] = Lam s (nf e)
        spine (Lam s e) (a:as) = spine (subst s a e) as
        spine f as = app f as
        app f as = foldl App f (map nf as)

betaEq :: Expr -> Expr -> Bool
betaEq e1 e2 = alphaEq (nf e1) (nf e2)

Computing the NF is similar to WHNF, but as we reconstruct expressions we make sure that all subexpression have NF as well. Note that both whnf and nf may fail to terminate because not all expressions have a normal form. The canonical non-terminating example is (λx.x x)(λx.x x) which has one redex, and doing the reduction produces the same term again. But if an expression has a normal form then it is unique (the Church-Rosser theorem). Here are some sample lambda terms (named for convenience):

zero ≡ λs.λz.z one ≡ λs.λz.s z two ≡ λs.λz.s (s z) three ≡ λs.λz.s (s (s z)) plus ≡ λm.λn.λs.λz.m s (n s z)

Or, in Haskell

[z,s,m,n] = map (Var . (:[])) "zsmn"
app2 f x y = App (App f x) y
zero  = Lam "s" $ Lam "z" z
one   = Lam "s" $ Lam "z" $ App s z
two   = Lam "s" $ Lam "z" $ App s $ App s z
three = Lam "s" $ Lam "z" $ App s $ App s $ App s z
plus  = Lam "m" $ Lam "n" $ Lam "s" $ Lam "z" $ app2 m s (app2 n s z)

And now we can check that addition works, betaEq (app2 plus one two) three will produce True.

A detour, simply typed lambda calculus.

To do type checking we need to introduce types. A very simple system is the simply typed lambda calculus. It has one (or more) base type (think of it as Bool or Int if you want an example) and function types. In Haskell terms:

data Type = Base | Arrow Type Type
    deriving (Eq, Read, Show)

Or

t→t B

The expressions themselves will have an explicit type on the bound variable in a lambda expression. So we now have

x e e λx:t.e

For example, (λx:(B→B).λy:B.x)(λz:B.z). The Haskell type for expressions is

data Expr
    = Var Sym
    | App Expr Expr
    | Lam Sym Type Expr
    deriving (Eq, Read, Show)

The only difference is the Type in Lam. All the functions we had for the untyped lambda calculus can be trivially extended to the simply typed one by simply carrying the type along. So finally, time for some type checking. The type checker will take an expression and return the type of the expression. The type checker will also need the types of all free variables in the expression to be able to do this. Otherwise, what type would it assign to, say, the expression x? To represent the types of the free variables we use an environment which is simply a list of variables and their types.

newtype Env = Env [(Sym, Type)] deriving (Show)

initalEnv :: Env
initalEnv = Env []

extend :: Sym -> Type -> Env -> Env
extend s t (Env r) = Env ((s, t) : r)

Type checking can go wrong; there can be type errors. To cater for this the type checker will be written in monadic style where the monad is simply an error (exception) monad. The error messages are strings, and the monad itself is the Either type. So TC is the type checking monad.

type ErrorMsg = String

type TC a = Either ErrorMsg a

We can now write variable lookup.

findVar :: Env -> Sym -> TC Type
findVar (Env r) s =
    case lookup s r of
    Just t -> return t
    Nothing -> throwError $ "Cannot find variable " ++ s

It simply looks up the variable and returns the type. If not found it throws an error with throwError (from Control.Monad.Error). And then the type checker itself.

tCheck :: Env -> Expr -> TC Type
tCheck r (Var s) =
    findVar r s
tCheck r (App f a) = do
    tf <- tCheck r f
    case tf of
     Arrow at rt -> do
        ta <- tCheck r a
        when (ta /= at) $ throwError "Bad function argument type"
        return rt
     _ -> throwError "Non-function in application"
tCheck r (Lam s t e) = do
    let r' = extend s t r
    te <- tCheck r' e
    return $ Arrow t te

For variables, just look up the type for it in the environment. For application, type check the function part and the argument part. The function should have function (arrow) type, and if it does the type of the application is the return type of the function. Finally, for a lambda expression we extend the environment with the bound variable. We then check the body, and the type of the lambda expression is a function type from the argument type to the type of the body. For convenience:

typeCheck :: Expr -> Type
typeCheck e =
    case tCheck initalEnv e of
    Left msg -> error ("Type error:\n" ++ msg)
    Right t -> t

Pretty easy sailing so far. The simply typed lambda calculus is a pain to use. Take something like λx.x in the untyped world. What type should we give it? Well that depends on how we intend to use it. Maybe λx:B.x, maybe λx:(B→B).x, maybe λx:(B→B→B).x... So we can no longer have one identity function; we need one for each type. What a bummer! It's as bad as C. BTW, all (type correct) expression in the simply typed lambda calculus have a normal form (Tait 1967).

Almost going down the wrong track, the polymorphic lambda calculus.

(Don't get me wrong, the polymorphic lambda calculus is a work of marvel.) So how can we fix the problem with one identity function for each type? We can add polymorphism! We can extend the expression language so that we also pass types around; we add type abstraction and type application.

x e e λx:t.e Λα:k.e e[t]

Where Λα:k.e is a type abstraction, i.e., α is a type variable which we can use in type expressions inside e. To supply a type argument we have type application, e[t]. So the types we have would functions, base type, and type variables.

t→t B α

And what is k in the Λα:k.e? Well, now types have gotten so complicated that it is possible to construct types that make no sense, so we need a "type system" for the types. We call them kinds.

k→k *

Defining all this is Haskell would be something like

data Expr
    = Var Sym
    | App Expr Expr
    | Lam Sym Type Expr
    | TLam Sym Kind Expr
    | TApp Expr Type
    deriving (Eq, Read, Show)
data Type
    = Arrow Type Type
    | Base
    | TVar Sym
    deriving (Eq, Read, Show)
data Kind
    = KArrow Type Type
    | Star
    deriving (Eq, Read, Show)

But wait, there's an awful lot of duplication here. The structures on the three levels have a lot of similarities. (Oh, and we don't really need Base anymore now when we have variables.) BTW, this system, called System F_ω, is (a simplified version of) what GHC uses internally to represent Haskell code. It's a beautiful system, really. Oh, the identity function, well it would be Λα:*.λx:α.x. And using it: id[B]a, assuming a has type B.

Simply easy, the lambda cube.

To simplify and (as often happens when you simplify) generalize the expressions above we are going to squish them all into one expression data type. So TLam and Lam will join, as will TApp and App, TVar and Var, KArrow and Arrow. But wait, there's nothing corresponding to Arrow in Expr. We need to add something. We could just add it as it is, but we won't. TADA, enter dependent types. Instead of the boring function type t→u we will use a more exciting one, (x:t)→u. What does it mean? It means that the variable x can occur in u. If it doesn't then it's simply the same as the old fashioned function type. If x does occur it means that type u can depend on the value of the argument (x). In Haskell:

data Expr
    = Var Sym
    | App Expr Expr
    | Lam Sym Type Expr
    | Pi  Sym Type Type
    | Kind Kinds
    deriving (Eq, Read, Show)
type Type = Expr

data Kinds = Star | Box deriving (Eq, Read, Show)

The new arrow type is called Pi. We will also need more than one kind, Star and Box. It's pretty easy to extend the functions from the first part to handle this expression type. There's just a few more places to recurse. Here's the code again. Absolutly nothing subtle about it.

freeVars :: Expr -> [Sym]
freeVars (Var s) = [s]
freeVars (App f a) = freeVars f `union` freeVars a
freeVars (Lam i t e) = freeVars t `union` (freeVars e \\ [i])
freeVars (Pi i k t) = freeVars k `union` (freeVars t \\ [i])
freeVars (Kind _) = []

subst :: Sym -> Expr -> Expr -> Expr
subst v x = sub
  where sub e@(Var i) = if i == v then x else e
        sub (App f a) = App (sub f) (sub a)
        sub (Lam i t e) = abstr Lam i t e
        sub (Pi i t e) = abstr Pi i t e
        sub (Kind k) = Kind k
        fvx = freeVars x
        cloneSym e i = loop i
           where loop i' = if i' `elem` vars then loop (i ++ "'") else i'
                 vars = fvx ++ freeVars e
        abstr con i t e =
            if v == i then
                con i (sub t) e
            else if i `elem` fvx then
                let i' = cloneSym e i
                    e' = substVar i i' e
                in  con i' (sub t) (sub e')
            else
                con i (sub t) (sub e)

To cut down on the code you could actually join the Lam and Pi constructors since they are treated identically in many cases. I've left them separate for clarity. The alphaEq function extends in the natural way to the new type, so does nf, but here it is anyway.

nf :: Expr -> Expr
nf ee = spine ee []
  where spine (App f a) as = spine f (a:as)
        spine (Lam s t e) [] = Lam s (nf t) (nf e)
        spine (Lam s _ e) (a:as) = spine (subst s a e) as
        spine (Pi s k t) as = app (Pi s (nf k) (nf t)) as
        spine f as = app f as
        app f as = foldl App f (map nf as)

So, now for the meaty part, the type checking itself. The handling of the environment is just as before, so we'll just look at the different cases for the type checking.

tCheck :: Env -> Expr -> TC Type
tCheck r (Var s) =
    findVar r s

Just as before.

tCheck r (App f a) = do
    tf <- tCheckRed r f
    case tf of
     Pi x at rt -> do
        ta <- tCheck r a
        when (not (betaEq ta at)) $ throwError $ "Bad function argument type"
        return $ subst x a rt
     _ -> throwError $ "Non-function in application"

This is almost as before, but the arrow type is called Pi now. The key thing here — and this is really where the fact that we are doing dependent types shows up — is the return type. For the simply typed lambda calculus it was just rt, but now rt can contain free occurences of the variable x. Since we are returning rt the x would no longer be in scope, so we substitute the value of the argument for it. This is coolest part of the type checker. You've seen it. That's where it is. Since types can now be arbitrary expression we use betaEq to compare them instead of (==).

tCheck r (Lam s t e) = do
    tCheck r t
    let r' = extend s t r
    te <- tCheck r' e
    let lt = Pi s t te
    tCheck r lt
    return lt

The lambda case is similar to before, but we return a Pi now, so we need to include the variable name. Furthermore, to avoid nonsense like λx:5.e we make sure that the type we want to return actually has a valid kind itself. (The first call to tCheck is to ensure the type we're putting into the environment is valid; I'm sure there's a more elegant way to do this, but I can't remember what it is right now.)

tCheck _ (Kind Star) = return $ Kind Box
tCheck _ (Kind Box) = throwError "Found a Box"

Everything has a type, so what's the type of * (Kind Star), well it's a [] (Kind Box) (excuse the ugly box, I can't find the HTML version of a box). And what's the type of Box? Well, you could keep going, but instead we'll stop right here. The idea is that the source language which we'll write our terms in will not allow the box to be written, so it should never occur.

tCheck r (Pi x a b) = do
    s <- tCheckRed r a
    let r' = extend x a r
    t <- tCheckRed r' b
    when ((s, t) `notElem` allowedKinds) $ throwError "Bad abstraction"
    return t

How do we check the type of the (dependent) function type? Well, we check the type of the thing to the left of the arrow, extend the environment, and then check the thing to the right. So now what should (s, t) be? Well, a and b should be types (or maybe kinds). So their types should be kinds. This leads to the following definition:

allowedKinds :: [(Type, Type)]
allowedKinds = [(Kind Star, Kind Star), (Kind Star, Kind Box), (Kind Box, Kind Star), (Kind Box, Kind Box)]

I.e., we allow (*,*), (*,[]), ([],*), and ([],[]). What does it all mean? Here's the beauty of the lambda cube. By varying what we allow we can change what system we type check.

(*,*) values can depend on values. Just this gives the simply typed λ calculus. ([],[]) types can depend on types. ([],*) values can depend on type. Include all these three and you get F_ω. (*,[]) types can depend on values. Include this one to get dependent types.

With all four combination allowed you get Calculus of Construction (CoC). If you always include (*,*), but make a choice of the other 3 you get 8 choices; these are the corners of the lambda cube. All of these system have been studied. BTW, all the systems in the lambda cube have the property that a well typed expression has a normal form. (Well, the proof of this is so complicated for some of these systems that some people kinda doubt it.)

Examples

Here the syntax s→t means (_:s)→t, where "_" is some new variable not used in t.

Identity
id ≡ λa:*.λx:a.x
Pairs
Pair ≡ λa:*.λb:*.(c:*→((a→b→c)→c)) pair ≡ λa:*.λb:*.λx:a.λy:b.λc:*.λf:(a→b→c).f x y split ≡ λa:*.λb:*.λr:*.λf:(a→b→r).λp:(Pair a b).p r f fst ≡ λa:*.λb:*.λp:(Pair a b).split a b a (λx:a.λy:b.x) p snd ≡ λa:*.λb:*.λp:(Pair a b).split a b b (λx:a.λy:b.y) p

My fingers are numb from all these greek characters, so I'll continue with examples another time. And, of course, a parser and pretty printer.