Substitution-Based Higher-Order Type Systems

In this lesson you learn how to define a substitution-based type system for a higher-order language, namely the LAMBDA language defined in Part 1 of the tutorial.

Let us copy the definition of LAMBDA from Part 1 of the tutorial, Lesson 8. We are going to modify it into a type systems for LAMBDA.

Before we start, it is important to clarify an important detail, namely that our type system will yield a type checker when executed, not a type inferencer. In particular, we are going to change the LAMBDA syntax to allow us to associate a type to each declared variable. The constructs which declare variables are lambda, let, letrec and mu. The syntax of all these will therefore change.

Since here we are not interested in a LAMBDA semantics anymore, we take the freedom to eliminate the Val syntactic category, our previous results. Our new results are going to be the types, because programs will now reduce to their types.

As explained, the syntax of the lambda construct needs to change, to also declare the type of the variable that it binds. We add the new syntactic category Type, with the following constructs: int, bool, the function type (which gives it its higher-order status), and parentheses as bracket. Also, we make types our K results.

We are now ready to define the typing rules.

Let us start with the typing rule for lambda abstraction: lambda X : T . E types to the function type T -> T', where T' is the type obtained by further typing E[T/X]. This can be elegantly achieved by reducing the lambda abstraction to T -> E[T/X], provided that we extend the function type construct to take expressions, not only types, as arguments, and to be strict. This can be easily achieved by redeclaring it as a strict expression construct (strictness in the second argument would suffice in this example, but it is more uniform to define it strict overall).

The typing rule for application is as simple as it can get: (T1->T2) T1 => T2.

Let us now give the typing rules of arithmetic and Boolean expression constructs. First, let us get rid of Val. Second, rewrite each value to its type, similarly to the type system for IMP++ in the previous lesson. Third, replace each semantic rule by its typing rule. Fourth, make sure you do not forget to subsort Type to Exp, so your rules above will parse.

The typing policy of the conditional statement is that its first argument should type to bool and its other two arguments should type to the same type T, which will also be the result type of the conditional. So we make the conditional construct strict in all its three arguments and we write the obvious rule: if bool then T:Type else T => T. We want a runtime check that the latter arguments are actually typed, so we write T:Type.

There is nothing special about let, except that we have to make sure we change its syntax to account for the type of the variable that it binds. This rule is a macro, so the let is desugared statically.

Similarly, the syntax of letrec and mu needs to change to account for the type of the variable that they bind. The typing of letrec remains based on its desugaring to mu; we have to make sure the types are also included now.

The typing policy of mu is that its body should type to the same type T of its variable, which is also the type of the entire mu expression. This can be elegantly achieved by rewriting it to (T -> T) E[T/X]. Recall that application is strict, so E[T/X] will be eventually reduced to its type. Then the application types correctly only if that type is also T, and in that case the result type will also be T.

kompile and krun some programs. You can, for example, take the LAMBDA programs from the first tutorial, modify them by adding types to their variable declarations, and then type check them using krun.

In the next lesson we will discuss an environment-based type system for LAMBDA.

Go to Lesson 3, Type Systems: Environment-Based Higher-Order Type Systems.

MOVIE (out of date) [6'52"]