- Usual records and tuples can be modelled with
Cartesian product types. They are composed of components
which can be independently selected.
- Dependent types offers a Generalization to dependent products where the
type of one component depends on the value of another,
(a : A)×B(a).
- Functions may return results whose type depends on
the value of their arguments.
mod: (Integer, m: Integer) -> IntegerMod(m)
- If types can be used as values, then dependent types become
very natural for generic programming.
identity: (n: Integer, R: Ring) -> Matrix(n, n, R)
- Parametric polymorphism.
commutator(R: Ring)(p: R, q: R): R == p*q - q*p;