Typed lambda calculus

<h2 id="kinds-of-typed-lambda-calculi">Kinds of typed lambda calculi</h2>
<p>Various typed lambda calculi have been studied. The <a href="/facts/Simply_typed_lambda_calculus/5RQlXLjy">simply typed lambda calculus</a> has only one <a href="/facts/Type_constructor/4zRCrxUW">type constructor</a>, the arrow 
  
    
      
        →
      
    
    {\displaystyle \to }
  
, and its only types are <a href="/facts/Basic_type/0c898228">basic types</a> and <a href="/facts/Function_type/CmbusBzk">function types</a> 
  
    
      
        σ
        →
        τ
      
    
    {\displaystyle \sigma \to \tau }
  
. <a href="/facts/Dialectica_interpretation/WPfbFVmL">System T</a> extends the simply typed lambda calculus with a type of natural numbers and higher-order <a href="/facts/Primitive_recursion/4z97gRnl">primitive recursion</a>; in this system all functions provably <a href="/facts/Computable_function/dzwBlLGn">recursive</a> in <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a> are definable. <a href="/facts/System_F/odpwVpAG">System F</a> allows <a href="/facts/Polymorphism_(computer_science)/S3cCKsVT">polymorphism</a> by using universal quantification over all types; from a logical perspective it can describe all functions that are provably total in <a href="/facts/Second-order_logic/C138cGXQ">second-order logic</a>. Lambda calculi with <a href="/facts/Dependent_types/wCeQI7ds">dependent types</a> are the base of <a href="/facts/Intuitionistic_type_theory/qwkrpKlP">intuitionistic type theory</a>, the <a href="/facts/Calculus_of_constructions/whAjbfWY">calculus of constructions</a> and the <a href="/facts/LF_(logical_framework)/bVGxB8Lk">logical framework</a> (LF), a pure lambda calculus with dependent types. Based on work by Berardi on <a href="/facts/Pure_type_system/045wJpGU">pure type systems</a>, <a href="/facts/Henk_Barendregt/jmvltEQ6">Henk Barendregt</a> proposed the <a href="/facts/Lambda_cube/tSR2laCs">Lambda cube</a> to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions).<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a>
</p><p>Some typed lambda calculi introduce a notion of <i><a href="/facts/Subtyping/0L9t8twv">subtyping</a></i>, 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 <a href="/facts/System_F-sub/sJ73ej8w">System F<:</a>.
</p><p>All the systems mentioned so far, with the exception of the untyped lambda calculus, are <i><a href="/facts/Strongly_normalizing/eV9G3veH">strongly normalizing</a></i>: all computations terminate. Therefore, they cannot describe all <a href="/facts/Turing-computable/dzwBlLGn">Turing-computable</a> functions.<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> 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 <a href="/facts/Girard%27s_paradox/GY82oxvG">Girard's paradox</a>. This system is also the simplest pure type system, a formalism which generalizes the Lambda cube. Systems with explicit recursion combinators, such as <a href="/facts/Gordon_Plotkin/2CrnVkVj">Plotkin's</a> "<a href="/facts/Programming_language_for_Computable_Functions/X9oXdkSK">Programming language for Computable Functions</a>" (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.
</p>
<h2 id="applications-to-programming-languages">Applications to programming languages</h2>
<p>In <a href="/facts/Computer_programming/QmSsFnu0">computer programming</a>, the routines (functions, procedures, methods) of <a href="/facts/Strongly_typed_programming_language/WYexudnr">strongly typed programming languages</a> closely correspond to typed lambda expressions.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a>
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Kappa_calculus/q6THpbqo">Kappa calculus</a>—an analogue of typed lambda calculus which excludes higher-order functions</li></ul>
<h2 id="notes">Notes</h2>

<h2 id="further-reading">Further reading</h2>
<ul><li>Barendregt, Henk (1992). <a href="https://ftp.science.ru.nl/CSI/CompMath.Found/HBK.ps">"Lambda Calculi with Types"</a>. In Abramsky, S. (ed.). <i>Background: Computational Structures</i>. Handbook of Logic in Computer Science. Vol. 2. Oxford University Press. pp. 117–309. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780198537618.</li>
<li>Brandl, Helmut (2022). <a href="https://hbr.github.io/Lambda-Calculus/cc-tex">Calculus of Constructions / Typed Lambda Calculus</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Brandl, Helmut (27 April 2024). "Typed Lambda Calculus / Calculus of Constructions" (PDF). Calculus of Constructions. Retrieved 27 April 2024. <a href="https://hbr.github.io/Lambda-Calculus/cc-tex/cc.pdf" target="_blank">https://hbr.github.io/Lambda-Calculus/cc-tex/cc.pdf</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>Lambek, J.; Scott, P. J. (1986), Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 978-0-521-35653-4, MR 0856915 <a href="978-0-521-35653-4" target="_blank">978-0-521-35653-4</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Barendregt, Henk (1991). "Introduction to generalized type systems". Journal of Functional Programming. 1 (2): 125–154. doi:10.1017/S0956796800020025. hdl:2066/17240. ISSN 0956-7968. <a href="https://www.cambridge.org/core/product/identifier/S0956796800020025/type/journal_article" target="_blank">https://www.cambridge.org/core/product/identifier/S0956796800020025/type/journal_article</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
<li id="fn:4"><p>since the halting problem for the latter class was proven to be undecidable <a href="/wiki/Halting_problem" target="_blank">/wiki/Halting_problem</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li>
<li id="fn:5"><p>"What to know before debating type systems | Ovid [blogs.perl.org]". blogs.perl.org. Retrieved 2024-04-26. <a href="https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html" target="_blank">https://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li>
</ol>

Typed lambda calculus open-in-new

Typed lambda calculus