Speaking philosophically on a theoretical computer science forum, the word induction derives from Latin inducere which means something like "lead into". The word has several usages in science and logic. In the case of inductive types, it relates the idea of generating objects or constructing facts from other smaller or simpler objects or facts. In particular, the conception of inductive type has two essential features:
Monotonicity or covariance, which says inductively generated entities behave monotonically with respect to the building block, or transforms covariantly with respect to the building blocks. For example, if we build a new object $C(a,b)$ using a construction $C$ from parts $a$ and $b$, then
- increasing either $a$ or $b$ will increase $C(a,b)$ (monotonicity)
- a transformation $a \mapsto a'$ induces a transformation $C(a,b) \mapsto C(a',b)$, and similarly for a transformation of $b$ (covariance)
Freeness or initiality: inductive generation of entities introduces no relations between them, other than those that are necessary. To put this another way, the inductive construction is the most economic form of construction of a give shape.
All of these ideas are captured by the word "inductive". They can be made mathematically precise, and I would strongly encourage anyone who wishes to discuss them in detail to do so. It should be pointed out that covariance is a generalization of monotonicity. The freeness leads to the mathematical ideas of induction and recursion. The eliminators for an inductive type express exactly the idea of freeness.
The principles explain why we disallow certain kinds of constructions. For example, the suggested constructor
Inductive bad := b : (bad -> bad) -> bad.
violates the covariance assumption, or monotonicity. It therefore does not fit the idea that inductive generation accumulates, generates, or generally constructs entities, since the constructor b
may generate less from more. (Again, if you want a more precise answer, I strongly suggest that you switch to actual mathematics, as then things will be clear.)
The monotonicity requirement is by no means a philosophical or mathematical imperative. One may well drop it and allow arbitrary recursive types, which include the type bad
above. Such types are very rich, have interesting mathematics, and are used in programming languages. They do not qualify as "inductive" because they do not fit the idea of inductive generation of entities.
I will now downvote my own answer to indicate the fact that such talk is only welcome when supplemented by some coherent mathematical thoughts.
b
does introduce inconsistency. It enables encoding self-application, which enables expressing unrestrictive fixpoint operators like the Y combinator, which allows expressing non-normalizing proof terms, which allows you to prove false. $\endgroup$ – Andreas Rossberg Jan 29 '18 at 14:37