<p>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$, <code>bad</code> should satisfy $F_1($<code>bad</code>$)=$<code>bad</code>.</p>

<p>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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2018-01-30T11:39:48.057Z
I don't find this answer entirely satisfying because it seems to rely on the notion that when we have a type in mind, we already must have it understand as a completed totality; or worse, that we presume that our types must match up to some sort of set-based semantics.  I can say that the type I have in mind when I declare `bad` is precisely the freely generated terms produced by its constructor and nothing more.
user181407
CC BY-SA 3.0
2018-01-30T11:39:52.587Z
To put it another way, all the other rules of dependent type theory are easily and clearly justifiable, but once we talk about inductive types suddenly we have to reach for Knaster-Tarski and assume that our types are actually like sets?
user181407
CC BY-SA 3.0
2018-01-29T14:40:53.190Z
2018-01-29T14:40:53.190Z
xavierm02
<p>Speaking philosophically on a theoretical computer science forum, the word <em>induction</em> derives from Latin <em>inducere</em> 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:</p>

<ol>
<li><p><strong>Monotonicity</strong> or <strong>covariance</strong>, 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</p>

<ul>
<li>increasing either $a$ or $b$ will increase $C(a,b)$ (monotonicity)</li>
<li>a transformation $a \mapsto a'$ induces a transformation $C(a,b) \mapsto C(a',b)$, and similarly for a transformation of $b$ (covariance)</li>
</ul></li>
<li><p><strong>Freeness</strong> or <strong>initiality</strong>: 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.</p></li>
</ol>

<p>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.</p>

<p>The principles explain why we disallow certain kinds of constructions. For example, the suggested constructor</p>

<pre><code>Inductive bad := b : (bad -&gt; bad) -&gt; bad.
</code></pre>

<p>violates the covariance assumption, or monotonicity. It therefore does not fit the idea that inductive generation accumulates, generates, or generally <em>constructs</em> entities, since the constructor <code>b</code> 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.)</p>

<p>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 <code>bad</code> 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.</p>

<p>I will now downvote my own answer to indicate the fact that such talk is only welcome when supplemented by some coherent mathematical thoughts.</p>

CC BY-SA 3.0
2018-01-30T13:26:21.690Z
Dang, I can't downvote myself.
Andrej Bauer
CC BY-SA 3.0
2018-01-30T13:26:09.037Z
2018-01-31T07:23:27.300Z
2018-01-31T07:23:27.300Z
Andrej Bauer
<p>To elaborate on Andreas Rossberg's comment on the question, a good way to understand this is in terms of <a href="https://en.wikipedia.org/wiki/Curry%27s_paradox" rel="noreferrer">Curry's paradox</a>. Basically, if your language supports:</p>
<ol>
<li>The ability to use hypotheses in an argument more than once</li>
<li>Implication</li>
<li>General self-reference</li>
</ol>
<p>Then it is inconsistent. Greg Restall wrote a nice paper, <a href="http://consequently.org/papers/costing.pdf" rel="noreferrer"><em>Curry's revenge: the costs of non-classical solutions to the paradoxes of self-reference</em></a>, discussing this from a philosophical perspective.</p>
<p>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 <em>contraction</em>), implication means having a function type, and general self-reference means unrestricted recursive types,</p>
<ol>
<li><p>If we drop the ability to use a variable multiple times, we get <em>linear logic</em>, and it is well-known that linear logic (without exponentials) remains consistent even with unrestricted recursive types.</p>
</li>
<li><p>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).</p>
</li>
<li><p>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.</p>
<p>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 &quot;inductive-recursive&quot; definitions in dependent type theory.</p>
</li>
</ol>

CC BY-SA 3.0
2018-01-30T13:11:58.293Z
Guys, guys, this is math, you're supposed to answer philosophically.
Andrej Bauer
CC BY-SA 3.0
2018-01-30T10:27:31.800Z
2018-01-30T10:27:31.800Z
2020-06-17T09:38:08.363Z
Neel Krishnaswami
<p>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 <em>endo</em>functor, $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$.</p>

CC BY-SA 3.0
2018-01-30T06:27:25.683Z
2018-01-30T06:27:25.683Z
Damiano Mazza
<p>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</p>

<pre><code>Inductive bad :=
  | b : (bad -&gt; bad) -&gt; bad.
</code></pre>

<p>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.</p>

