Simply typed lambda calculus
Encyclopedia
The simply typed lambda calculus (
), a form
of type theory
, is a typed interpretation
of the lambda calculus
with only one type constructor
:
that builds function type
s. 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
, coproduct
s or natural number
s (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 are still considered simple because the Church encoding
s of such structures can be done using only
and suitable type variables, while polymorphism and dependency cannot.
. These are sometimes called atomic types or type constants. With this fixed, the syntax of types is:
.
In this article, we use
and 
to range over types. Informally, the function type 
refers to the set of functions that, given an input of type 
, produce an output of type 
.
By convention,
associates to the right: we read 
as 
.
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:
for "the type of propositions" and 
for "the type of individuals". The type 
has no term constants, whereas 
has one term constant. Frequently the calculus with only one base type, usually 
, is considered.
The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. The term syntax used in this article is as follows:
where
is a term constant.
That is, variable reference, abstractions, application, and constant. A variable reference
is bound if it is inside of an abstraction binding 
. A term is closed if there are no unbound variables.
Compare this to the syntax of untyped lambda calculus:
We see that in typed lambda calculus every function (abstraction) must specify the type of its argument.
, which are sets of typing assumptions. A typing assumption has the form 
, meaning 
has type 
.
The typing relation
indicates that 
is a term of type 
in context 
. It is therefore said that "
is well-typed (at 
)". Instances of the typing relation are called typing judgments. The validity of a typing judgment is shown by providing a typing derivation, constructed using the following typing rules (wherein the premises above the line allow us to derive the conclusion below the line):
In other words,
Examples of closed terms, i.e. terms typable in the empty context, are:
These are the typed lambda calculus representations of the basic combinators of combinatory logic
.
Each type
is assigned an order, a number 
. For base types, 
; for function types, 
. That is, the order of a type measures the depth of the most left-nested arrow. Hence:
-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
on integers and the identity term 
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,
and 
mean the same thing (i.e., the same thing as 
).
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 Church or Curry goggles.
holds in context 
whenever 
and 
, while the equation 
holds whenever 
.
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.
-equivalence) is the internal language of Cartesian Closed Categories
(CCCs), as was first observed by Lambek
.
(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.
. 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
) may have more than one type (
, 
, etc., which are all instances of the principal type 
).
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
and 
respectively. Operationally, the three components 
, 
, and 
are all inputs to the checking judgment 
, whereas the synthesis judgment 
only takes 
and 
as inputs, producing the type 
as output. These judgments are derived via the following rules:
Observe that rules [1]–[4] 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:
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 [3], because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules [5] and [6] as follows:
Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations. And in fact, annotations are needed only at β-redexes.
: that is, well-typed terms always reduce to a value, i.e., a
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 
. Recursion can be added to the language by either having a special operator 
of type 
or adding general recursive type
s, though both eliminate strong normalization.
Since it is strongly normalizing, it is decidable
whether or not a simply typed lambda calculus program halts: it does! We can therefore conclude that the language is not Turing complete.
), a formof type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, is a typed interpretation
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
of the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
with only one type constructor
Type constructor
In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old. Typical type constructors encountered are product types, function types, power types and list types. Basic types are considered...
:
that builds function typeFunction type
In computer science, a function type is the type of a variable or parameter to which a function has or can be assigned or the result type of a higher-order function returning a function....
s. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church
Alonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life: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
Cartesian product
In mathematics, a Cartesian product is a construction to build a new set out of a number of given sets. Each member of the Cartesian product corresponds to the selection of one element each in every one of those sets...
, coproduct
Coproduct
In category theory, the coproduct, or categorical sum, is the category-theoretic construction which includes the disjoint union of sets and of topological spaces, the free product of groups, and the direct sum of modules and vector spaces. The coproduct of a family of objects is essentially the...
s or natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s (System T
System T
In mathematics, System T can refer to:* A theory of arithmetic in all finite types use in Gödel's Dialectica interpretation* An axiom system of modal logic...
) or even full recursion
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
(like PCF
Programming language for Computable Functions
In computer science, Programming Computable Functions,"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions" . Programming Computable Functions is used by . It is also referred to as Programming with Computable Functions or Programming language...
). In contrast, systems which introduce polymorphic types (like System F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
) or dependent types
Dependent type
In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram....
(like the Logical Framework
LF (logical framework)
In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for ...
) are not considered simply typed. The former are still considered simple because the Church encoding
Church encoding
In mathematics, Church encoding is a means of embedding data and operators into the lambda calculus, the most familiar form being the Church numerals, a representation of the natural numbers using lambda notation...
s of such structures can be done using only
and suitable type variables, while polymorphism and dependency cannot.Syntax
To define the types, we begin by fixing a set of base types,. These are sometimes called atomic types or type constants. With this fixed, the syntax of types is:.In this article, we use
and to range over types. Informally, the function type refers to the set of functions that, given an input of type , produce an output of type .By convention,
associates to the right: we read as .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:
for "the type of propositions" and for "the type of individuals". The type has no term constants, whereas has one term constant. Frequently the calculus with only one base type, usually , is considered.The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. The term syntax used in this article is as follows:
where
is a term constant.That is, variable reference, abstractions, application, and constant. A variable reference
is bound if it is inside of an abstraction binding . A term is closed if there are no unbound variables.Compare this to the syntax of untyped lambda calculus:
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, which are sets of typing assumptions. A typing assumption has the form , meaning has type .The typing relation
indicates that is a term of type in context . It is therefore said that " is well-typed (at )". Instances of the typing relation are called typing judgments. The validity of a typing judgment is shown by providing a typing derivation, constructed using the following typing rules (wherein the premises above the line allow us to derive the conclusion below the line):  (1)  (2) |
 (3)  (4) |
