HOME

TheInfoList



OR:

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 Formalism may refer to: * Form (disambiguation) * Formal (disambiguation) * Legal formalism, legal positivist view that the substantive justice of a law is a question for the legislature rather than the judiciary * Formalism (linguistics) * S ...
that uses the lambda-symbol (\lambda) 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 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 ...
, 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 In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
such as ML and
Haskell Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...
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 progr ...
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 sy ...
and
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, ...
via the Curry–Howard isomorphism and they can be considered as the internal language of classes of
categories Category, plural categories, may refer to: Philosophy and general uses *Categorization, categories in cognitive science, information science and generally *Category of being * ''Categories'' (Aristotle) * Category (Kant) *Categories (Peirce) * ...
; 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 c ...
is the language of Cartesian closed categories (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 c ...
has only one type constructor, the arrow \to, 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 returni ...
s \sigma\to\tau. 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 o ...
. Lambda calculi with dependent types are the base of
intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
, 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 d ...
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 A is a subtype of B, then all terms of type A also have type B. 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 In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
'': 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 g ...
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. 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, the routines (functions, procedures, methods) of
strongly typed programming language In computer programming, one of the many ways that programming languages are colloquially classified is whether the language's type system makes it strongly typed or weakly typed (loosely typed). However, there is no precise technical definition o ...
s 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