A typed
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
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 (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the
untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and ''untyped lambda calculus'' a special case with only one type.
Typed lambda calculi are foundational
programming languages
A programming language is a system of notation for writing computer program, computer programs. Most programming languages are text-based formal languages, but they may also be visual programming language, graphical. They are a kind of computer ...
and are the base of typed
functional programming languages such as
ML and
Haskell and, more indirectly, typed
imperative programming languages. Typed lambda calculi play an important role in the design of
type systems
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...
for programming languages; here, typability usually captures desirable properties of the program (e.g., the program will not cause a memory access violation).
Typed lambda calculi are closely related to
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
and
proof theory via the
Curry–Howard isomorphism and they can be considered as the
internal language of classes of
categories; e.g., the
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda ...
is the language of
Cartesian closed categories
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 ma ...
(CCCs).
Kinds of typed lambda calculi
Various typed lambda calculi have been studied. The
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda ...
has only one
type constructor, the arrow
, and its only types are
basic types and
function type In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or ret ...
s
.
System T extends the simply typed lambda calculus with a type of natural numbers and higher order primitive recursion; in this system all functions provably recursive in
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
are definable.
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions that are provably total in
second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies ...
. Lambda calculi with
dependent types are the base of
intuitionistic type theory, the
calculus of constructions
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason ...
and the
logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi on
pure type system __NOTOC__
In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and ...
s,
Henk Barendregt
Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory.
Life and work
Barendregt studied mathematical logic at Utrecht University, obtaining his master's de ...
proposed the
Lambda cube
In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ ...
to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions).
Some typed lambda calculi introduce a notion of ''
subtyping
In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, ...
'', i.e. if
is a subtype of
, then all terms of type
also have type
. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and
System F<:.
All the systems mentioned so far, with the exception of the untyped lambda calculus, are ''
strongly normalizing'': all computations terminate. Therefore, they cannot describe all
Turing-computable functions.
[since the ]halting problem
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a ...
for the latter class was proven to be undecidable As another consequence they are consistent as a logic, i.e. there are uninhabited types. There exist, however, typed lambda calculi that are not strongly normalizing. For example the dependently typed lambda calculus with a type of all types (Type : Type) is not normalizing due to
Girard's paradox
In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). They were both proved inconsistent by Jea ...
. This system is also the simplest pure type system, a formalism which generalizes the Lambda cube. Systems with explicit recursion combinators, such as
Plotkin's "
Programming language for Computable Functions" (PCF), are not normalizing, but they are not intended to be interpreted as a logic. Indeed, PCF is a prototypical, typed functional programming language, where types are used to ensure that programs are well-behaved but not necessarily that they are terminating.
Applications to programming languages
In
computer programming
Computer programming is the process of performing a particular computation (or more generally, accomplishing a specific computing result), usually by designing and building an executable computer program. Programming involves tasks such as anal ...
, the routines (functions, procedures, methods) of
strongly typed programming languages closely correspond to typed lambda expressions.
See also
*
Kappa calculus—an analogue of typed lambda calculus which excludes higher-order functions
Notes
Further reading
*
* Brandl, Helmut (2022)
Calculus of Constructions / Typed Lambda Calculus
{{DEFAULTSORT:Typed Lambda Calculus
Lambda calculus
Logic in computer science
Theory of computation
Type theory