Typed versions of the lambda calculus extend the standard lambda calculus with types. By assigning to each term a type, one can insist on type compatibility during substitutions. This is a clean theoretical model of the way types operate in conventional programming languages; it is of course a restriction on the programmer. Many typed lambda calculi exist, varying in the types and typing features they support.

Simply typed lambda calculus

In the simply typed lambda calculus, each term is either a base type in the case of a constant, or a composite type in the case of a function (lambda abstraction). Composite types are denoted α→β for functions from (values of) type α to (values of) type β. The type of a function application depends on the type of the function being applied and the type of the argument.

As an example, natural language utterances can be considered as follows:

• Nouns are constants of type e, for entity.
• Sentences have type t, for truth.
• Verbs are regarded as functions from nouns to sentences, or e→t.

Uses of lambda calculi

The great advantage of simply-typed over untyped lambda calculus is that every term is or can be reduced to a normal form. This is because all forms of the untyped lambda calculus that do not have normal forms cannot receive valid types. For example, the famous Ω combinator

Ω ≡ (λ x . x x) (λ x . x x)

cannot be simply typed.

Indeed, the normal form property holds for still more powerful typed lambda calculi, such as System F.

Because of this property, a decidable equational system can be developed that considers lambda terms equal if and only if they have the same normal form (up to α-conversion). Typed lambda calculi with this property are often used to form types for typed functional programming languages, as part of the type checking process requires checking two types for equality. Notable examples in this family are Haskell, Standard ML and Caml.

Typed lambda calculi are typically associated to various intuitionistic logics through Curry-Howard isomorphisms.

See also

• H.P. Barendregt's Lambda cube
• Jean-Yves Girard's System F
• Thierry Coquand 's Calculus of Constructions