Our lambda calculus needs a type system. Some people may argue that this makes the lambda calculus worse, but I will take the stance that a type system adds information to our programs such that we may be able to prove certain properties. The first thing is to define the system. We introduce a new kind of types:
ty : type.
nat : ty.
arrow : ty -> ty -> ty.
We inform Twelf that natural numbers are types. We inform twelf that functions can be formed via the arrow type. (arrow A B) means a function from domain A to codomain B.
Naturally, we would like a typing judgement, relating an expression to a type. To do this, we introduce a type family, called ``of'' for exactly this:
of : exp -> ty -> type.
Now, We will tell Twelf about specific relations. We directly have:
of/z : of z nat.
of/s : of (s S) nat
<- of S nat.
Zero is a natural number. And successors are natural numbers provided that the ``innards'' are. For applications, we need a bit more structure:
of/app : of (app E1 E2) T2
<- of E1 (arrow T1 T2)
<- of E2 T1.
An application has a type T2, if the first part of the application has function type (arrow T1 T2) and the value we wish to pass to the function has type T1. Finally, there is the lambda-case. Higher-order abstract types shine here:
of/lam : of (lam [x] E x) (arrow T1 T2)
<- ({x : exp} of x T1 -> of (E x) T2).
To break it up: The conclusion of the rule (the first line) says that a lambda-expression has arrow type (arrow T1 T2). The premise (second line) says: ``Suppose the variable x is an exp and suppose that x has type T1. Then we must show that (E x) has type T2''. Assumptions like these are all over the place in Twelf proof developments.
We now have most of the toolset to construct theorems. But it has to wait for a later post.
