Dependent Types

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