Editing Lambda cube (section)

== Examples of Systems ==

=== (λ→) Simply typed lambda calculus ===

The simplest system found in the λ-cube is the [[simply typed lambda calculus]], also called λ→. In this system, the only way to construct an abstraction is by making ''a term depend on a term'', with the [[typing rule]]:

<math>\frac{\Gamma, x : \sigma \;\vdash\; t : \tau}{\Gamma \;\vdash\; \lambda x . t : \sigma \to \tau}</math>

=== (λ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>.

=== (λ<u>ω</u>) System F<u>ω</u> ===

In System F<math>\underline{\omega}</math> a construction is introduced to supply ''types that depend on other types''. This is called a [[type constructor]] and provides a way to build "a function with a type as a ''value''".<ref>{{harvnb|Nederpelt|Geuvers|2014|p=85}}</ref> An example of such a type constructor is the type of binary trees with leaves labeled by data of a given type <math>A</math>: <math>\mathsf{TREE} := \lambda A : * . \Pi B . (A \to B) \to (B \to B \to B) \to B</math>, where "<math>A:*</math>" informally means "<math>A</math> is a type". This is a function that takes a type parameter <math>A</math> as an argument and returns the type of <math>\mathsf{TREE}</math>s of values of type <math>A</math>. In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives. The previous type constructor roughly corresponds to the following definition of a tree with labeled leaves in OCaml:<syntaxhighlight lang="ocaml">
type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree
</syntaxhighlight>

This type constructor can be applied to other types to obtain new types. E.g., to obtain type of trees of integers:<syntaxhighlight lang="ocaml">type int_tree = int tree</syntaxhighlight>

System F<math>\underline{\omega}</math> is generally not used on its own, but is useful to isolate the independent feature of type constructors.<ref>{{harvnb|Nederpelt|Geuvers|2014|p=100}}</ref>

=== (λP) Lambda-P ===
In the [[λΠ-calculus|λP]] system, also named λΠ, and closely related to the [[Logical framework#LF|LF Logical Framework]], one has so called [[dependent types]]. These are ''types that are allowed to depend on terms''. The crucial introduction rule of the system is

<math>\frac{\Gamma, x : A \;\vdash\; B : *}{\Gamma \;\vdash\; (\Pi x : A . B) : *}</math>

where <math>*</math> represents valid types. The new type constructor <math>\Pi</math> corresponds via the [[Curry Howard isomorphism|Curry-Howard isomorphism]] to a universal quantifier, and the system λP as a whole corresponds to [[first-order logic]] with implication as only connective. An example of these dependent types in concrete programming is the type of vectors on a certain length: the length is a term, on which the type depends.

=== (λω) System Fω ===
[[System F-omega|System Fω]] combines both the <math>\Lambda</math> constructor of System F and the type constructors from System F<math>\underline{\omega}</math>. Thus System Fω provides both ''terms that depend on types'' and ''types that depend on types''.

=== (λC) Calculus of constructions ===
In the [[calculus of constructions]], denoted as λC in the cube or as λPω,<ref name=:0/>{{rp|130}} these four features cohabit, so that both types and terms can depend on types and terms. The clear border that exists in λ→ between terms and types is somewhat abolished, as all types except the universal <math>\square</math> are themselves terms with a type.