I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories generally) for the nested positivity conditions and how they come about? I've found older papers like Dybjer's Inductive Families and Coquand and Paulin's Inductively Defined Types, but I believe these only mention the strict positivity condition, and newer papers like the pCuIC one and A Comprehensible Guide to CIC don't mention nested positivity either.

Now, I'm trying to gain an intuitive understanding of why nested positivity is required. In essence, nested positivity states that when defining a constructor C for some inductive type $D$, if the type of an argument to $C$ is something like $I ~ \vec{p} ~ \vec{t}$, then $D$ can only appear strictly positively in $\vec{p}$, and only if $I \neq D$. I understand that allowing $D$ in negative positions of $\vec{p}$ basically allows for proofs of $(D \to \bot) \to \bot$, and allowing $D$ in other positive positions essentially allows for double negation elimination (and some inconsistency stuff with impredicative Prop). What I don't understand are these:

  • Why can't $D$ appear strictly positively in $\vec{p}$ if $I = D$ (either as constructor argument or return type)? For instance, for a constructor $C$ of an inductive type $D ~ (A: \textrm{Type}): \textrm{Type}$ (with $A$ as the sole parameter), why is $C: D ~ (D ~ A) \to D ~ A$ disallowed?

    EDIT: Not only is this accepted in Agda, $C: D ~ (D ~ A \to \bot) \to D ~ A$ is also accepted, which seems suspicious to me.

  • Why can $D$ otherwise appear strictly positively in the parameters $\vec{p}$, but not in the indices $\vec{t}$? Consider for instance the (rather silly) constructor $C: (D =_{\textrm{Type}} D) \to D$ for the inductive type $D: \textrm{Type}$, where $=$ is the usual equality type.

    EDIT: It turns out this doesn't type check in Agda for unrelated universe level reasons, so consider instead the following which Agda rejects for positivity reasons:

    data Box : (A : Set) → Set where
      box : (A : Set) → Box A
    data D : Set where
      C : Box D → D

    This is accepted by Agda if A is instead a parameter, as expected from the nested positivity rules.

I'm particularly interested in finding examples where violating nested positivity conditions (specifically these two I've listed) causes inconsistencies and proofs of $\bot$, which personally would be easier to understand than arguments about monotonicity.

  • 2
    $\begingroup$ Probably useful to mention cstheory.stackexchange.com/questions/18797/… $\endgroup$ – cody Jan 4 at 14:30
  • $\begingroup$ In general, it would (I believe) be possible to encode non strictly positive types by proxy if indices were considered strictly positive. Like neg : C = D -> ... where C occurs negatively elsewhere, but is not subject to the check. I'm not certain why your particular example isn't accepted by Agda, because it has analysis for detecting that X is actually like a parameter (that's why Box is well-sized). I guess it doesn't take that into account with respect to positivity checking. $\endgroup$ – Dan Doel Jan 6 at 6:25
  • $\begingroup$ @DanDoel So I tried to construct an example and this was about as far as I could get: data _≡_ (A : Set) : Set → Set where refl : A ≡ A, data D : Set where neg : (E : Set) → (E → ⊥) → D ≡ E → D. This isn't accepted but it's because neg needs to be in the same universe as D, but E: Set means that it's actually in Set₁. Interestingly, with the constructor c: D ≡ ⊤ → D, Agda complains about D not being strictly positive in , but not if I change the type of refl to A ≡ ⊤, so it seems Agda doesn't merely check whether it's a parameter or index. $\endgroup$ – ionathanch Jan 6 at 12:00
  • $\begingroup$ It also turns out that I can't use code blocks in comments :/ $\endgroup$ – ionathanch Jan 6 at 12:03
  • 1
    $\begingroup$ FYI, in the example in your first bullet point, if you add a constructor that actually uses $A$ in the dangerous example, Agda will complain that $D$ is no longer strictly positive. So it is just noticing that your $D (D A → ⊥)$ doesn't matter. It is odd that $D (D A)$ is allowed, though, since it doesn't make much sense under the usual semantics. $\endgroup$ – Dan Doel Jan 6 at 22:11

Here is an example exploiting positivity of an index to prove false:

module Whatever where

open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Data.Empty

  ℓ : Level
  A B : Set ℓ

data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where
  trefl : A ≅ A

Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B
Subst P trefl PA = PA

data U : Set where
  d : U

El : U → Set
data D : Set

El d = D

data D where
  neg : ∀(c : U) → El c ≅ D → (El c → ⊥) → D

¬D : D → ⊥
¬D v@(neg c eq f) = Subst (λ D → D → ⊥) eq f v

spin : ⊥
spin = ¬D (neg d trefl ¬D)

Technically it also makes use of the fact that induction-recursion can create small universes, and that type equality can be smaller than general equality applied to the universe, but those are otherwise not really problematic to my knowledge (Coq has impredicative equality anyway, I believe). It's possible the simultaneous definition could be eliminated, too, but it's not straight forward, at least.

Edit: I asked around about your first bullet point. It was pointed out to me that there is essentially nothing special about a nested type that is nested in itself. This article shows how to use a non-native translation of nested types into indexed types of equivalent size. When you do that, as long as nesting is strictly positive, it's not difficult to apply the translation to a strictly positive indexed type.

Or for instance, the example translation I was shown uses a nested $ℕ$ parameter instead of self-nesting:

data D' (A : Set) (n : ℕ) : Set where
  c : D' A (suc n) → D' A n
  t : (case n of λ where
         zero → A
         (suc m) → D' A m
      ) → D' A n

Where I added the t constructor to make something actually use A, and D A is meant to be equivalent to D' A 0. I think another way to write this would be:

data D' (A : Set) : ℕ → Set where
  c : D' A (suc n) → D' A n
  t : D' A n → D' A (suc n)
  t' : A → D' A zero

Essentially, the $ℕ$ is a tree tracking how much nesting we need to unfold.

  • $\begingroup$ I have a suspicion that since (El c → ⊥) reduces to (D → ⊥), the definition might not pass plain positivity (as opposed to merely violating nested positivity), but there doesn't seem to be a way to turn off only nested positivity in Agda anyway. $\endgroup$ – ionathanch Jan 6 at 21:11
  • 1
    $\begingroup$ El c does not reduce to D. El c is a neutral term, because c is a variable. In my example, d is the only value for c to take, but I could easily add more. $\endgroup$ – Dan Doel Jan 6 at 21:23

I'm going to partially answer point 2 here. If you allowed the inductive type to appear even strictly positively in another inductive's index, and you had impredicative Prop, you could derive an inconsistency through an equality type with a type that does occur negatively, as Dan stated in the comments. Here's an example in Coq, with the inductive type stated as axioms.

Inductive Equal (A: Prop) : Prop -> Prop :=
| refl : Equal A A.

(** These axioms correspond to the following inductive definition:
 *  Inductive D : Prop :=
 *  | C : forall (E: Prop) (p: Equal D E), (E -> False) -> D. *)
Axiom D : Prop.
Axiom introD: forall (E: Prop) (p: Equal D E), (E -> False) -> D.
Axiom matchD: forall (E: Prop) (p: Equal D E), D -> (E -> False).

Definition DnotD (d: D): (D -> False) := matchD D (refl D) d.
Definition notD (d: D): False := (DnotD d) d.
Definition isD: D := introD D (refl D) notD.
Definition bottom: False := notD isD.

I'm not sure whether you can do the same when you only have predicative universes without resorting to universe polymorphism tricks or the like.


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.