# Typed lambda calculus

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Typed_lambda_calculus
> Markdown URL: https://mediated.wiki/source/Typed_lambda_calculus.md
> Source: https://en.wikipedia.org/wiki/Typed_lambda_calculus
> Source revision: 1318206586
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Formalism in computer science

In [mathematics](/source/Mathematics) and [computer science](/source/Computer_science), a **typed [lambda calculus](/source/Lambda_calculus)** is a [typed](/source/Type_theory) formalism that uses the lambda symbol ( λ {\displaystyle \lambda } ) to denote anonymous function abstraction. In this context, types are usually objects of a [syntactic](/source/Syntax_(logic)) 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](/source/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.[1]

Typed lambda calculi are foundational [programming languages](/source/Programming_languages) and are the base of typed [functional programming languages](/source/Functional_programming_languages) such as [ML](/source/ML_programming_language) and [Haskell](/source/Haskell_(programming_language)) and, more indirectly, typed [imperative programming languages](/source/Imperative_programming). Typed lambda calculi play an important role in the design of [type systems](/source/Type_systems) 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](/source/Mathematical_logic) and [proof theory](/source/Proof_theory) via the [Curry–Howard isomorphism](/source/Curry%E2%80%93Howard_isomorphism) and they can be considered as the [internal language](/source/Internal_language) of certain classes of [categories](/source/Category_theory). For example, the [simply typed lambda calculus](/source/Simply_typed_lambda_calculus) is the language of [Cartesian closed categories](/source/Cartesian_closed_category) (CCCs).[2]

## Kinds of typed lambda calculi

Various typed lambda calculi have been studied. The [simply typed lambda calculus](/source/Simply_typed_lambda_calculus) has only one [type constructor](/source/Type_constructor), the arrow → {\displaystyle \to } , and its only types are [basic types](/source/Basic_type) and [function types](/source/Function_type) σ → τ {\displaystyle \sigma \to \tau } . [System T](/source/Dialectica_interpretation) extends the simply typed lambda calculus with a type of natural numbers and higher-order [primitive recursion](/source/Primitive_recursion); in this system all functions provably [computable](/source/Computable_function) in [Peano arithmetic](/source/Peano_arithmetic) are definable. [System F](/source/System_F) allows [polymorphism](/source/Polymorphism_(computer_science)) by using universal quantification over all types; from a logical perspective it can describe all functions that are provably total in [second-order logic](/source/Second-order_logic). Lambda calculi with [dependent types](/source/Dependent_types) are the base of [intuitionistic type theory](/source/Intuitionistic_type_theory), the [calculus of constructions](/source/Calculus_of_constructions) and the [logical framework](/source/LF_(logical_framework)) (LF), a pure lambda calculus with dependent types. Based on work by Berardi on [pure type systems](/source/Pure_type_system), [Henk Barendregt](/source/Henk_Barendregt) proposed the [lambda cube](/source/Lambda_cube) to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions).[3]

Some typed lambda calculi introduce a notion of *[subtyping](/source/Subtyping)*, i.e. if A {\displaystyle A} is a subtype of B {\displaystyle B} , then all terms of type A {\displaystyle A} also have type B {\displaystyle B} . Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and [System F<:](/source/System_F-sub).

All the systems mentioned so far, with the exception of the untyped lambda calculus, are *[strongly normalizing](/source/Strongly_normalizing)*: all computations terminate. Therefore, they cannot describe all [Turing-computable](/source/Turing-computable) functions.[4] 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](/source/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](/source/Gordon_Plotkin) "[Programming language for Computable Functions](/source/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](/source/Computer_programming), the routines (functions, procedures, methods) of [strongly typed programming languages](/source/Strongly_typed_programming_language) closely correspond to typed lambda expressions.[5]

## See also

- [Kappa calculus](/source/Kappa_calculus)—an analogue of typed lambda calculus which excludes higher-order functions

## Notes

1. **[^](#cite_ref-1)** Brandl, Helmut (27 April 2024). ["Typed Lambda Calculus / Calculus of Constructions"](https://hbr.github.io/Lambda-Calculus/cc-tex/cc.pdf) (PDF). *Calculus of Constructions*. Retrieved 27 April 2024.

1. **[^](#cite_ref-2)** [Lambek, J.](/source/Joachim_Lambek); Scott, P. J. (1986), [*Introduction to Higher Order Categorical Logic*](https://archive.org/details/introductiontohi0000lamb), [Cambridge University Press](/source/Cambridge_University_Press), [ISBN](/source/ISBN_(identifier)) [978-0-521-35653-4](https://en.wikipedia.org/wiki/Special:BookSources/978-0-521-35653-4), [MR](/source/MR_(identifier)) [0856915](https://mathscinet.ams.org/mathscinet-getitem?mr=0856915)

1. **[^](#cite_ref-3)** Barendregt, Henk (1991). ["Introduction to generalized type systems"](https://www.cambridge.org/core/product/identifier/S0956796800020025/type/journal_article). *[Journal of Functional Programming](/source/Journal_of_Functional_Programming)*. **1** (2): 125–154. [doi](/source/Doi_(identifier)):[10.1017/S0956796800020025](https://doi.org/10.1017%2FS0956796800020025). [hdl](/source/Hdl_(identifier)):[2066/17240](https://hdl.handle.net/2066%2F17240). [ISSN](/source/ISSN_(identifier)) [0956-7968](https://search.worldcat.org/issn/0956-7968).

1. **[^](#cite_ref-4)** since the [halting problem](/source/Halting_problem) for the latter class was proven to be [undecidable](/source/Undecidable_problem)

1. **[^](#cite_ref-5)** ["What to know before debating type systems | Ovid \[blogs.perl.org\]"](https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html). *blogs.perl.org*. Retrieved 2024-04-26.

## Further reading

- Barendregt, Henk (1992). ["Lambda Calculi with Types"](https://ftp.science.ru.nl/CSI/CompMath.Found/HBK.ps). In Abramsky, S. (ed.). *Background: Computational Structures*. Handbook of Logic in Computer Science. Vol. 2. Oxford University Press. pp. 117–309. [ISBN](/source/ISBN_(identifier)) [9780198537618](https://en.wikipedia.org/wiki/Special:BookSources/9780198537618).

- Brandl, Helmut (2022). [Calculus of Constructions / Typed Lambda Calculus](https://hbr.github.io/Lambda-Calculus/cc-tex)

---
Adapted from the Wikipedia article [Typed lambda calculus](https://en.wikipedia.org/wiki/Typed_lambda_calculus) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Typed_lambda_calculus?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.