Editing Typed lambda calculus

{{Short description|Formalism in computer science}}
A '''typed [[lambda calculus]]''' is a typed [[formalism (mathematics)|formalism]] that uses the lambda symbol (<math>\lambda</math>) 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.<ref>{{Cite web |last=Brandl |first=Helmut |date=27 April 2024 |title=Typed Lambda Calculus / Calculus of Constructions |url=https://hbr.github.io/Lambda-Calculus/cc-tex/cc.pdf |access-date=27 April 2024 |website=Calculus of Constructions}}</ref>

Typed lambda calculi are foundational [[programming languages]] and are the base of typed [[functional programming languages]] such as [[ML programming language|ML]] and [[Haskell (programming language)|Haskell]] and, more indirectly, typed [[imperative programming|imperative programming languages]]. Typed lambda calculi play an important role in the design of [[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]] and [[proof theory]] via the [[Curry&ndash;Howard isomorphism]] and they can be considered as the [[internal language]] of certain classes of [[category theory|categories]].  For example, the [[simply typed lambda calculus]] is the language of [[cartesian closed category|Cartesian closed categories]] (CCCs).<ref>{{citation | last1=Lambek | first1=J. | last2=Scott | first2=P. J. | title=Introduction to Higher Order Categorical Logic | publisher=[[Cambridge University Press]] | isbn=978-0-521-35653-4 | year=1986 | mr=856915 | url-access=registration | url=https://archive.org/details/introductiontohi0000lamb }}</ref>

== Kinds of typed lambda calculi ==
Various typed lambda calculi have been studied. The [[simply typed lambda calculus]] has only one [[type constructor]], the arrow <math>\to</math>, and its only types are [[basic type]]s and [[function type]]s <math>\sigma\to\tau</math>. [[Dialectica interpretation|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 [[computable function|recursive]] in [[Peano arithmetic]] are definable. [[System F]] allows [[Polymorphism (computer science)|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]]. Lambda calculi with [[dependent types]] are the base of [[intuitionistic type theory]], the [[calculus of constructions]] and the [[LF (logical framework)|logical framework]] (LF), a pure lambda calculus with dependent types. Based on work by Berardi on [[pure type system]]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).<ref>{{Cite journal |last=Barendregt |first=Henk |date=1991 |title=Introduction to generalized type systems |url=https://www.cambridge.org/core/product/identifier/S0956796800020025/type/journal_article |journal=Journal of Functional Programming |language=en |volume=1 |issue=2 |pages=125–154 |doi=10.1017/S0956796800020025 |issn=0956-7968|hdl=2066/17240 |hdl-access=free }}</ref>

Some typed lambda calculi introduce a notion of ''[[subtyping]]'', i.e. if <math>A</math> is a subtype of <math>B</math>, then all terms of type <math>A</math> also have type <math>B</math>. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and [[System F-sub|System F<sub><:</sub>]].

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.<ref>since the [[halting problem]] for the latter class was proven to be [[Undecidable problem|undecidable]]</ref> 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 [[Gordon Plotkin|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]]s closely correspond to typed lambda expressions.<ref>{{Cite web |title=What to know before debating type systems {{!}} Ovid [blogs.perl.org] |url=https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html |access-date=2024-04-26 |website=blogs.perl.org}}</ref>

== See also ==
* [[Kappa calculus]]—an analogue of typed lambda calculus which excludes higher-order functions

== Notes ==
<references />

== Further reading ==
*{{cite book |first=Henk |last=Barendregt |chapter-url= https://ftp.science.ru.nl/CSI/CompMath.Found/HBK.ps <!-- ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps --> |chapter=Lambda Calculi with Types |editor-first=S. |editor-last=Abramsky |title=Background: Computational Structures |series=Handbook of Logic in Computer Science |volume=2 |publisher=Oxford University Press |year=1992 |pages=117–309 |isbn=9780198537618 }}
* Brandl, Helmut (2022). [https://hbr.github.io/Lambda-Calculus/cc-tex Calculus of Constructions / Typed Lambda Calculus]

{{DEFAULTSORT:Typed Lambda Calculus}}
[[Category:Lambda calculus]]
[[Category:Logic in computer science]]
[[Category:Theory of computation]]
[[Category:Type theory]]