# Basic Definition of Dependent Types?

I'm looking at the wikipedia page for Dependent Types and I am getting stuck trying to understand the definition.

It says,

... given a type $A:U$ in a universe of types $U$, one may have a family of types $B:A\rightarrow U$ which [sic] assigns to each term $a:A$ a type $B(a):U$.

So far, so good. I read from this that a "family of types" $B$ is an ordinary function from a type $A$ to a universe of types $U$, and I deduce that the members $a$ of a type $A$ are called "terms." I get horked on the next sentence:

A function whose codomain varies depending on its argument is a dependent function, ...

As I read it, $B$ cannot be such a function because its codomain $U$ does not vary depending on its argument. The value of $B(a)$, of course, varies depending on its argument $a$, but not the codomain of $B$, which is always the same universe $U$. Perhaps the writer means that the value $B(a)$ at input $a$ is, in turn, the "function whose codomain varies depending on its argument." If so, then $B(a)=u$ is a function whose codomain varies depending on its argument, and that would mean that each type $u$ in $U$ is a function whose codomain varies depending on its argument, but now I'm lost, because I don't know enough about types, in general, to complete the thought.

• I found a nice clarifying example here goo.gl/oNjtuc: the type of vectors of length $n$, with components of type $A$, is a dependent type. The type is different for each $n$, i.e., 2-vectors are of a different type to 3-vectors, etc. Relating, then, to the definition above, the type $A(n)$ is a dependent type. I would write $B:A\times Z\rightarrow U$. – Reb.Cabin Jan 25 '15 at 17:52

The article is trying to explain the notion of a dependent product, but the passage you quote is not very precise. To use set-theoretic terms, if $A$ is a set and $B$ is a set-valued function on $A$, the dependent product: $$\prod_{x:A} B(x)$$ denotes the set of all functions $f: A \rightarrow U$, where $U$ is the union of the sets $B(x)$, such that for each $x \in A$, $f(x) \in B(x)$. A member of the dependent product, which the wikipedia article calls a dependent function, is a function equipped with a fine-grained description of its codomain giving a "bound" $B(x)$ on the value of $f(x)$ for each $x$ in its domain.

• If I were to put the vectors example in these terms, then (correct me if I'm wrong), let $A=N$ the set of Naturals (including zero), and $B$ be the set-valued function that assigns to each $n\in N$ the vector space $F^n$, where $F$ denotes some field underlying all the vector spaces. $\Pi B(n)$ would be the set of all functions $f:N\rightarrow V=\cup \{F^0, F^1, ...\}$ such that for each $n\in N$, $f(n)\in B(n)$. Makes sense to me. – Reb.Cabin Jan 25 '15 at 18:30
• @Reb.Cabin: yes, that's exactly right: a function in that dependent type would map each natural number $n$ to an $n$-vector over $F$. – Rob Arthan Jan 25 '15 at 19:08
• The field $F$ is a free variable in the values of $B(n)$ and $\Pi B(n)$; this might be what @Hanno was getting at. Also, I am not sure that including $F^0$ is right. I can imagine a $0$-dimensional vector space containing only $()$, a vector of no components, therefore being linear over any field, that is, such that $\mu () = (\mu * \textrm{nothing}) = (), \mu\in F, \forall F$. Hardly useful whether right or wrong, so this is a small point. – Reb.Cabin Jan 25 '15 at 22:05

I'm not an expert in type theory, but I agree that the Wikipedia article does not separate the different notions very clearly, at least as far as I understand things.

First, there is the notion of a dependent type, which is a type expression involving free variables from other types. Given such a type expression $t$ involving a free variable $a$ of type $A$, one may - if the type system allows that - form the $\lambda$-abstraction $\lambda _{a:A}.t$, which is a type valued function on $A$, i.e. a term of type $A\to U$ with $U$ the universe of types. Conversely, a type valued function $B: A\to U$ on $A$, $B a$ is a dependent type with free variable $a$ of type $A$.

If a dependent type $t$ involving a parameter $a:A$ is given, its dependent product type $\prod_{a:A} t$ is another type which has as its terms the $\lambda$-abstractions of terms which have type $t$ in context $a:A$, and these can be understood as dependent functions with their codomain varying depending on the argument. So:

$\left[\text{(dependent type)}\leftrightarrow\text{(type valued function)}\right]\leadsto\text{(dependent product type)}\ni\text{(dependent functions)}$