- 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;

2003-06-06