2
$\begingroup$

I'm gathering examples from everything that I've read about Dependent Type Theory mainly from Dependent types at Work paper.

This is my list so far of some dependent types (with abbreviations of mine):

  • [NVec]: $A^n$ vectors of length n with elements of type $A$
  • [NMMAtrix]: $A^{m\times n}$ matrices
  • [Fin]: Finite sets of size $n$
  • [SList]: Sorted lists
  • [NBTree]: Height-balanced trees of a certain height
  • [SBTree]: Sorted binary trees
  • [PAIR]: A pair of integers where the second is greater than the first

How can I justify that the types from my list are indeed dependent types. I appreciate another example to add it to my list.

$\endgroup$
7
$\begingroup$

I think it helps to keep in mind the propositions as types mantra. Every type can be read either as a propostion or a set. This gives us two readings (let's just consider types dependent on natural numbers):

  1. A dependent type $P : \mathtt{nat} \to \mathtt{Type}$ is like a family of sets $P(0), P(1), P(2), \ldots$
  2. A dependent type $P : \mathtt{nat} \to \mathtt{Type}$ is a property of natural numbers where we think of $P(n)$ as the proofs that $n$ has property $P$

With this in mind it may be easier to make sense of dependent types. For instance, consider:

  • $\mathtt{Mat}(n)$: the type of matrices of size $n \times n$
  • $\mathtt{Less}(a,b)$: the proofs that $a < b$

Then $\mathtt{Mat}(n)$ should be thought of as a collection of sets, one for each $n$, while $\mathtt{Less}(a,b)$ is a relation (a binary predicate) on pairs $(a,b)$.

Your first three examples (NVec, NMMatrix, Fin) are dependen types of the first kind. The other ones are of the second kind.

Strictly speaking, when you say "a pair of integers where teh second is greater than the first", that is not a dependent type but an element of the dependent sum, i.e,

$$\mathtt{PAIR} = \textstyle\sum_{(a,b) : \mathtt{nat} \times \mathtt{nat}} \mathtt{Less}(a,b),$$

i.e., a triple $(a, b, p)$ where $p$ is a proof that $a < b$. Similarly, your NBtree and SBTree examples are really dependent sums of the form $\sum_{t : \mathtt{Tree}} P(t)$, not dependent types. The sums of course use dependent types $P(t) = \text{"proofs that the tree $t$ is height-balanced"}$ and $P(t) = \text{"proofs that the tree $t$ is sorted"}$.

$\endgroup$
  • $\begingroup$ Thanks, I've been reading your answer more than once, It helps me to understand a lot. I don't understand well about dependent sums. Can I say that a dependent type is either of the first kind or the second kind but not of both? $\endgroup$ – jonaprieto Apr 23 '16 at 7:36
  • $\begingroup$ The difference between a dependent type $P : A \to \mathsf{Type}$ and the dependent sum $\sum_{x : A} P(x)$ is the same as the difference between a sequence of numbers $p_0, p_1, p_2, \ldots$ and its sum $\sum_{i \in \mathbb{N}} p_i$. $\endgroup$ – Andrej Bauer Apr 23 '16 at 18:50
  • 2
    $\begingroup$ The idea that types describe objects or proofs of propositions is part of an explanation of what types are good for and how to create a mental picture of what is going on. It is entirely up to you to create your own mental picture. You can find types that have a double reading, and some that have none. The math and the types themselves do not care how we look at them. So, all this talk about two kinds of dependent types is just a pedagogical device. $\endgroup$ – Andrej Bauer Apr 23 '16 at 18:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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