nLab inductive family

Idea

Inductive families generalize inductive types. Instead of defining a single type inductively, one simultaneously defines a whole family of types. An alternative term is “indexed inductive definition”.

A simple example of an inductive family is the type of vectors Vect n indexed by the dimension n. This is defined by two constructors: one for the empty vector of dimension 0, and another for the operation which constructs a vector of dimension n+1 by adding a component to a vector of dimension n. The family of finite types Fin n (indexed by n) can also be defined as an inductive family: the constructor 0 is in any Fin n, and there is a successor operation which constructs an element in Fin (n+1) from an element in Fin n.

By the identification of propositions as types, inductive families correspond to inductively defined predicates. For example, the identity type on a type A can be defined inductively by the reflexivity rule stipulating that a is identical to a for any a : A, that is, identity is the least reflexive relation. The identity family of types in intuitionistic type theory results from the identification of this relation with a family of types.

Examples

• The identity types of an indexed W-type are another indexed W-type. This has been formalized by Huginin.

• The inductive covers in formal topology and real analysis are an example of a higher inductive family.

Semantics

Standard inductive types, W-types can be interpreted in any topos with natural numbers object (Moerdijk-Palmgren). Gambino and Hyland construct initial algebras for dependent polynomial functors. Indexed containers are the same as dependent polynomial functors. Indexed containers are claimed to form a foundation for inductive families.

Higher categorical version/ homotopy type theory

van den Berg and Moerdijk show that (standard) W-types can be interpreted in certain model categories.

Reduction to ordinary W-types

In homotopy type theory with universes, one can reduce indexed W-types to W-types. This has been formalized here, here and here. Sattler outlines a generalization of the reduction to homotopy type theory without the need of universes.

References

History of inductive types

Historical references on the definition of inductive types.

Precursors

A first type theoretic formulation of general inductive definitions:

• Per Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, Studies in Logic and the Foundations of Mathematics 63 (1971) 179-216 $[$doi:10.1016/S0049-237X(08)70847-4$]$

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:

• Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 (1975) 73-118 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in:

• Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) $[$webpage, pdf, pdf$]$

The special case of inductive types now known as $\mathcal{W}$-types is first formulated in:

• 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), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) $[$pdf, pdf$]$

Early proposals for a general formal definition of inductive types:

• Robert L. Constable, N. Paul Francis Mendler, Recursive definitions in type theory, in Logic of Programs 1985, Lecture Notes in Computer Science 193 Springer (1985) $[$doi:10.1007/3-540-15648-8_5$]$

• Paul Francis Mendler, Inductive Definition in Type Theory, Cornell (1987) $[$hdl:1813/6710$]$

• Roland Backhouse, On the Meaning and Construction of the Rules of Martin-Löf’s Theory of Types, in: Workshop on General Logic, ECS-LFCS-88-52 (1988) $[$pdf, pdf$]$

Modern definition

The modern notion of inductive types and inductive families in intensional type theory is independently due to

• Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 $[$doi:10.1017/CBO9780511569807.012, pdf$]$

• Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 $[$doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf$]$

and due to

• Thierry Coquand, Christine Paulin, Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer (1990) 50-66 $[$doi:10.1007/3-540-52335-9_47$]$

which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:

• Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$doi:10.1007/BFb0040259$]$

• Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) $[$doi:10.1007/BFb0037116$]$

reviewed in

• Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ISBN:9780198538356, pdf$]$

• Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) $[$hal:01094195, pdf, pdf slides$]$

with streamlined exposition in:

• Univalent Foundations Project, §5.6 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) $[$web, pdf$]$

The generalization to inductive-recursive types is due to

• Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 $[$doi:10.2307/2586554, pdf$]$

• Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) $[$doi:10.1007/3-540-45504-3_7, pdf$]$

See also:

• Peter Dybjer, Inductive and inductive-recursive definitions in type theory (link list)

Further developments

• Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris, Indexed containers (pdf)

• Nicola Gambino and Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors PDF

• Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory (arXiv:1307.2765)

• Christian Sattler, On relating indexed W-types with ordinary ones slides

• Jasper Hugunin, IWTypes, https://github.com/jashug/IWTypes