natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In type theory, by a $\mathcal{W}$-type [Martin-LΓΆf (1982), pp. 171, (1984), pp. 43] one means a type which is defined inductively in a $\mathcal{W}$ell-founded way based on a type $C$ of βconstructorsβ and a type of $A$ of βaritiesβ. As such, $\mathcal{W}$-types are special kinds of inductive types (see below).
The same terminology β$\mathcal{W}$-typeβ is used [Moerdijk & Palmgren (2000)] for objects in (suitable pre-)toposes which provide categorical semantics for the type-theoretic notion (see further below).
Concretely, the terms/elements of a $\mathcal{W}$-type may be thought of as βrooted well-founded treesβ with a certain branching type; different $\mathcal{W}$-types are distinguished by their branching signatures: In categorical semantics in Sets, a branching signature is represented by a family of sets $\{A_c\}_{c \in C}$ such that
each node of the tree is labeled with an element $c \colon C$ β referring to a constructor;
if a node is labeled by $c$ then it has exactly ${|A_c|}$ outgoing edges, each labeled by some $a \colon A_c$ β the arity of the constructor $c$.
If one discards the requirement that the trees be well-founded, then the notion of $\mathcal{W}$-type becomes that of a coinductive type called an M-type (presumably since βMβ is like a βWβ upside down).
In practice, $\mathcal{W}$-types are used to:
provide a constructive counterpart of the classical notion of a well-ordering
uniformly define a variety of well-behaved inductive types.
More complex inductive types, with multiple constructors that are assumed only to be strictly positive, can be reduced to $\mathcal{W}$-types, at least in the presence of other structure such as sum types and function extensionality; see for instance Abbott, Altenkirch & Ghani (2004). This can even be extended to inductive families.
In most set theoretic mathematical foundations, $\mathcal{W}$-types can be proven to exist, but in predicative mathematics and in type theory, where this is not the case, they are often introduced axiomatically (as usual for inductive types more generally).
There are two slightly different formulations of W-types:
(inference rules for $\mathcal{W}$-types)
(1) type formation rule:
(4) computation rule:
(due to Martin-LΓΆf (1984), pp. 43; streamlined review e.g. in Awodey, Gambino & Sojakova (2012, Β§2))
If the type theory is extensional, i.e. identities have unique proofs and (dependent) function types are extensional ($f=g$ if and only if $f(x)=g(x)$ for all $x$), then this is more or less equivalent to the 1-category-theoretic definition below. The type theories that are the internal logic of familiar kinds of categories are all extensional in this sense.
The main distinction from the naive categorical theory below is that the map $f$ (1) must be assumed to be a display map, i.e. to exhibit $A$ as a dependent type over $B$, in order that the dependent product $\Pi_f$ be defined.
In the case of dependent polynomial functors, it seems that $q$ must also be a display map, in order to define $\Sigma_q$. However, using adjointness, one can still define the W-type even if $q$ is not a display map. This more general version is what in type theory is called an indexed W-type; if $q$ is a display map then one sometimes refers to non-uniform parameters instead of indices. (By contrast, uniform parameters are the kind discussed above where $g f = h$, so that the entire construction takes place in a single slice category This is an instance of the red herring principle, since non-uniform parameters are not really parameters at all, but a special kind of indices.) For example, identity types are indexed W-types but not parametrized ones (even non-uniformly); see this blog post.)
In intensional type theory, a $\mathcal{W}$-type is only an initial algebra with respect to propositional equality, not definitional equality. In particular, the constructors are injective only propositionally, not definitionally. This applies already for the natural numbers type (Exp. ).
We discuss the categorical semantics of $\mathcal{W}$-types, due to Moerdijk & Palmgren (2000).
Here one describes a $\mathcal{W}$-type as an initial algebra for an endofunctor on an ambient category $\mathcal{C}$. The family $\{A_c\}_{c\in C}$ can be thought of as a morphism
in some category $\mathcal{C}$ (such that the fiber over $c\in C$ is $A_c$), and the endofunctor in question is the composite
where
$A^*$ denotes context extension, hence the pullback functor (a.k.a. $A\times -$);
$\Pi_f$ denotes the interpretation of the dependent product, i.e. the right base change along $f$;
$\Sigma_C$ the denotes the interpretation of the dependent sum, i.e. the left base change given by the forgetful functor from $\mathcal{C}_{/C}$ to $\mathcal{C}$.
Equivalently, it is the composite
where $\bigcirc_f$ is the reader monad $\Pi_f \circ f^*$. In other words, the dependent product is not actually dependent.
Such a composite is called a polynomial endofunctor. Explicitly, it is the functor $X \mapsto \sum_{c : C} X^{A_c}$.
This definition makes sense in any locally cartesian closed category, although the W-type (the initial algebra) may or may not exist in any given such category. (A non-elementary construction of them is given by the transfinite construction of free algebras.)
The above definition is most useful when the category $\mathcal{C}$ is not just locally cartesian closed but is a Ξ -pretopos, since often we want to use at least coproducts in constructing $A$ and $C$. For example, a natural numbers object (Exp. ) is a $\mathcal{W}$-type specified by one of the coproduct inclusions $1\to 1+1$, and the list object $L X$ is a $\mathcal{W}$-type specified by $X\to X+1$. More generally, endofunctors that look like polynomials in the traditional sense:
can be constructed as polynomial endofunctors in the above sense for any lextensive category, and hence in any $\Pi$-pretopos. A $\Pi$-pretopos in which all W-types exist is called a Ξ W-pretopos.
In a topos with a natural numbers object (NNO), W-types for any polynomial endofunctor can be constructed as certain sets of well-founded trees; thus every topos with a NNO is a Ξ W-pretopos. This applies in particular in the topos Set (unless one is a predicativist, in which case $Set$ is not a topos and W-types in it must be postulated explicitly).
The above has a natural generalization to dependent or indexed W-types (Gambino & Hyland (2004)) with a type $C$ of indices:
given a diagram of the form
there is the dependent polynomial functor
This reduces to the above for $C = \ast$ the terminal object.
Notice that we do not necessarily have $g f = h$, so this is not just a polynomial endofunctor of $\mathcal{C}/_{C}$ considered as a lccc in its own right. If we do have $g f = h$, then $C$ is called a type of parameters instead of indices.
(natural numbers type as a $\mathcal{W}$-type)
The natural numbers type $(\mathbb{N},\, 0,\, succ)$ is equivalently the $\mathcal{W}$-type (Def. ) with
$C \,\coloneqq\, \{0, succ\} \,\simeq\, \ast \sqcup \ast$;
$A_0 \,\coloneqq\, \varnothing$ (empty type);
$A_{succ} \,\coloneqq\, \ast$ (unit type)
(Danielsson (2012))
In homotopy type theory, if $C$ has h-level $n\geq -1$, then any $\mathcal{W}$-type of the form $\underset{C}{\mathcal{W}} B$ has h-level $n$ (as it should be for $\infty$-colimits).
The original definition in type theory is due to
Per Martin-LΓΆf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 $[$doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0$]$
Per Martin-LΓΆf (notes by Giovanni Sambin), pp. 43 of: Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) [pdf, pdf]
On the h-level of W-types:
Nils Anders Danielsson, Positive h-levels are closed under W (2012) [web]
which also computes the identity types of W-types (and more generally indexed W-types).
The observation that the categorical semantics of well-founded inductive types ($\mathcal{W}$-types) is given by initial algebras over polynomial endofunctors on the type system:
Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-LΓΆfβs type theory, Theoretical Computer Science 176 1β2 (1997) 329-335 $[$doi:10.1016/S0304-3975(96)00145-4$]$
Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories, Annals of Pure and Applied Logic 104 1-3 (2000) 189-218 $[$doi:10.1016/S0168-0072(00)00012-9$]$
Further discussion:
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Containers: Constructing strictly positive types, Theoretical Computer Science 342 1 (2005) 3-27 $[$doi:10.1016/j.tcs.2005.06.002$]$
Benno van den Berg, Ieke Moerdijk, $W$-types in sheaves [arXiv:0810.2398]
Generalization to inductive families (dependent $\mathcal{W}$-types):
Nicola Gambino, Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors, in: Types for Proofs and Programs TYPES 200, Lecture Notes in Computer Science 3085, Springer (2004) $[$doi:10.1007/978-3-540-24849-1_14$]$
Michael Abbott, Thorsten Altenkirch, Neil Ghani: Representing Nested Inductive Types using W-types, in: Automata, Languages and Programming, ICALP 2004, Lecture Notes in Computer Science, 3142, Springer (2004) $[$doi:10.1007/978-3-540-27836-8_8, pdf$]$
exposition: Inductive Types for Free β Representing nested inductive types using W-types, talk at ICALP (2004) $[$pdf$]$
Generalization to homotopy-initial algebras as categorical semantics for $\mathcal{W}$-types in homotopy type theory:
Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICSβ12: (2012) 95β104 $[$arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code$]$
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 $[$arXiv:1307.2765, doi:10.1017/S0960129514000516$]$
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31β42 $[$arXiv:1402.0761, doi:10.1145/2775051.2676983$]$
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1β45 $[$arXiv:1504.05531, doi:10.1145/3006383$]$
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 [arXiv:1307.2765, doi:10.1017/S0960129514000516]
Towards combining generalization to dependent and homotopical W-types:
Last revised on February 27, 2024 at 21:35:10. See the history of this page for a list of all contributions to it.