Lambda cube

In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus (written as λ→ in the cube diagram to the right) as the vertex of a cube placed at the origin, and the calculus of constructions (higher-order dependently typed polymorphic lambda calculus; written as λPω in the diagram) as its diametrically opposite vertex. Each axis of the cube represents a new form of abstraction:

All eight calculi include the most basic form of abstraction, values depending on values, ordinary functions as in the simply typed lambda calculus. The richest calculus in the cube, with all three abstractions, is the calculus of constructions. All eight calculi are strongly normalizing.

Subtyping however is not represented in the cube, even though systems like ${\displaystyle F_{<:}^{\omega }}$, known as higher-order bounded quantification, which combines subtyping and polymorphism are of practical interest, and can be further generalized to bounded type operators. Further extensions to ${\displaystyle F_{<:}^{\omega }}$ allow the definition of purely functional objects; these systems were generally developed after the lambda cube paper was published.

...
Wikipedia