Typed lambda calculus

Time you got around to sponsoring a child

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 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, Standard ML and Caml.

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