Well-formedness condition for inductive types

Question

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. What can I read about them? Could give a simple enough well-formedness condition which I can use?

Answer 1

In addition to Martin's answer, you can try the "British school":

• Altenkirch, McBride & McKinna Why Dependent Types Matter

• Goguen, McBride & McKinna Eliminating Dependent Pattern-Matching

I'm sure that by this point you've been told to read Ulf Norrel's PhD dissertation. In fact pretty much any paper by Ulf is useful in this regard.

Answer 2

Inductive types have been studied heavily and many variants exist. A well-known introduction to inductive definitions is

• P. Aczel, An Introduction to Inductive Definitions

which was originally published in the indispensable Handbook of Mathematical Logic, but is now available online stand-alone. An introduction to inductive types is

• T. Coquand, P. Dybjer, Inductive Definitions and Type Theory: an Introduction.

The theory of inductive definitions for Coq was first (?) approached in

• F. Pfenning, C. Paulin-Mohring, Inductively defined types in the Calculus of Constructions,

I don't know to what extend modern Coq has diverged from what's described in that paper. Either way, none of those is easy reading. You're probably better off to look at a Coq manual and copy the well-formedness conditions imposed there.