Introduction to Dependent Types

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.

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.