The simply typed lambda calculus ($\backslash lambda^\backslash to$), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor ($\backslash to$) that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.
The term ''simple type'' is also used to refer to extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered ''simply typed''. The former, except full recursion, are still considered ''simple'' because the Church encodings of such structures can be done using only $\backslash to$ and suitable type variables, while polymorphism and dependency cannot.

** Syntax **

In this article, we use $\backslash sigma$ and $\backslash tau$ to range over types. Informally, the ''function type'' $\backslash sigma\; \backslash to\; \backslash tau$ refers to the type of functions that, given an input of type $\backslash sigma$, produce an output of type $\backslash tau$.
By convention, $\backslash to$ associates to the right: we read $\backslash sigma\backslash to\backslash tau\backslash to\backslash rho$ as $\backslash sigma\backslash to(\backslash tau\backslash to\backslash rho)$.
To define the types, we begin by fixing a set of ''base types'', $B$. These are sometimes called ''atomic types'' or ''type constants''. With this fixed, the syntax of types is:
:$\backslash tau\; ::=\; \backslash tau\; \backslash to\; \backslash tau\; \backslash mid\; T\; \backslash quad\; \backslash mathrm\; \backslash quad\; T\; \backslash in\; B$.
For example, $B\; =\; \backslash $, generates an infinite set of types starting with $a,b,$$a\; \backslash to\; a,$$a\; \backslash to\; b,b\backslash to\; b,$$b\backslash to\; a,$$a\; \backslash to\; (a\; \backslash to\; a),\backslash ldots,$$(b\backslash to\; a)\; \backslash to\; (a\backslash to\; b),\; \backslash ldots$
We also fix a set of ''term constants'' for the base types. For example, we might assume a base type `nat`, and the term constants could be the natural numbers. In the original presentation, Church used only two base types: $o$ for "the type of propositions" and $\backslash iota$ for "the type of individuals". The type $o$ has no term constants, whereas $\backslash iota$ has one term constant. Frequently the calculus with only one base type, usually $o$, is considered.
The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. We write $x\backslash mathbin\backslash tau$ to denote that the variable $x$ is of type $\backslash tau$. The term syntax, in BNF, is then:
:$e\; ::=\; x\; \backslash mid\; \backslash lambda\; x\backslash mathbin\backslash tau.e\; \backslash mid\; e\; \backslash ,\; e\; \backslash mid\; c$
where $c$ is a term constant.
That is, ''variable reference'', ''abstractions'', ''application'', and ''constant''. A variable reference $x$ is ''bound'' if it is inside of an abstraction binding $x$. A term is ''closed'' if there are no unbound variables.
Compare this to the syntax of untyped lambda calculus:
:$e\; ::=\; x\; \backslash mid\; \backslash lambda\; x.e\; \backslash mid\; e\; \backslash ,\; e$
We see that in typed lambda calculus every function (''abstraction'') must specify the type of its argument.

** Typing rules **

