5.3 W-types

Inductive types are very general, which is excellent for their usefulness and applicability, but makes them difficult to study as a whole.Fortunately, they can all be formally reduced to a few special cases.It is beyond the scope of this book to discuss this reduction — which is anyway irrelevant to the mathematician using type theory in practice — but we will take a little time to discuss the one of the basic special cases that we have not yet met.These are Martin-Löf’s $\mathrm{W}$-types, also known as the types of well-founded trees.$𝖶$-types are a generalization of such types as natural numbers, lists, and binary trees, which are sufficiently general to encapsulate the “recursion” aspect of any inductive type.

A particular $𝖶$-type is specified by giving two parameters $A:𝒰$ and $B:A\to 𝒰$, in which case the resulting $𝖶$-type is written ${𝖶}_{(a:A)}B(a)$.The type $A$ represents the type of labels for ${𝖶}_{(a:A)}B(a)$, which function as constructors (however, we reserve that word for the actual functions which arise in inductive definitions). For instance, when defining natural numbers as a $𝖶$-type,the type $A$ would be the type $\mathrm{𝟐}$ inhabited by the two elements $0_{\mathrm{𝟐}}$ and $1_{\mathrm{𝟐}}$, since there are precisely two ways to obtain a natural number — either it will be zero or a successor of another natural number.

The type family $B:A\to 𝒰$ is used to record the arity of labels: a label $a:A$ will take a family of inductive arguments, indexed over $B(a)$. We can therefore think of the “$B(a)$-many” arguments of $a$. These arguments are represented by a function $f:B(a)\to {𝖶}_{(a:A)}B(a)$, with the understanding that for any $b:B(a)$, $f(b)$ is the “$b$-th” argument to the label $a$. The $𝖶$-type ${𝖶}_{(a:A)}B(a)$ can thus be thought of as the type of well-founded trees, where nodes are labeled by elements of $A$ and each node labeled by $a:A$ has $B(a)$-many branches.

In the case of natural numbers, the label $0_{\mathrm{𝟐}}$ has arity 0, since it constructs the constant zero; the label $1_{\mathrm{𝟐}}$ has arity 1, since it constructs the successor of its argument. We can capture this by using simple elimination on $\mathrm{𝟐}$ to define a function ${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,\mathrm{𝟎},\mathrm{𝟏})$ into a universe of types; this function returns the empty type $\mathrm{𝟎}$ for $0_{\mathrm{𝟐}}$ and the unit type $\mathrm{𝟏}$ for $1_{\mathrm{𝟐}}$. We can thus define

$${𝐍}^{𝐰}:\equiv {𝖶}_{(b:\mathrm{𝟐})}{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,\mathrm{𝟎},\mathrm{𝟏})$$

where the superscript $𝐰$ serves to distinguish this version of natural numbers from the previously used one.Similarly, we can define the type of lists over $A$ as a $𝖶$-type with $\mathrm{𝟏}+A$ many labels: one nullary label for the empty list, plus one unary label for each $a:A$, corresponding to appending $a$ to the head of a list:

$$\mathrm{𝖫𝗂𝗌𝗍}(A):\equiv {𝖶}_{(x:\mathrm{𝟏}+A)}{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟏}+A}(𝒰,\mathbf{\hspace{0.33em}0},\lambda a\mathbf{.\hspace{0.17em}1}).$$

In general, the $𝖶$-type ${𝖶}_{(x:A)}B(x)$ specified by $A:𝒰$ and $B:A\to 𝒰$ is the inductive type generated by the following constructor:

• $\mathrm{𝗌𝗎𝗉}:{\prod }_{(a:A)}(B(a)\to {𝖶}_{(x:A)}B(x))\to {𝖶}_{(x:A)}B(x)$.

The constructor $\mathrm{𝗌𝗎𝗉}$ (short for supremum) takes a label $a:A$ and a function $f:B(a)\to {𝖶}_{(x:A)}B(x)$ representing the arguments to $a$, and constructs a new element of ${𝖶}_{(x:A)}B(x)$. Using our previous encoding of natural numbers as $𝖶$-types, we can for instance define

