Simply Typed Lambda Calculus - Alternative Syntaxes

Alternative Syntaxes

The presentation given above is not the only way of defining the syntax of the simply typed lambda calculus. One alternative is to remove type annotations entirely (so that the syntax is identical to the untyped lambda calculus), while ensuring that terms are well-typed via Hindley-Milner type inference. The inference algorithm is terminating, sound, and complete: whenever a term is typable, the algorithm computes its type. More precisely, it computes the term's principal type, since often an unannotated term (such as ) may have more than one type (, etc., which are all instances of the principal type ).

Another alternative presentation of simply typed lambda calculus is based on bidirectional type checking, which requires more type annotations than Hindley-Milner inference but is easier to describe. The type system is divided into two judgments, representing both checking and synthesis, written and respectively. Operationally, the three components, and are all inputs to the checking judgment, whereas the synthesis judgment only takes and as inputs, producing the type as output. These judgments are derived via the following rules:

Observe that rules – are nearly identical to rules (1)–(4) above, except for the careful choice of checking or synthesis judgments. These choices can be explained like so:

1. If is in the context, we can synthesize type for .
2. The types of term constants are fixed and can be synthesized.
3. To check that has type in some context, we extend the context with and check that has type .
4. If synthesizes type (in some context), and checks against type (in the same context), then synthesizes type .

Observe that the rules for synthesis are read top-to-bottom, whereas the rules for checking are read bottom-to-top. Note in particular that we do not need any annotation on the lambda abstraction in rule, because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules and as follows:

5. To check that has type, it suffices to synthesize type .
6. If checks against type, then the explicitly annotated term synthesizes .

Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations. And in fact, annotations are needed only at β-redexes.