24
$\begingroup$

I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-recursion, etc.).

In particular, the following definition is accepted by Agda:

  data Ty : Set0 -> Set0 where
    c1 : Ty ℕ
    c2 : Ty (Ty ℕ)

whereas the equivalent Coq definition is rejected because the appearance of [Ty _] as an index of itself in c2 is considered to violate strict positivity.

  Inductive Ty : Set -> Set :=
    | c1 : Ty nat
    | c2 : Ty (Ty nat).

In fact, this case is almost verbatim an example from Coq'Art Section 14.1.2.1 of violating strict positivity:

  Inductive T : Set -> Set := c : (T (T nat)).

But I don't see the reasons for this difference between the type theories. The classic example of proving False using a negative occurrence of a type in a constructor argument is clear to me, but I can't see how one might derive a contradiction from this style of indexing (regardless of otherwise strictly positive constructor arguments).

Poking around the literature, Dybjer's early Inductive Families paper makes an offhand comment about Paulin-Mohring's solution in the CID paper having slightly different restrictions, and vaguely suggests the differences might be related to impredicativity, but doesn't elaborate further. Dybjer's paper seems to allow this, while Paulin-Mohring's clearly prohibits it.

Apparently I'm not the first to notice this difference of opinion, and some believe this definition shouldn't be permitted in either system (https://lists.chalmers.se/pipermail/agda/2012/004249.html), but I haven't found any explanations of why it is either sound in one system but not the other, or just a difference of opinion.

So I suppose I have several questions:

  1. Is this an example of a monotone, but non-strictly-positive type? (In Coq; clearly Agda considers it strictly positive)
  2. Why does Agda permit this while Coq rejects it? It is simply an idiosyncratic difference in the interpretation of "strictly positive," is there a subtle difference between Coq and Agda that makes it sound in Agda and unsound in Coq, or is it a matter of taste driven by particular theoretical preferences?
  3. Is there a meaningful difference between the first definition above, and the equivalent inductive-recursive definition below?

Inductive-recursive definition:

  mutual
    data U : Set0 -> Set0 where
      c : (i : Fin 2) -> U (T i)
    T : Fin 2 -> Set0
    T zero = ℕ
    T (suc zero) = U ℕ

I'm happy to have pointers to relevant literature.

Thanks in advance.

$\endgroup$
  • 1
    $\begingroup$ As far as I know, Coq is stricter than what the underlying theory allows, because it was easier to implement and useful enough in practice. This answer about a different but related case is as far as my understanding goes. $\endgroup$ – Gilles Aug 29 '13 at 23:43
  • 1
    $\begingroup$ This definition is not accepted by the current dev version of Agda: Ty is not strictly positive, because it occurs in an index of the target type of the constructor c2 in the definition of Ty. $\endgroup$ – gallais Aug 30 '13 at 16:42
  • 2
    $\begingroup$ Yes, you're right, someone else pointed this out to me last night. I had been using Debian's 2.3.0.1 package, but 2.3.2.1 from Cabal rejects both the direct and IR definitions. It looks like a seemingly unrelated bug made positivity checking on indices stricter: code.google.com/p/agda/issues/detail?id=690 Since it was discussed on the list without explicitly being marked a soundness issue, I'm still wondering if the type itself is sound. $\endgroup$ – Colin Gordon Aug 30 '13 at 18:03
10
$\begingroup$

The issue seems to be confusion resulting from a confluence of two factors:

  1. I was using a stale version of Agda (2.3.0.1). It appears that prior to 2.3.2, Agda simply wasn't checking strict positivity of the indices of constructor results (see the bug I linked elsewhere in the thread).
  2. A closer reading of Dybjer's Inductive Families paper suggests that he may have intended that the inductive type being defined not be bound when typing the indices of a constructor result. Section 3.2.1 gives the scheme for inductive constructors in prose, and apparently I misread the language describing the binding environments of each portion of the scheme.

This closer reading is of course consistent with the check that Coq and (recent versions of) Agda perform, that prohibit any appearance of T in its own indices.

$\endgroup$
4
$\begingroup$

A possible reason for the difference, as your own remarks hint, is impredicativity. Coq historically had an impredicative set (still available as a flag i believe!)

Quoting Adam Chlipala's book http://adam.chlipala.net/cpdt/html/Universes.html

The Coq tools support a command-line flag -impredicative-set, which modifies Gallina in a more fundamental way by making Set impredicative. A term like forall T : Set, T has type Set, and inductive definitions in Set may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for Prop. The restriction only applies to large inductive types, where some constructor quantifies over a type of type Type. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is Set or Prop. This rule contrasts with the rule for Prop, where the restriction applies even to non-large inductive types, and where the result type may only have type Prop. In old versions of Coq, Set was impredicative by default. Later versions make Set predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative Set with axioms of choice. In combination with excluded middle or predicate extensionality, inconsistency can result. Impredicative Set can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it.

$\endgroup$
  • $\begingroup$ From the sound of the bug fix I found above, it sounds like Agda simply wasn't checking positivity of indices for constructor results. Which doesn't actually indicate whether my proposed type in monotone, but suggests it isn't related to impredicativity. $\endgroup$ – Colin Gordon Aug 30 '13 at 18:46
  • 2
    $\begingroup$ And yes, -impredicative-set makes Set impredicative in Coq. $\endgroup$ – Colin Gordon Aug 30 '13 at 18:47

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.