# Dependent type

(from `Dependent Types at Work` by Ana Bove, Peter Dybjer, 2008)

> A dependent type is a type that depends on elements of other type(s). A dependent type is a _family of types indexed by the **terms** of another type_. On the other hand, a _parametrised type_ is a family of types _indexed by another type_.

The canonical example of a dependent type is the type `Aⁿ` of vectors of length `n` with components of type `A`. We say that the type `Aⁿ` depends on the number `n`, or that `Aⁿ` is a family of types indexed by the number `n`.

Parametrised types, such as the list type `[A]` with elements of type `A`, are usually not called dependent types. They are families of types indexed by other types, not families of types indexed by elements of another type. However, in dependent type theories there is a type of small types (universe), so that we might have a type `[A]` of lists of elements of a given small type `A`.

The strong type system and the support for dependent types in Agda (an extension of Martin-Lof type theory) permit us to express, more or less, any conceivable dependent property. We have to say "more or less" because Godel's incompleteness theorem sets a limit for the expressiveness of logical languages.

The simply typed lambda calculus and the Hindley-Milner type system, on which typed functional programming languages such as ML and Haskell are based, do not include dependent types, only parametrised types. Similarly, the polymorphic lambda calculus `System F` has types like `∀X.A` where `X` ranges over all types, but no quantification over elements of other types.

The modern development of dependently typed programming languages has its origins in the CHI between propositions and types. There is a one-to-one correspondence between combinatory terms and proofs in implicational logic. In a similar way, product types correspond to conjunctions, and sum types (disjoint unions) to disjunctions.

To extend this correspondence to predicate logic, Howard and de Bruijn introduced dependent types `A(x)` corresponding to predicates `P(x)`. They formed indexed products `Πx : D.A(x)` and indexed sums `Σx : D.A(x)` corresponding, respectively, to universal quantifications `∀x : D.P(x)` and existential quantifications `∃x : D.P(x)`.

`Πx : D.A(x)` \~ `∀x : D.P(x)`\
`Σx : D.A(x)` \~ `∃x : D.P(x)`

What we obtain here is a Curry-Howard interpretation of intuitionistic predicate logic (IPL). There is a one-to-one correspondence between propositions and types in a type system with dependent types. There is also a one-to-one correspondence between proofs of a certain proposition in constructive predicate logic and terms of the corresponding type. Furthermore, to accommodate equality in predicate logic, we introduce the type `a == b` of proofs that `a` and `b` are equal. In this way, we get a Curry-Howard interpretation of predicate logic with equality. We can go even further and add the type of natural numbers with addition and multiplication, and get a Curry-Howard version of Heyting (intuitionistic) arithmetic.

The CHI was the basis for _Martin-Lof's intuitionistic type theory_, where the propositions and types are actually identified. Although Martin-Lof's theory was primarily intended to be a foundational system for constructive mathematics, it can also be used as a programming language.

From the early 1980's and onwards, a number of computer systems implementing variants of Martin-Lof type theory were built. The most well-known are the `NuPRL` system from Cornell, implementing an _extensional version_ of the theory, and the `Coq` system from INRIA in France, implementing an _intensional impredicative version_. The `Agda` system implements an _intensional predicative extension of Martin-Lof type theory_. It is the latest in a sequence of systems developed in Goteborg.

Systems implementing dependent type theories are often referred to as either _proof assistants_ or _dependently typed PL_, depending on whether the emphasis is on proving or on programming. `Agda` is primarily designed to be a PL, although it can be used as a proof assistant as well. It extends Martin Lof type theory with a number of features, such as flexible mechanisms for defining new inductive data types and for defining functions by pattern matching.