CC BY-SA 3.0
2018-01-29T14:37:08.677Z
No time for a proper answer, but a type like `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.
Andreas Rossberg
CC BY-SA 3.0
2018-01-30T07:52:47.323Z
Yes, there is a good philisophical reason: dropping the requirement gives an inconsistent system. Actually, that's a mathematical reason, which is even better than a philosophical reason. Also, this question is not research-level and should be asked on a different forum.
Andrej Bauer
CC BY-SA 3.0
2018-01-30T11:28:03.403Z
@AndrejBauer  I don't think a mathematical reason is any better than a philosophical reason.  If I was studying set theory and was wondering why people require only restricted comprehension instead of general comprehension, I would much prefer an answer that says something like "typically properties we have in mind are already implicitly bound over a given set so this better matches actual mathematical practice etc." instead of "because otherwise it's inconsistent so shut up and stop asking questions", which is to say that pointing out that a concept yields inconsistencies doesn't necessarily
user181407
CC BY-SA 3.0
2018-01-30T11:28:27.443Z
...explain _why_ a concept is conceptually faulty.
user181407
CC BY-SA 3.0
2018-01-30T13:10:54.873Z
Sure, we can do philsophy: "The monotonicity requirement captures the idea of free covariant generation." It's just that you're not on the right site for that sort of thing. As far as usefulness of philisophical ideas goes, I could paraphrase the one about theory and practice: "Mathematics without philosophy is blind calculation, philosophy without mathematics is just idle contemplation."
Andrej Bauer
CC BY-SA 3.0
2018-01-30T15:00:10.690Z
@AndrejBauer I'm glad I could change your response from "your question doesn't warrant a response and furthermore doesn't belong here" to just "your questions doesn't belong here". In the future I will remember to take such questions to the Philosophy of Type Theory stack exchange instead.
user181407
CC BY-SA 3.0
2018-01-30T16:48:36.797Z
@user181407: people require restricted comprehension, because they also want implication and contraction in their logical foundation, and all three  let Russell prove the inconsistency of Frege's system. However, unrestricted comprehension is totally okay if you drop contraction: for example, Kazushige Terui's Light Affine Set Theory is a consistent set theory with unrestricted comprehension, at the price of giving up contraction. Paul Taylor once remarked to me that if A, B, and C jointly imply a contradiction, you have 7 options on what to accept. Philosophy helps you pick the subset.
Neel Krishnaswami
CC BY-SA 3.0
2018-01-31T08:45:48.600Z
@user181407: Philosophy of Type Theory that would be a very cool site :-)
Andrej Bauer
CC BY-SA 3.0
2018-01-31T09:38:45.507Z
iirc, the first version of Martin-Löf's type theory was inconsistent (Girard's paradox). Not sure what is the relation to Bishop. I think of these kind of conditions as a means to make sure a limit (you can think of a least fixed point exists) exists.
Kaveh
<lo.logic><type-theory><philosophy>
Philosophy behind monotonicity requirement for inductive types
user181407
# Philosophy behind monotonicity requirement for inductive types

(Asked by: username_0 on 2018-01-29)

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.

**Tags:** lo.logic, type-theory, philosophy
> **Comments:**
> **username_1**: No time for a proper answer, but a type like `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.  
> **username_2**: Yes, there is a good philisophical reason: dropping the requirement gives an inconsistent system. Actually, that's a mathematical reason, which is even better than a philosophical reason. Also, this question is not research-level and should be asked on a different forum.  
> **username_0**: @AndrejBauer  I don't think a mathematical reason is any better than a philosophical reason.  If I was studying set theory and was wondering why people require only restricted comprehension instead of general comprehension, I would much prefer an answer that says something like "typically properties we have in mind are already implicitly bound over a given set so this better matches actual mathematical practice etc." instead of "because otherwise it's inconsistent so shut up and stop asking questions", which is to say that pointing out that a concept yields inconsistencies doesn't necessarily  
> **username_0**: ...explain _why_ a concept is conceptually faulty.  
> **username_2**: Sure, we can do philsophy: "The monotonicity requirement captures the idea of free covariant generation." It's just that you're not on the right site for that sort of thing. As far as usefulness of philisophical ideas goes, I could paraphrase the one about theory and practice: "Mathematics without philosophy is blind calculation, philosophy without mathematics is just idle contemplation."  
> **username_0**: @AndrejBauer I'm glad I could change your response from "your question doesn't warrant a response and furthermore doesn't belong here" to just "your questions doesn't belong here". In the future I will remember to take such questions to the Philosophy of Type Theory stack exchange instead.  
> **username_3**: @user181407: people require restricted comprehension, because they also want implication and contraction in their logical foundation, and all three  let Russell prove the inconsistency of Frege's system. However, unrestricted comprehension is totally okay if you drop contraction: for example, Kazushige Terui's Light Affine Set Theory is a consistent set theory with unrestricted comprehension, at the price of giving up contraction. Paul Taylor once remarked to me that if A, B, and C jointly imply a contradiction, you have 7 options on what to accept. Philosophy helps you pick the subset.  
> **username_2**: @user181407: Philosophy of Type Theory that would be a very cool site :-)  
> **username_4**: iirc, the first version of Martin-Löf's type theory was inconsistent (Girard's paradox). Not sure what is the relation to Bishop. I think of these kind of conditions as a means to make sure a limit (you can think of a least fixed point exists) exists.  

---

## 4 answers

### Answer by username_5 on 2018-01-29. Score: 11

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.

> **Comments:**
> **username_0**: I don't find this answer entirely satisfying because it seems to rely on the notion that when we have a type in mind, we already must have it understand as a completed totality; or worse, that we presume that our types must match up to some sort of set-based semantics.  I can say that the type I have in mind when I declare `bad` is precisely the freely generated terms produced by its constructor and nothing more.  
> **username_0**: To put it another way, all the other rules of dependent type theory are easily and clearly justifiable, but once we talk about inductive types suddenly we have to reach for Knaster-Tarski and assume that our types are actually like sets?  

---

### Answer by username_2 on 2018-01-30. Score: 8

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.

> **Comments:**
> **username_2**: Dang, I can't downvote myself.  

---

### Answer by username_3 on 2018-01-30. Score: 8

To elaborate on Andreas Rossberg's comment on the question, a good way to understand this is in terms of [Curry's paradox](https://en.wikipedia.org/wiki/Curry%27s_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*](http://consequently.org/papers/costing.pdf), 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.

> **Comments:**
> **username_2**: Guys, guys, this is math, you're supposed to answer philosophically.  

---

### Answer by username_6 on 2018-01-30. Score: 5

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 *endo*functor, $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$.


---

