Main Page | See live article | Alphabetical index

Typed lambda calculus

Typed versions of the lambda calculus extend the standard lambda calculus with types, assigning to each term a type. Many typed lambda calculi exist, varying in the types and typing features they support.

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 et.

The great advantage of 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 term (λ x . x x) (the ω-combinator) cannot be typed.

Typed lambda calculus is the basis of many functional programming languages, notably Haskell and Standard ML.