Editing Lambda cube (section)

=== (λ2) System F ===
In [[System F]] (also named λ2 for the "second-order typed lambda calculus")<ref>{{cite book |last1=Nederpelt |first1=Rob |last2=Geuvers |first2=Herman |title=Type Theory and Formal Proof |date=2014 |publisher=Cambridge University Press |isbn=9781107036505 |page=69 |url=https://www.cambridge.org/vi/academic/subjects/computer-science/programming-languages-and-applied-logic/type-theory-and-formal-proof-introduction?format=HB }}</ref> there is another type of abstraction, written with a <math>\Lambda</math>, that allows ''terms to depend on types'', with the following rule:

<math>\frac{\Gamma \;\vdash\; t : \sigma}{\Gamma \;\vdash\; \Lambda \alpha . t : \Pi \alpha . \sigma} \;\text{ if } \alpha\text{ does not occur free in }\Gamma</math>

The terms beginning with a <math>\Lambda</math> are called [[Parametric polymorphism|polymorphic]], as they can be applied to different types to get different functions, similarly to polymorphic functions in [[ML (programming language)|ML-like languages]]. For instance, the polymorphic identity <syntaxhighlight lang="ocaml">
fun x -> x
</syntaxhighlight>of [[OCaml]] has type <syntaxhighlight lang="ocaml">
'a -> 'a
</syntaxhighlight>meaning it can take an argument of any type <code>'a</code> and return an element of that type. This type corresponds in λ2 to the type <math>\Pi \alpha . \alpha \to \alpha</math>.