Dependent types

dependent type The construction of $\Pi$ and $\Sigma$ types over U₁ suggests something more expressive. Instead of limiting the dependent constructions to functions from $T \in A \rightarrow U_1$, we could allow dependency whenever we can form a type expression B[x] that is meaningful for all x of type A. We are led to consider a rule of the form

$\vdash A \in U_1\ \ \ \ \ x:A \vdash B[x] \in U_1$

        $f\!un(A; x.B) \in U_1$

        $prod(A; x. B) \in U_1$

We call fun a dependent functiondependent function constructor and prod a dependent product dependent product.³² We adopt a different notation from $\Pi$ and $\Sigma$ to suggest the more fundamental character of the construction. If we have $T \in A \rightarrow U_1$, then $\Pi(A; T)$ is the same as $f\!un(A; x.T(x))$ and $\Sigma(A; T)$ is the same as prod(A; x.T(x)). But now we can iterate the construction without going beyond U₁. That is, we postulate that U₁ is closed under dependent functions and products.

This conception of $\Pi$ and $\Sigma$ is reminiscent of the collection axiom in set theory. For example, in ZF if R(x, y) is a single-valued relation on sets, then we can form $\{y\: \vert\: \exists x \in A. R(x, y)\}$. Another way to think of collection is to have a function $f:A \rightarrow Set$ where $A \in Set$ and postulate the existence of the set $\{f(x)\: \vert\: x \in A\}$.

The similarity between collection and these rules is that we can consider B in $f\!un(A; x.B)$ to define a function $\lambda(x.B)$from A into U₁. With the addition of dependent types, the intuitive model becomes more complex. What assurance can we offer that the theory is still consistent, e.g. that we can't derive 0=1in N or that we derive $t \in T$ but evaluation of t fails to terminate? Can we continue to understand the model inductively? If we can build an inductive model of U₁ then we can be assured of not only consistency but of a constructive explanation. We answer these questions next.