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