The simply typed lambda calculus (
λ\to
\to
The term simple type is also used to refer to extensions of the simply typed lambda calculus with constructs such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems that introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The simple types, except for full recursion, are still considered simple because the Church encodings of such structures can be done using only
\to
In the 1930s Alonzo Church sought to use the logistic method: his lambda calculus, as a formal language based on symbolic expressions, consisted of a denumerably infinite series of axioms and variables, but also a finite set of primitive symbols, denoting abstraction and scope, as well as four constants: negation, disjunction, universal quantification, and selection respectively; and also, a finite set of rules I to VI. This finite set of rules included rule V modus ponens as well as IV and VI for substitution and generalization respectively. Rules I to III are known as alpha, beta, and eta conversion in the lambda calculus. Church sought to use English only as a syntax language (that is, a metamathematical language) for describing symbolic expressions with no interpretations.
In 1940 Church settled on a subscript notation for denoting the type in a symbolic expression. In his presentation, Church used only two base types:
o
\iota
o
\iota
o
\alpha,\beta
(\alpha\beta)
\beta\to\alpha
\to
\sigma
\tau
\sigma\to\tau
\sigma
\tau
\to
\sigma\to\tau\to\rho
\sigma\to(\tau\to\rho)
To define the types, a set of base types,
B
\tau::=\tau\to\tau\midT where T\inB
For example,
B=\{a,b\}
a
b
a\toa
a\tob
b\tob
b\toa
a\to(a\toa)
(b\toa)\to(a\tob)
A set of term constants is also fixed for the base types. For example, it might be assumed that one of the base types is, and its term constants could be the natural numbers.
The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. The term
xn{:}\tau
x
\tau
e::=x\midλxn{:}\tau.e\midee\midc
where
c
x
x
In comparison, the syntax of untyped lambda calculus has no such typing or term constants:
e::=x\midλx.e\midee
Whereas in typed lambda calculus every abstraction (i.e. function) must specify the type of its argument.
To define the set of well-typed lambda terms of a given type, one defines a typing relation between terms and types. First, one introduces typing contexts, or typing environments
\Gamma,\Delta,...
xn{:}\sigma
x
\sigma
The typing relation
\Gamma\vdashen{:}\sigma
e
\sigma
\Gamma
e
\sigma
\in\Gamma}{\Gamma\vdashxn{:}\sigma}} |
T}} | |||||||
en{:}\tau}{\Gamma\vdash(λxn{:}\sigma.~e)n{:}(\sigma\to\tau)}} |
e2n{:}\sigma}{\Gamma\vdashe1~e2n{:}\tau}} |
In words,
x
\sigma
x
\sigma
x
\sigma
e
\tau
x
λxn{:}\sigma.~e
\sigma\to\tau
e1
\sigma\to\tau
e2
\sigma
e1~e2
\tau
Examples of closed terms, i.e. terms typable in the empty context, are:
\tau
λxn{:}\tau.xn{:}\tau\to\tau
\sigma,\tau
λxn{:}\sigma.λyn{:}\tau.xn{:}\sigma\to\tau\to\sigma
\tau,\tau',\tau''
λxn{:}\tau\to\tau'\to\tau''.λyn{:}\tau\to\tau'.λzn{:}\tau.xz(yz):(\tau\to\tau'\to\tau'')\to(\tau\to\tau')\to\tau\to\tau''
Each type
\tau
o(\tau)
o(T)=0
o(\sigma\to\tau)=max(o(\sigma)+1,o(\tau))
o(\iota\to\iota\to\iota)=1
o((\iota\to\iota)\to\iota)=2
Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, variously called intrinsic vs. extrinsic, ontological vs. semantical, or Church-style vs. Curry-style.[1] An intrinsic 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
λxn{:}int.~x
λxn{:}bool.~x
λxn{:}int.~x
λxn{:}bool.~x
λ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 an extrinsic semantics on annotated terms simply by ignoring the types (i.e., through type erasure), as it is possible to give an intrinsic 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 an intrinsic or extrinsic perspective.
The simply typed lambda calculus (STLC) has the same equational theory of βη-equivalence as untyped lambda calculus, but subject to type restrictions. The equation for beta reduction
(λxn{:}\sigma.~t)u=\betat[x:=u]
\Gamma
\Gamma,xn{:}\sigma\vdashtn{:}\tau
\Gamma\vdashun{:}\sigma
λxn{:}\sigma.~tx=ηt
\Gamma\vdasht:\sigma\to\tau
x
t
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.
The simply typed lambda calculus enriched with product types, pairing and projection operators (with
\betaη
There are typing rules for pairing, projection, and a unit term. Given two terms
sn{:}\sigma
tn{:}\tau
(s,t)
\sigma x \tau
un{:}\tau1 x \tau2
\pi1(u)n{:}\tau1
\pi2(u)n{:}\tau2
\pii
\pi1(sn{:}\sigma,tn{:}\tau)=sn{:}\sigma
\pi2(sn{:}\sigma,tn{:}\tau)=tn{:}\tau
(\pi1(un{:}\sigma x \tau),\pi2(un{:}\sigma x \tau))=un{:}\sigma x \tau
tn{:}1=
The above can then be turned into a category by taking the types as the objects. The morphisms
\sigma\to\tau
(xn{:}\sigma,tn{:}\tau)
\sigma
\tau
This correspondence can be extended to include "language homomorphisms" and functors between the category of Cartesian closed categories, and the category of simply typed lambda theories.
Part of this correspondence can be extended to closed symmetric monoidal categories by using a linear type system.
The simply typed lambda calculus is closely related to the implicational fragment of propositional intuitionistic logic, i.e., the implicational propositional calculus, via the Curry–Howard isomorphism: terms correspond precisely to proofs in natural deduction, and inhabited types are exactly the tautologies of this logic.
From his logistic method Church 1940 p.58 laid out an axiom schema, p. 60, which Henkin 1949 filled in with type domains (e.g. the natural numbers, the real numbers, etc.). Henkin 1996 p. 146 described how Church's logistic method could seek to provide a foundation for mathematics (Peano arithmetic and real analysis), via model theory.
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
λx.~x
int\toint
bool\tobool
\alpha\to\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
\Gamma\vdashe\Leftarrow\tau
\Gamma\vdashe ⇒ \tau
\Gamma
e
\tau
\Gamma\vdashe\Leftarrow\tau
\Gamma\vdashe ⇒ \tau
\Gamma
e
\tau
\in\Gamma}{\Gamma\vdashx ⇒ \sigma}} |
| |||||||
e\Leftarrow\tau}{\Gamma\vdashλx.~e\Leftarrow\sigma\to\tau}} |
| |||||||
|
\tau) ⇒ \tau}} |
xn{:}\sigma
\sigma
x
λx.~e
\sigma\to\tau
xn{:}\sigma
e
\tau
e1
\sigma\to\tau
e2
\sigma
e1~e2
\tau
e
\tau
\tau
e
\tau
(en{:}\tau)
\tau
Given the standard semantics, the simply typed lambda calculus is strongly normalizing: every sequence of reductions eventually terminates. 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
\Omega=(λx.~x~x)(λx.~x~x)
fix\alpha
(\alpha\to\alpha)\to\alpha
Unlike the untyped lambda calculus, the simply typed lambda calculus is not Turing complete. All programs in the simply typed lambda calculus halt. For the untyped lambda calculus, there are programs that do not halt, and moreover there is no general decision procedure that can determine whether a program halts.
\beta
\betaη
l{E}4
\betaη
(o\too)\to(o\too)
λ\to
λ\to
\betaη
\betaη
\betaη