Editing Lambda cube (section)

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