Editing Lambda cube (section)

== Subtyping ==
[[Subtyping]] however is not represented in the cube, even though systems like <math>F^\omega_{<:}</math>, known as [[higher-order bounded quantification]], which combines subtyping and polymorphism are of practical interest, and can be further generalized to [[bounded type operator]]s. Further extensions to <math>F^\omega_{<:}</math> allow the definition of [[purely functional objects]]; these systems were generally developed after the lambda cube paper was published.<ref>{{Cite book|title=Types and programming languages|last=Pierce|first=Benjamin|date=2002|publisher=MIT Press|isbn=978-0262162098|pages=467–490|oclc=300712077 }}</ref>

The idea of the cube is due to the mathematician [[Henk Barendregt]] (1991). The framework of [[pure type system]]s generalizes the lambda cube in the sense that all corners of the cube, as well as many other systems can be represented as instances of this general framework.<ref>{{harvnb|Pierce|2002|p=466}}</ref> This framework predates the lambda cube by a couple of years. In his 1991 paper, Barendregt also defines the corners of the cube in this framework.