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 e→t.

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.