Inductive type classes and large types

The types defined so far belong to an inductively defined collection according to the scheme for $T\ is\_a\ type$ in the last section. Let U₁ denote this inductively defined collection of types; it has the characteristic of a type in that it has elements and is structured. Evaluation is defined on the elements, e.g.  ${{\mathbb{N} }}\ evals\_to\ {{\mathbb{N} }}$, $({{\mathbb{N} }}\times {{\mathbb{N} }})\ evals\_to\ ({{\mathbb{N} }}\times {{\mathbb{N} }})$, etc. So all of the elements are canonical and are built up inductively themselves. In this regard U₁ resembles ${{\mathbb{N} }}$. It has all the properties of a type.

We want to make U₁ a type. So we add rules for its elements in terms of equalities. For example, there are rules $\mathbf{0} = \mathbf{0}\ \mbox{in}\ U_1$ and

$$\frac{A = A'\ \mbox{in}\ U_1\ \ \ B = B'\ \mbox{in}\ U_1}{A \times B = A' \times B'\ \mbox{in}\ U_1}$$

The equality rules we have in mind are these

$${{\mathbb{N} }}={{\mathbb{N} }}\ \mbox{in}\ U_1\ \ \ \mathbf{... ...}\ \mbox{in}\ U_1\ \ \ \mathbf{1}=\mathbf{1}\ \mbox{in}\ U_1$$

A=A' in U₁ B=B'    in U₁

    $(A \times B) = (A' \times B')$     in U₁

    $list(A) = list(A')\ \$       in U₁

    $(A\rightarrow B) = (A' \rightarrow B')$   in U₁

    (A+B) = (A'+B')     in U₁

This is a structural or intensional equality (used in both Nuprl and [80]). It turns out that this equality is also extensional since A=Bin U₁ iff $a \in A$ implies $a \in B$ and conversely. This is the only type so far whose elements are types, but it does not include all types, in particular U₁ is not in U₁ according to our semantics.

We have no way to prove that U₁ is not in U₁. We don't even have a way to say this. But it would be possible to add a recursion combinator on U₁ that expressed the idea that U₁is the least type closed under these operations. The combinator would have the form of a primitive recursive definition

	f(, x) = b0(x)
	f(1, x)=b1(x)
	f(N, x)=b2(x)
	$f((A \times B), x)=h_1(A, B, f(A, x), f(B, x))$
	$\vdots$
	f((A+B), x)=h4(A, B, f(A, x), f(B, x))

With this form of recursion and the corresponding induction rule we could prove that every element of U₁ was either 0, 1, N, a product, a union, etc.

Once we can regard types as elements of a type like U₁, then we can extend our methods for building objects, say over ${{\mathbb{N} }}$ or by case analysis over a type of Booleans, say ${{\mathbb{B} }}$ etc. to building types. Here are two examples, taking ${{\mathbb{B} }}$ as an abbreviation of 1 + 1 and abbreviating $inl(\bullet)$ as tt and $inr(\bullet)$ as $f\!f$.

Let T(tt)=A, T(ff)=B, then $\lambda(x. T(x))$ is a function ${{\mathbb{B} }} \rightarrow U_1$. If we build a generalization of ${{\mathbb{B} }}$ to n distinct values, say ${{\mathbb{B} }}_n = ((\mathbf{1}+\mathbf{1})+\cdots +\mathbf{1})$ n times defined by ${{\mathbb{B} }}= \mathbf{1}, {{\mathbb{B} }}(suc(n))={{\mathbb{B} }}(n)+\mathbf{1}$ with elements $1_b, \ldots, n_b$, then we can build a function T(x) selecting n types, T(i_b).

It is worth thinking harder about functions like $T:{{\mathbb{B} }}_n \rightarrow U_1$. This is an indexed collection of types, $\{T(1_b), \cdots, T(n_b)\}$. We can imagine putting them together to form types in various ways, for instance by products or unions or functions

	$T(1_b) \times \cdots \times T(n_b)$ or
	$T(1_b) + \cdots + T(n_b)$ or
	$T(1_b) \rightarrow \cdots \rightarrow T(n_b).$

We could define these types recursively, say by functions $\Pi$, $\Sigma$ and $\Theta$ if we could have inputs like this: m in ${{\mathbb{N} }}$, T in ${{\mathbb{B} }}_m \rightarrow U_1$,

	$\Pi_m(0)(T)=T(i_m(1))$
	$\Pi_m(n)(T)=\Pi_m(n-1)(T) \times T(i_m(suc(n)))$

where i_m(k) selects the k-th constant of ${{\mathbb{B} }}_n$, k_b.³¹ Likewise for $\Sigma$ and $\Theta$. However, we are unable to type these functions $\Pi, \Sigma, \Theta$ with the current type constructors. We could type them with the new ones we are trying to define!

In the case of $\Pi$ and $\Sigma$ the operations make sense even for infinite families of types, say indexed by $T \in A \rightarrow U_1$for any type A. We can think of $\Pi$ over $T \in A \rightarrow U_1$ as functions f such that on input $a \in A$, we have $f(a) \in T(a)$. For $\Sigma$ over $T \in A \rightarrow U_1$ we can use the elements a as ``tags'' so that elements are pairs $\langle a, t\rangle$where $t \in T(a)$.

These ideas give rise to two new type constructors, $\Pi$ and $\Sigma$over an indexed family of types $T \in A \rightarrow U_1$. We write the new constructors as $\Pi(A; T)$ and $\Sigma(A; T)$. We could use typing rules like these

5(160,80) $\frac{\textstyle A \in U_1\ \ \ \ \ T \in A \rightarrow U_1} {\stackrel{\textstyle \Pi(A; T) \in U_1} {\textstyle \Sigma(A; T) \in U_1}}$

5(250,80) $\frac{\textstyle x \in A \vdash f\in T(x)}{\textstyle \lambda(x.f) \in \Pi(A;... ...\vdash a \in A\ \ \ \vdash b \in T(a)}{\textstyle pair(a; b) \in \Sigma(A; T)}$

The dotted lines forming the box indicate that this is an exploratory rule which will be supplanted later. We treat $\lambda(x.f)$ and pair(a; b) just as before, so we are not adding new elements to the theory, just new ways to type existing ones.

With $\Pi$ and $\Sigma$ and using induction over ${{\mathbb{N} }}$ we can build types that are not in this U₁. For example, let $f(0)=A, f(suc(n))=A \times f(n)$. Then f is a function ${{\mathbb{N} }} \rightarrow U_1$ where $f(n)=A \times \cdots \times A$ taken n times. The actual function is $\lambda(n. R(n; A; u, t. A \times t))$. Now we can build types like $\Sigma(N; \lambda(n. R(n; A; u, t. A \times t)))$ and $\Pi(A; \lambda(n. R(n; A; u, t. A \times t)))$ which are not in U₁. We could imagine trying to enlarge the inductive type class U₁ by adding these operators to the inductive definition. We will take up this topic in the next section.