Philosophy behind monotonicity requirement for inductive types

Question

Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions? According to my understanding of the Bishop/Martin-Löf view of mathematics, to construct a set is to say how to construct elements of said set (as well as say how elements are identified, but that's not so important for this discussion). That's fine, but then I don't see why the standard inductive presentation of the naturals is a valid construction, but something like

Inductive bad :=
  | b : (bad -> bad) -> bad.

is not. To be clear, I understand how such definitions yield inconsistencies and so I certainly understand from a purely pragmatic perspective why such restrictions need to be made. However, it's one thing to be able to banish inconsistency, and another to be able to give a natural explanation for why such restrictions should be made.

Answer 1

When you write an inductive, you are defining a type by an equation. For example, if we write $F_1(X)=X^X=X\to X$, bad should satisfy $F_1($bad$)=$bad.

In general such equations can have several solutions, or none. For example, for $F_2(X)=X^X\times X$, you have (at least) two distinct solutions: $0$ (empty set) and $1$ (singleton). So you want some way to pick a specific solution.

The fact that you declared your type as inductive means that you pick the smallest solution (and coinductive would've meant the largest). So you want to be sure that this smallest solution exists. One way to ensure this is to ask for $F$ to be monotonous because then, the Knaster–Tarski theorem implies that it has a smallest fixpoint.

Aside from inconsistencies, I don't see a reason to ban other classes of equations, as long as you have a way to pick a specific solution. But unless you are sure that there is always a smallest solution for those equations, and that you will pick it, you probably shouldn't call it inductive.

Answer 2

To elaborate on Andreas Rossberg's comment on the question, a good way to understand this is in terms of Curry's paradox. Basically, if your language supports:

1. The ability to use hypotheses in an argument more than once
2. Implication
3. General self-reference

Then it is inconsistent. Greg Restall wrote a nice paper, Curry's revenge: the costs of non-classical solutions to the paradoxes of self-reference, discussing this from a philosophical perspective.

In type theory, the ability to use hypotheses more than once is the ability to refer to the same variable multiple times in an expression (for various reasons, this is called contraction), implication means having a function type, and general self-reference means unrestricted recursive types,

1. If we drop the ability to use a variable multiple times, we get linear logic, and it is well-known that linear logic (without exponentials) remains consistent even with unrestricted recursive types.

2. If we decide to drop function spaces, then depending on what you are interested in, this can be understood as leading to the finitary strategies in game semantics, or possibly as geometric logic (from topos theory).

3. If we decide to drop unrestricted self-reference, then essentially we are saying we need to appeal to a fixed point theorem to justify a recursive construction.

   The Knaster-Tarski theorem is most typical, but a variety of others are also used -- Banach's theorem is used in guarded type theory, and Pataraia's theorem justifies the "inductive-recursive" definitions in dependent type theory.

Answer 3

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:

1. 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)

2. 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.

Answer 4

Let me give another point of view on xavierm02's answer, perhaps a bit more general. One possible general way of seeing inductive types is as initial algebras of endofunctors (of some category $\mathbf C$, e.g. $\mathbf{Set}$). Typically, in a definition like $$\mathtt{datatype~ T = C1 ~|~ ... ~|~ Cn},$$ the fact that $C_1,\ldots,C_n$ mention $T$ means that these will be functors (of the variable $T$), and the type $T$ itself is the initial algebra of the functor $C_1+\ldots+C_n$. Now, for this to be an endofunctor, $T$ must occur only in positive position in $C_i$, because a negative occurrence would give a contravariant dependency and the resulting functor will be of the form $\mathbf C^{\textrm{op}}\times\mathbf C\to\mathbf C$ instead of $\mathbf C\to\mathbf C$.