Dependent types are functions whose type depends on a value. This comes in two forms:

  • the dependent product (∏, Pi) whose return type is dependent on the argument

  • the dependent sum (∑, Sigma) whose argument type depends on the value of the first argument

Dependent Product

The dependent product generalises Arrow Types. An example of the dependent product would be a function which, given a Natural number n, returns an array of Integers of size n. This is written:

∏ n: Natural . Array(Integer, n)

where the return type is not dependent on the value of an argument, then it simplifies to the Arrow Type, ∏ x: A . B, usually written A → B, the subset of the cartesian product.

Dependent Sum

This types generalises the cartesian product where the type of the second component depends on the first. To find the length of an array we might define:

∑ n: Natural . Array(Integer, n) → singleton(n)

where singleton(n) is the Singleton Type.


Many programming languages have workarounds for not supporting depedent types. This can appear as partial functions, metaprogramming and exceptions. Dependent types allow arbitrary functions to describe a type, this makes type checking as hard as full program verification. This is why dependent types are usually only found in languages used in program verification. Due to Goedel’s incompleteness theorem, not all functions can be known to be either true or false.


comments powered by Disqus