# Indexing a dependent type on a value?

If i'm recalling from Robert Harper's lectures Homotopy type theory A dependent type is a family of type index by a type. If we allow index to be just a value can we gain something instead of allowing to be a type ?

Is that the same thing they did in DML?

Wikipedia definition states in this regards :

A dependent type is a type whose definition depends on a value.

If i have a specification stating : "list of Strings" rather than " a List of Strings of n length", are't i'm still stating something about the value ? Is this definition enough to distinguish dependent types ? thanks

## 1 Answer

The best answer I can give is that you are confused about the meaning of words. I tried to explain this already in another answer to you, so let me be more explicit this time.

To say

type $A$ indexed by type $B$

and

type $A$ indexed by values of type $B$

is the same thing. People say both of these to mean one and the same thing.

The important thing is to think of $A$ as a function with domain $B$ and codomain $\mathsf{Type}$ (the "type of all types" or a "universe of types"). So, whatever people say and however you are getting confused about "value" vs. "type" here, a dependent type is a function from a type (the indexing type) to the universe of types. Thus:

A dependent type $A$ indexed by $B$ has as its domain the type $B$, therefore it takes as inputs values of type $B$.

You cannot index a dependent type by just a single value, that makes no sense. That would be like saying "the dependent type of lists of length 7". That is not dependent on anything because "7" is fixed. If you say "the dependent type of lists of length $n : \mathsf{nat}$" that is the same thing as saying "the dependent type of lists whose length is indexed by type $\mathsf{nat}$". Here $n$ is not fixed, it is just a sloppy way of introducing an unecessary variable. To be less sloppy, you would have to say "the dependent type which, for any $n : \mathsf{nat}$, gives the lists of length $n$". This is more correct because it explains that the dependent type is a function taking any $n$ to a type.

I hope that helps.

Just to be sure, let me also say explicitly that in set theory and ordinary mathematics the domain of a function is a set (and not an element of a set). Is that clear?

• Glad to help. You see that little checkmark next to the answer? Try what happens if you click on it. – Andrej Bauer Apr 10 '16 at 0:06
• Is that radioActive ? – Pushpa Apr 10 '16 at 5:34
• Nope, but it gets you brownie points in the computer science heaven. – Andrej Bauer Apr 10 '16 at 8:32
• I'm surely going to Computer science Hell so yeah , click ! – Pushpa Apr 10 '16 at 8:43
• I am not sure I understand you, but presumably you are talking about a dependent type which is indexed by a universe. – Andrej Bauer Apr 10 '16 at 22:49