3
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Andreas Rossberg Jan 29 '18 at 14:37
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jan 30 '18 at 7:52
  • $\begingroup$ @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 $\endgroup$ – user181407 Jan 30 '18 at 11:28
  • 2
    $\begingroup$ 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." $\endgroup$ – Andrej Bauer Jan 30 '18 at 13:10
  • 1
    $\begingroup$ @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. $\endgroup$ – Neel Krishnaswami Jan 30 '18 at 16:48
12
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – user181407 Jan 30 '18 at 11:39
  • $\begingroup$ 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? $\endgroup$ – user181407 Jan 30 '18 at 11:39
8
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Guys, guys, this is math, you're supposed to answer philosophically. $\endgroup$ – Andrej Bauer Jan 30 '18 at 13:11
7
$\begingroup$

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.

$\endgroup$
  • 6
    $\begingroup$ Dang, I can't downvote myself. $\endgroup$ – Andrej Bauer Jan 30 '18 at 13:26
5
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.