$$0^{𝐰}:\equiv \mathrm{𝗌𝗎𝗉}(0_{\mathrm{𝟐}},\lambda x.{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x)).$$

Put differently, we use the label $0_{\mathrm{𝟐}}$ to construct $0^{𝐰}$. Then, ${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,\mathrm{𝟎},\mathrm{𝟏},0_{\mathrm{𝟐}})$ evaluates to $\mathrm{𝟎}$, as it should since $0_{\mathrm{𝟐}}$ is a nullary label. Thus, we need to construct a function $f:\mathrm{𝟎}\to {𝐍}^{𝐰}$, which represents the (zero) arguments supplied to $0_{\mathrm{𝟐}}$. This is of course trivial, using simple elimination on $\mathrm{𝟎}$ as shown. Similarly, we can define

$1^{𝐰}$$:\equiv \mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},\lambda x{\mathrm{.\hspace{0.17em}0}}^{𝐰})$

$2^{𝐰}$$:\equiv \mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},\lambda x{\mathrm{.\hspace{0.17em}1}}^{𝐰})$

and so on.

We have the following induction principle for $𝖶$-types:

• When proving a statement $E:\left({𝖶}_{(x:A)}B(x)\right)\to 𝒰$ about all elements of the $𝖶$-type ${𝖶}_{(x:A)}B(x)$, it suffices to prove it for $\mathrm{𝗌𝗎𝗉}(a,f)$, assuming it holds for all $f(b)$ with $b:B(a)$.In other words, it suffices to give a proof

  $$e:\prod _{(a:A)}\prod _{(f:B(a)\to {𝖶}_{(x:A)}B(x))}\prod _{(g:{\prod }_{(b:B(a))}E(f(b)))}E(\mathrm{𝗌𝗎𝗉}(a,f))$$

The variable $g$ represents our inductive hypothesis, namely that all arguments of $a$ satisfy $E$. To state this, we quantify over all elements of type $B(a)$, since each $b:B(a)$ corresponds to one argument $f(b)$ of $a$.

How would we define the function $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$ on natural numbers encoded as a $𝖶$-type? We would like to use the recursion principle of ${𝐍}^{𝐰}$ with a codomain of ${𝐍}^{𝐰}$ itself. We thus need to construct a suitable function

$$e:\prod _{(a:\mathrm{𝟐})}\prod _{(f:B(a)\to {𝐍}^{𝐰})}\prod _{(g:B(a)\to {𝐍}^{𝐰})}{𝐍}^{𝐰}$$

which will represent the recurrence for the $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$ function; for simplicity we denote the type family ${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,\mathrm{𝟎},\mathrm{𝟏})$ by $B$.

Clearly, $e$ will be a function taking $a:\mathrm{𝟐}$ as its first argument. The next step is to perform case analysis on $a$ and proceed based on whether it is $0_{\mathrm{𝟐}}$ or $1_{\mathrm{𝟐}}$. This suggests the following form

$$e:\equiv \lambda a.{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(C,e_0,e_1,a)$$

where

$$C:\equiv \prod _{(f:B(a)\to {𝐍}^{𝐰})}\prod _{(g:B(a)\to {𝐍}^{𝐰})}{𝐍}^{𝐰}$$

If $a$ is $0_{\mathrm{𝟐}}$, the type $B(a)$ becomes $\mathrm{𝟎}$. Thus, given $f:\mathrm{𝟎}\to {𝐍}^{𝐰}$ and $g:\mathrm{𝟎}\to {𝐍}^{𝐰}$, we want to construct an element of ${𝐍}^{𝐰}$. Since the label $0_{\mathrm{𝟐}}$ represents $\mathrm{𝟎}$, it needs zero inductive arguments and the variables $f$ and $g$ are irrelevant. We return $0^{𝐰}$ as a result:

$$e_0:\equiv \lambda f.\lambda g{\mathrm{.\hspace{0.17em}0}}^{𝐰}$$

Analogously, if $a$ is $1_{\mathrm{𝟐}}$, the type $B(a)$ becomes $\mathrm{𝟏}$.Since the label $1_{\mathrm{𝟐}}$ represents the successor operator, it needs one inductive argument — the predecessor — which is represented by the variable $f:\mathrm{𝟏}\to {𝐍}^{𝐰}$.The value of the recursive call on the predecessor is represented by the variable $g:\mathrm{𝟏}\to {𝐍}^{𝐰}$.Thus, taking this value (namely $g(\star )$) and applying the successor operator twice thus yields the desired result:

$$e_1:\equiv \lambda f.\lambda g.\mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda x.\mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda y.g(\star ))))).$$