To define the set of well-typed lambda terms of a given type, we will define a typing relation between terms and types. First, we introduce ''typing contexts'' or ''typing environments'' $\backslash Gamma,\backslash Delta,\backslash dots$, which are sets of typing assumptions. A ''typing assumption'' has the form $x\backslash mathbin\backslash sigma$, meaning $x$ has type $\backslash sigma$.
The ''typing relation'' $\backslash Gamma\backslash vdash\; e\backslash mathbin\backslash sigma$ indicates that $e$ is a term of type $\backslash sigma$ in context $\backslash Gamma$. In this case $e$ is said to be ''well-typed'' (having type $\backslash sigma$). Instances of the typing relation are called ''typing judgements''. The validity of a typing judgement is shown by providing a ''typing derivation'', constructed using typing rules (wherein the premises above the line allow us to derive the conclusion below the line). Simply-typed lambda calculus uses these rules:
In words,
# If $x$ has type $\backslash sigma$ in the context, we know that $x$ has type $\backslash sigma$.
# Term constants have the appropriate base types.
# If, in a certain context with $x$ having type $\backslash sigma$, $e$ has type $\backslash tau$, then, in the same context without $x$, $\backslash lambda\; x\backslash mathbin\backslash sigma.~e$ has type $\backslash sigma\; \backslash to\; \backslash tau$.
# If, in a certain context, $e\_1$ has type $\backslash sigma\; \backslash to\; \backslash tau$, and $e\_2$ has type $\backslash sigma$, then $e\_1~e\_2$ has type $\backslash tau$.
Examples of closed terms, ''i.e.'' terms typable in the empty context, are:
*For every type $\backslash tau$, a term $\backslash lambda\; x\backslash mathbin\backslash tau.x\backslash mathbin\backslash tau\backslash to\backslash tau$ (identity function/I-combinator),
*For types $\backslash sigma,\backslash tau$, a term $\backslash lambda\; x\backslash mathbin\backslash sigma.\backslash lambda\; y\backslash mathbin\backslash tau.x\backslash mathbin\backslash sigma\; \backslash to\; \backslash tau\; \backslash to\; \backslash sigma$ (the K-combinator), and
*For types $\backslash tau,\backslash tau\text{'},\backslash tau\text{'}\text{'}$, a term $\backslash lambda\; x\backslash mathbin\backslash tau\backslash to\backslash tau\text{'}\backslash to\backslash tau\text{'}\text{'}.\backslash lambda\; y\backslash mathbin\backslash tau\backslash to\backslash tau\text{'}.\backslash lambda\; z\backslash mathbin\backslash tau.x\; z\; (y\; z)\; :\; (\backslash tau\backslash to\backslash tau\text{'}\backslash to\backslash tau\text{'}\text{'})\backslash to(\backslash tau\backslash to\backslash tau\text{'})\backslash to\backslash tau\backslash to\backslash tau\text{'}\text{'}$ (the S-combinator).
These are the typed lambda calculus representations of the basic combinators of combinatory logic.
Each type $\backslash tau$ is assigned an order, a number $o(\backslash tau)$. For base types, $o(T)=0$; for function types, $o(\backslash sigma\backslash to\backslash tau)=\backslash mbox(o(\backslash sigma)+1,o(\backslash tau))$. That is, the order of a type measures the depth of the most left-nested arrow. Hence:
: $o(\backslash iota\; \backslash to\; \backslash iota\; \backslash to\; \backslash iota)\; =\; 1$
: $o((\backslash iota\; \backslash to\; \backslash iota)\; \backslash to\; \backslash iota)\; =\; 2$

** Semantics **

** Intrinsic vs. extrinsic interpretations **

Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, sometimes called ''intrinsic'' vs. ''extrinsic'', or ''Church-style'' vs. ''Curry-style''.
An intrinsic/Church-style semantics only assigns meaning to well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. For example, the identity term $\backslash lambda\; x\backslash mathbin\backslash mathtt.~x$ on integers and the identity term $\backslash lambda\; x\backslash mathbin\backslash mathtt.~x$ on booleans may mean different things. (The classic intended interpretations
are the identity function on integers and the identity function on boolean values.)
In contrast, an extrinsic/Curry-style semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language. In this view, $\backslash lambda\; x\backslash mathbin\backslash mathtt.~x$ and $\backslash lambda\; x\backslash mathbin\backslash mathtt.~x$ mean the same thing (''i.e.'', the same thing as $\backslash lambda\; x.~x$).
The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise. It is possible to define a Curry-style semantics on annotated terms simply by ignoring the types (''i.e.'', through type erasure), as it is possible to give a Church-style semantics on unannotated terms when the types can be deduced from context (''i.e.'', through type inference). The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language. Most of the different semantic interpretations discussed below can be seen through either a Church or Curry perspective.

** Equational theory **

The simply typed lambda calculus has the same equational theory of Î²Î·-equivalence as untyped lambda calculus, but subject to type restrictions. The equation for beta reduction
:$(\backslash lambda\; x\backslash mathbin\backslash sigma.~t)\backslash ,u\; =\_\; t:=u/math>\; holds\; in\; context$ \backslash Gamma$whenever$ \backslash Gamma,x\backslash mathbin\backslash sigma\; \backslash vdash\; t\backslash mathbin\backslash tau$and$ \backslash Gamma\backslash vdash\; u\backslash mathbin\backslash sigma$,\; while\; the\; equation\; foreta\; reduction:$ \backslash lambda\; x\backslash mathbin\backslash sigma.~t\backslash ,x\; =\_\backslash eta\; t$holds\; whenever$ \backslash Gamma\backslash vdash\; t\backslash !:\backslash sigma\; \backslash to\; \backslash tau$and$ x$does\; not\; appear\; free\; in$ t$.$

** Operational semantics **

Likewise, the operational semantics of simply typed lambda calculus can be fixed as for the untyped lambda calculus, using call by name, call by value, or other evaluation strategies. As for any typed language, type safety is a fundamental property of all of these evaluation strategies. Additionally, the strong normalization property described below implies that any evaluation strategy will terminate on all simply typed terms.

** Categorical semantics **

The simply typed lambda calculus (with $\backslash beta\backslash eta$-equivalence) is the internal language of Cartesian closed categories (CCCs), as was first observed by Lambek. Given any specific CCC, the basic types of the corresponding lambda calculus are just the objects, and the terms are the morphisms. Conversely, every simply typed lambda calculus gives a CCC whose objects are the types, and morphisms are equivalence classes of terms.
To make the correspondence clear, a type constructor for the Cartesian product is typically added to the above. To preserve the categoricity of the Cartesian product, one adds type rules for ''pairing'', ''projection'', and a ''unit term''. Given two terms $s\backslash mathbin\backslash sigma$ and $t\backslash mathbin\backslash tau$, the term $(s,t)$ has type $\backslash sigma\backslash times\backslash tau$. Likewise, if one has a term $u\backslash mathbin\backslash tau\_1\backslash times\backslash tau\_2$, then there are terms $\backslash pi\_1(u)\backslash mathbin\backslash tau\_1$ and $\backslash pi\_2(u)\backslash mathbin\backslash tau\_2$ where the $\backslash pi\_i$ correspond to the projections of the Cartesian product. The ''unit term'', of type 1, is written as $()$ and vocalized as 'nil', is the final object. The equational theory is extended likewise, so that one has
:$\backslash pi\_1(s\backslash mathbin\backslash sigma,t\backslash mathbin\backslash tau)\; =\; s\backslash mathbin\backslash sigma$
:$\backslash pi\_2(s\backslash mathbin\backslash sigma,t\backslash mathbin\backslash tau)\; =\; t\backslash mathbin\backslash tau$
:$(\backslash pi\_1(u\backslash mathbin\backslash sigma\backslash times\backslash tau)\; ,\; \backslash pi\_2(u\backslash mathbin\backslash sigma\backslash times\backslash tau))\; =u\backslash mathbin\backslash sigma\backslash times\backslash tau$
:$t\backslash mathbin1\; =\; ()$
This last is read as "''if t has type 1, then it reduces to nil''".
The above can then be turned into a category by taking the types as the objects. The morphisms $\backslash sigma\backslash to\backslash tau$ are equivalence classes of pairs $(x\backslash mathbin\backslash sigma,\; t\backslash mathbin\backslash tau)$ where ''x'' is a variable (of type $\backslash sigma$) and ''t'' is a term (of type $\backslash tau$), having no free variables in it, except for (optionally) ''x''. Closure is obtained from currying and application, as usual.
More precisely, there exist functors between the category of Cartesian closed categories, and the category of simply-typed lambda theories.
It is common to extend this case to closed symmetric monoidal categories by using a linear type system. The reason for this is that the CCC is a special case of the closed symmetric monoidal category, which is typically taken to be the category of sets. This is fine for laying the foundations of set theory, but the more general topos seems to provide a superior foundation.

** Proof-theoretic semantics **

The simply typed lambda calculus is closely related to the implicational fragment of propositional intuitionistic logic, i.e., minimal logic, via the Curryâ€“Howard isomorphism: terms correspond precisely to proofs in natural deduction, and inhabited types are exactly the tautologies of minimal logic.

** Alternative syntaxes **

The presentation given above is not the only way of defining the syntax of the simply typed lambda calculus. One alternative is to remove type annotations entirely (so that the syntax is identical to the untyped lambda calculus), while ensuring that terms are well-typed via Hindleyâ€“Milner type inference. The inference algorithm is terminating, sound, and complete: whenever a term is typable, the algorithm computes its type. More precisely, it computes the term's principal type, since often an unannotated term (such as $\backslash lambda\; x.~x$) may have more than one type ($\backslash mathtt\; \backslash to\; \backslash mathtt$, $\backslash mathtt\; \backslash to\; \backslash mathtt$, etc., which are all instances of the principal type $\backslash alpha\; \backslash to\; \backslash alpha$).
Another alternative presentation of simply typed lambda calculus is based on bidirectional type checking, which requires more type annotations than Hindleyâ€“Milner inference but is easier to describe. The type system is divided into two judgments, representing both ''checking'' and ''synthesis'', written $\backslash Gamma\; \backslash vdash\; e\; \backslash Leftarrow\; \backslash tau$ and $\backslash Gamma\; \backslash vdash\; e\; \backslash Rightarrow\; \backslash tau$ respectively. Operationally, the three components $\backslash Gamma$, $e$, and $\backslash tau$ are all ''inputs'' to the checking judgment $\backslash Gamma\; \backslash vdash\; e\; \backslash Leftarrow\; \backslash tau$, whereas the synthesis judgment $\backslash Gamma\; \backslash vdash\; e\; \backslash Rightarrow\; \backslash tau$ only takes $\backslash Gamma$ and $e$ as inputs, producing the type $\backslash tau$ as output. These judgments are derived via the following rules:
Observe that rules €“are nearly identical to rules (1)â€“(4) above, except for the careful choice of checking or synthesis judgments. These choices can be explained like so:
# If $x\backslash mathbin\backslash sigma$ is in the context, we can synthesize type $\backslash sigma$ for $x$.
# The types of term constants are fixed and can be synthesized.
# To check that $\backslash lambda\; x.~e$ has type $\backslash sigma\; \backslash to\; \backslash tau$ in some context, we extend the context with $x\backslash mathbin\backslash sigma$ and check that $e$ has type $\backslash tau$.
# If $e\_1$ synthesizes type $\backslash sigma\; \backslash to\; \backslash tau$ (in some context), and $e\_2$ checks against type $\backslash sigma$ (in the same context), then $e\_1~e\_2$ synthesizes type $\backslash tau$.
Observe that the rules for synthesis are read top-to-bottom, whereas the rules for checking are read bottom-to-top. Note in particular that we do not need any annotation on the lambda abstraction in rule because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules and as follows:

** General observations **

Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a $\backslash lambda$ abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term $\backslash Omega\; =\; (\backslash lambda\; x.~x~x)\; (\backslash lambda\; x.~x~x)$. Recursion can be added to the language by either having a special operator $\backslash mathtt\_\backslash alpha$of type $(\backslash alpha\; \backslash to\; \backslash alpha)\; \backslash to\; \backslash alpha$ or adding general recursive types, though both eliminate strong normalization.
Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it ''always'' halts. We can therefore conclude that the language is ''not'' Turing complete.

** Important results **

* Tait showed in 1967 that $\backslash beta$-reduction is strongly normalizing. As a corollary $\backslash beta\backslash eta$-equivalence is decidable. Statman showed in 1977 that the normalisation problem is not elementary recursive, a proof which was later simplified by Mairson (1992). A purely semantic normalisation proof (see normalisation by evaluation) was given by Berger and Schwichtenberg in 1991.
* The unification problem for $\backslash beta\backslash eta$-equivalence is undecidable. Huet showed in 1973 that 3rd order unification is undecidable and this was improved upon by Baxter in 1978 then by Goldfarb in 1981 by showing that 2nd order unification is already undecidable. A proof that higher order matching (unification where only one term contains existential variables) is decidable was announced by Colin Stirling in 2006, and a full proof was published in 2009.
* We can encode natural numbers by terms of the type $(o\backslash to\; o)\backslash to(o\; \backslash to\; o)$ (Church numerals). Schwichtenberg showed in 1976 that in $\backslash lambda^\backslash to$ exactly the extended polynomials are representable as functions over Church numerals; these are roughly the polynomials closed up under a conditional operator.
* A ''full model'' of $\backslash lambda^\backslash to$ is given by interpreting base types as sets and function types by the set-theoretic function space. Friedman showed in 1975 that this interpretation is complete for $\backslash beta\backslash eta$-equivalence, if the base types are interpreted by infinite sets. Statman showed in 1983 that $\backslash beta\backslash eta$-equivalence is the maximal equivalence which is ''typically ambiguous'', i.e. closed under type substitutions (''Statman's Typical Ambiguity Theorem''). A corollary of this is that the ''finite model property'' holds, i.e. finite sets are sufficient to distinguish terms which are not identified by $\backslash beta\backslash eta$-equivalence.
* Plotkin introduced logical relations in 1973 to characterize the elements of a model which are definable by lambda terms. In 1993 Jung and Tiuryn showed that a general form of logical relation (Kripke logical relations with varying arity) exactly characterizes lambda definability. Plotkin and Statman conjectured that it is decidable whether a given element of a model generated from finite sets is definable by a lambda term (''Plotkinâ€“Statman conjecture''). The conjecture was shown to be false by Loader in 1993.

** Notes **

** References **

* A. Church

A Formulation of the Simple Theory of Types

JSL 5, 1940 * W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967 * G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973 * G.P. Huet

The Undecidability of Unification in Third Order Logic

Information and Control 22(3): 257-267 (1973) * H. Friedman

Equality between functionals

LogicColl. '73, pages 22-37, LNM 453, 1975. * H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114. * R. Statman

The Typed lambda-Calculus Is not Elementary Recursive

FOCS 1977: 90-94 * W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230. * R. Statman. $\backslash lambda$-definable functionals and $\backslash beta\backslash eta$ conversion. Arch. Math. Logik, 23:21â€“26, 1983. * J. Lambek

Cartesian Closed Categories and Typed Lambda-calculi

Combinators and Functional Programming Languages 1985: 136-175 * U. Berger, H. Schwichtenberg

An Inverse of the Evaluation Functional for Typed lambda-calculus

LICS 1991: 203-211 * H. Mairson

A simple proof of a theorem of Statman

TCS 103(2):387-394, 1992. * Jung, A.,Tiuryn, J

A New Characterization of Lambda Definability

TLCA 1993 * R. Loader

The Undecidability of Î»-definability

appeared in the Church Festschrift, 2001 * H. Barendregt, tp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. . * L. Baxter

The undecidability of the third order dyadic unification problem

Information and Control 38(2), 170-178 (1978)

** External links **

*
* {{SEP|type-theory-church|Church's Type Theory
Category:Lambda calculus
Category:Theory of computation
Category:Type theory

- To check that $e$ has type $\backslash tau$, it suffices to synthesize type $\backslash tau$.
- If $e$ checks against type $\backslash tau$, then the explicitly annotated term $(e\backslash mathbin\backslash tau)$ synthesizes $\backslash tau$.

A Formulation of the Simple Theory of Types

JSL 5, 1940 * W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967 * G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973 * G.P. Huet

The Undecidability of Unification in Third Order Logic

Information and Control 22(3): 257-267 (1973) * H. Friedman

Equality between functionals

LogicColl. '73, pages 22-37, LNM 453, 1975. * H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114. * R. Statman

The Typed lambda-Calculus Is not Elementary Recursive

FOCS 1977: 90-94 * W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230. * R. Statman. $\backslash lambda$-definable functionals and $\backslash beta\backslash eta$ conversion. Arch. Math. Logik, 23:21â€“26, 1983. * J. Lambek

Cartesian Closed Categories and Typed Lambda-calculi

Combinators and Functional Programming Languages 1985: 136-175 * U. Berger, H. Schwichtenberg

An Inverse of the Evaluation Functional for Typed lambda-calculus

LICS 1991: 203-211 * H. Mairson

A simple proof of a theorem of Statman

TCS 103(2):387-394, 1992. * Jung, A.,Tiuryn, J

A New Characterization of Lambda Definability

TLCA 1993 * R. Loader

The Undecidability of Î»-definability

appeared in the Church Festschrift, 2001 * H. Barendregt, tp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. . * L. Baxter

The undecidability of the third order dyadic unification problem

Information and Control 38(2), 170-178 (1978)