Lambda cube

The Lambda Cube is a way of describing 8 different systems of the typed lambda calculus depending on how powerful they are. The “edges” on the cube correspond to a different construct (which is 3 different constructs, hence, cube). These are

1. Term polymorphism, Type -> Term (macros)
2. Type polymorphism, Type -> Type (generics)
3. Dependent types, Term -> Type (predicates)