patternMinor
Examples of Dependent Types
Viewed 0 times
dependentexamplestypes
Problem
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):
How can I justify that the types from my list are indeed dependent types.
I appreciate another example to add it to my list.
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.
Solution
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):
With this in mind it may be easier to make sense of dependent types. For instance, consider:
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"}$.
- A dependent type $P : \mathtt{nat} \to \mathtt{Type}$ is like a family of sets $P(0), P(1), P(2), \ldots$
- 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
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"}$.
Context
StackExchange Computer Science Q#56283, answer score: 9
Revisions (0)
No revisions yet.