In other words,
- If
has type 
in the context, we know that 
has type 
. - Term constants have the appropriate base types.
- If, in a certain context with
having type 
, 
has type 
, then, in the same context without 
, 
has type 
. - If, in a certain context,
has type 
, and 
has type 
, then 
has type 
.
Examples of closed terms, i.e. terms typable in the empty context, are:
- For every type
, a term 
(the I-combinator/identity function), - For types
, a term 
(the K-combinator), and - For types
, a term 
(the S-combinator).
These are the typed lambda calculus representations of the basic combinators of combinatory logic
Combinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
.
Each type
is assigned an order, a number . For base types, ; for function types, . That is, the order of a type measures the depth of the most left-nested arrow. Hence:
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 ChurchAlonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
-style vs. Curry
Haskell Curry
Haskell Brooks Curry was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...
-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
on integers and the identity term on booleans may mean different things. (The classic intended interpretationsare 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,
and mean the same thing (i.e., the same thing as ).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
Type erasure
In programming languages, type erasure refers to the compile-time process by which explicit type annotations are removed from a program, before it is executed at run-time. An operational semantics that does not require programs to be accompanied by types is called a type-erasure semantics, to be...
), 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
Type inference
Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
). 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 Church or Curry goggles.
Equational theory
The simply typed lambda calculus has the same theory of βη-equivalence as untyped lambda calculus, but subject to type restrictions. The equation holds in context whenever and , while the equation holds whenever .Operational semantics
Likewise, the operational semanticsOperational semantics
In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
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
Evaluation strategy
In computer science, an evaluation strategy is a set of rules for evaluating expressions in a programming language. Emphasis is typically placed on functions or operators: an evaluation strategy defines when and in what order the arguments to a function are evaluated, when they are substituted...
. As for any typed language, type safety
Type safety
In computer science, type safety is the extent to which a programming language discourages or prevents type errors. A type error is erroneous or undesirable program behaviour caused by a discrepancy between differing data types...
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-equivalence) is the internal language of Cartesian Closed CategoriesCartesian closed category
In category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in...
(CCCs), as was first observed by Lambek
Joachim Lambek
Joachim Lambek is Peter Redpath Emeritus Professor of Pure Mathematics at McGill University, where he earned his Ph.D. degree in 1950 with Hans Julius Zassenhaus as advisor. He is called Jim by his friends.- Scholarly work :...
.
Proof-theoretic semantics
The simply typed lambda calculus is closely related to the implicational fragment of propositional intuitionistic logicIntuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
(i.e., minimal logic) via the Curry–Howard isomorphism: terms correspond precisely to proofs in natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
, and inhabited types are exactly the tautologies
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
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 inferenceType inference
Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
. 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
Principal type
In type theory, the principal type of an expression is the most general possible type given an expression. One way to compute the principal type of an expression is by deploying Robinson's unification algorithm, which is used by the Hindley–Milner type inference algorithm.Expressions always...
, since often an unannotated term (such as
) may have more than one type (, , etc., which are all instances of the principal type ).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
Type system
A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
is divided into two judgments, representing both checking and synthesis, written
and respectively. Operationally, the three components , , and are all inputs to the checking judgment , whereas the synthesis judgment only takes and as inputs, producing the type as output. These judgments are derived via the following rules:
 [1]  [2] |
 [3]  [4] |
 [5]  [6] |