Putting this together, we thus have

$$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}:\equiv {\mathrm{𝗋𝖾𝖼}}_{{𝐍}^{𝐰}}({𝐍}^{𝐰},e)$$

with $e$ as defined above.

The associated computation rule for the function ${\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}B(x)}(E,e):{\prod }_{(w:{𝖶}_{(x:A)}B(x))}E(w)$ is as follows.

• For any $a:A$ and $f:B(a)\to {𝖶}_{(x:A)}B(x)$ we have

  $${\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}B(x)}(E,e,\mathrm{𝗌𝗎𝗉}(a,f))\equiv e(a,f,(\lambda b.{\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}B(x)}(E,f(b)))).$$

In other words, the function ${\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}B(x)}(E,e)$ satisfies the recurrence $e$.

By the above computation rule, the function $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$ behaves as expected:

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0^{𝐰})$$\equiv {\mathrm{𝗋𝖾𝖼}}_{{𝐍}^{𝐰}}({𝐍}^{𝐰},e,\mathrm{𝗌𝗎𝗉}(0_{\mathrm{𝟐}},\lambda x.{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x)))$

$\equiv e(0_{\mathrm{𝟐}},(\lambda x.{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x)),(\lambda x.\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}({\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x))))$

$\equiv e_t((\lambda x.{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x)),(\lambda x.\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}({\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x))))$

$\equiv 0^{𝐰}$

and

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(1^{𝐰})$$\equiv {\mathrm{𝗋𝖾𝖼}}_{{𝐍}^{𝐰}}({𝐍}^{𝐰},e,\mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},\lambda x{\mathrm{.\hspace{0.17em}0}}^{𝐰}))$

$\equiv e(1_{\mathrm{𝟐}},\left(\lambda x{\mathrm{.\hspace{0.17em}0}}^{𝐰}\right),(\lambda x.\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0^{𝐰})))$

$\equiv e_f(\left(\lambda x{\mathrm{.\hspace{0.17em}0}}^{𝐰}\right),(\lambda x.\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0^{𝐰})))$

$\equiv \mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda x.\mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda y.\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0^{𝐰})))))$

$\equiv \mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda x.\mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda y{\mathrm{.\hspace{0.17em}0}}^{𝐰}))))$

$\equiv 2^{𝐰}$

and so on.

Just as for natural numbers, we can prove a uniqueness theorem for$𝖶$-types:

Theorem 5.3.1.

Let $g\mathrm{,}h\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}w\mathrm{:}{\mathrm{W}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathrm{(}x\mathrm{)}\mathrm{)}}E\mathit{}\mathrm{(}w\mathrm{)}$ be two functions which satisfy the recurrence

$$e:\prod _{a,f}\left(\prod _{b:B(a)}E(f(b))\right)\to E(\mathrm{𝗌𝗎𝗉}(a,f)),$$

i.e., such that

$$\prod _{a,f}g(\mathrm{𝗌𝗎𝗉}(a,f))=e(a,f,\lambda b.g(f(b))),$$

$$\prod _{a,f}h(\mathrm{𝗌𝗎𝗉}(a,f))=e(a,f,\lambda b.h(f(b))).$$

Then $g$ and $h$ are equal.