Editing System F (section)

== System F<sub>ω</sub> ==
While System F corresponds to the first axis of [[Henk Barendregt|Barendregt's]] [[lambda cube]], '''System F<sub>ω</sub>''' or the '''higher-order polymorphic lambda calculus''' combines the first axis (polymorphism) with the second axis ([[type operator]]s); it is a different, more complex system.

System F<sub>ω</sub> can be defined inductively on a family of systems, where induction is based on the [[Kind (type theory)|kind]]s permitted in each system:

* <math>F_n</math> permits kinds:
** <math>\star</math> (the kind of types) and
** <math>J\Rightarrow K</math> where <math>J\in F_{n-1}</math> and <math>K\in F_n</math> (the kind of functions from types to types, where the argument type is of a lower order)

In the limit, we can define system <math>F_\omega</math> to be

* <math>F_\omega = \underset{1 \leq i}{\bigcup} F_i</math>

That is, F<sub>ω</sub> is the system which allows functions from types to types where the argument (and result) may be of any order.

Note that although F<sub>ω</sub> places no restrictions on the ''order'' of the arguments in these mappings, it does restrict the ''universe'' of the arguments for these mappings: they must be types rather than values.  System F<sub>ω</sub> does not permit mappings from values to types ([[dependent types]]), though it does permit mappings from values to values (<math>\lambda</math> abstraction), mappings from types to values (<math>\Lambda</math> abstraction), and mappings from types to types (<math>\lambda</math> abstraction at the level of types).