Observe that rules [1]–[4] 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
is in the context, we can synthesize type 
for 
. - The types of term constants are fixed and can be synthesized.
- To check that
has type 
in some context, we extend the context with 
and check that 
has type 
. - If
synthesizes type 
(in some context), and 
checks against type 
(in the same context), then 
synthesizes type 
.
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 [3], because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules [5] and [6] as follows:
- To check that
has type 
, it suffices to synthesize type 
. - If
checks against type 
, then the explicitly annotated term 
synthesizes 
.
Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations. And in fact, annotations are needed only at β-redexes.
General observations
Given the standard semantics, the simply typed lambda calculus is strongly normalizingNormalization property (lambda-calculus)
In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form...
: that is, well-typed terms always reduce to a value, i.e., a
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 . Recursion can be added to the language by either having a special operator of type or adding general recursive typeRecursive type
In computer programming languages, a recursive data type is a data type for values that may contain other values of the same type...
s, though both eliminate strong normalization.
Since it is strongly normalizing, it is decidable
Decidability (logic)
In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
whether or not a simply typed lambda calculus program halts: it does! We can therefore conclude that the language is not Turing complete.
Important results
- Tait showed in 1967 that
-reduction is strongly normalizingNormalization property (lambda-calculus)In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form...
. As a corollary
-equivalence is decidableDecidability (logic)In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
. Statman showed in 1977 that the normalisation problem is not elementary recursive. A purely semantic normalisation proof (see normalisation by evaluationNormalisation by evaluationIn programming language semantics, normalisation by evaluation is a style of obtaining the normal form of terms in the λ calculus by appealing to their denotational semantics. A term is first interpreted into a denotational model of the λ-term structure, and then a canonical representative is...
) was given by Berger and Schwichtenberg in 1991. - The unification problem for
-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. Whether higher order matching (unification where only one term contains existential variables) is decidable is still open. [2006: Colin Stirling, Edinburgh, has published a proof-sketch in which he claims that the problem is decidable; however, the complete version of the proof is still unpublished] - We can encode natural numberNatural numberIn mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s by terms of the type
(Church numerals). Schwichtenberg showed in 1976 that in 
exactly the extended polynomialPolynomialIn mathematics, a polynomial is an expression of finite length constructed from variables and constants, using only the operations of addition, subtraction, multiplication, and non-negative integer exponents...
s are representable as functions over Church numerals; these are roughly the polynomials closed up under a conditional operator. - A full model of
is given by interpreting base types as sets and function types by the set-theoretic function spaceFunction spaceIn mathematics, a function space is a set of functions of a given kind from a set X to a set Y. It is called a space because in many applications it is a topological space, a vector space, or both.-Examples:...
. Friedman showed in 1975 that this interpretation is completeCompletenessIn general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields.-Logical completeness:In logic, semantic completeness is the converse of soundness for formal systems...
for
-equivalence, if the base types are interpreted by infinite sets. Statman showed in 1983 that 
-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 
-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.
See also
- Article Church's Type Theory in the Stanford Encyclopedia of Philosophy.
- Hindley-Milner type inference algorithm