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
up vote 5 down vote accepted

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)}$

Your Answer

 

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.