Polymorphism — terms depend on types
Type operators — types depend on types
Dependent types — types depend on terms
λ→
Simply typed λ-calculus
The dependency table (what the cube is made of)
Ordinary programming is terms depending on terms. The three cube axes are the other three cells: which things are allowed to depend on which.
| …depends on a term | …depends on a type | |
|---|---|---|
| A term… |
Always on
Functions: f (x : A) : B
|
Polymorphism
Terms bind types: id {α} (x : α)
|
| A type… |
Dependent types
Types bind terms: Vec α n
|
Type operators
Types bind types: F : Type → Type
|
What you can express here
The gain along each active axis
Lean sketch (illustrative — not always valid Lean 4)