HOME

TheInfoList



OR:

A typed
lambda calculus In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
is a typed formalism 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 In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic ...
, 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 programs. Programming languages are described in terms of their syntax (form) and semantics (meaning), usually defined by a formal language. Languages usually provide features ...
and are the base of typed functional programming languages 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 pioneered several programming language ...
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'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usual ...
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 Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
and
proof theory Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
via the Curry–Howard isomorphism and they can be considered as the internal language of certain classes of categories. For example, the
simply typed lambda calculus 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 types. It is the canonical and simplest example of a typed lambda calculus. The ...
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 (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...
has only one
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 ones. Basic types are considered to be built using nullary type constructors. So ...
, 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 return ...
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 nea ...
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 polymorph ...
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 on ...
. 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 (MLTT)) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematicia ...
, 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 reaso ...
and the logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi on
pure type system 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 Structure (mathematic ...
s, Henk Barendregt proposed the Lambda cube 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 called subtype polymorphism or inclusion polymorphism) is a form of type polymorphism. A ''subtype'' is a datatype that is related to another datatype (the ''supertype'') by some notion of substi ...
'', 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'': all computations terminate. Therefore, they cannot describe all
Turing-computable Computable functions are the basic objects of study in computability theory. Informally, a function is ''computable'' if there is an algorithm that computes the value of the function for every value of its argument. Because of the lack of a precis ...
functions. 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 Computer programming or coding is the composition of sequences of instructions, called computer program, programs, that computers can follow to perform tasks. It involves designing and implementing algorithms, step-by-step specifications of proc ...
, 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