Why does Lean enforce strict positivity in inductive defs?

Stream: lean4

[nrs]

Am having a bit of trouble translating a definition from Agda to Lean. The following gives me the kernel error in the comment:

-- (kernel) arg #6 of 'Prog.enter' contains a non valid occurrence of the datatypes being declared

inductive Prog (Δ γ : Effect) (A : Type)
| return : A -> Prog Δ γ A
| call (op : Δ.op) (k : Δ.ret op -> Prog Δ γ A) : Prog Δ γ A
| enter {B : Type} (op : γ.op)  (sc : γ.ret op -> Prog Δ γ B) (k : B -> Prog Δ γ A) : Prog Δ γ A

From a stackexchange post, I understand this to be due to Lean enforcing strictly positive recursive occurrences in inductive type definitions. Could someone explain to me the theoretical underpinnings or issues that arise from this? Am hoping this will help in the translation.

[Kevin Buzzard]

If I'm allowed to define a function from the naturals to the naturals by $F(0)=37$ and $F(n+1)=F(n+1)+1$ then I can produce a contradiction so I'd better only be allowed to use $F(n)$ and not $F(n+1)$ in my definition of $F(n+1)$.

[nrs]

Kevin Buzzard said:

If I'm allowed to define a function from the naturals to the naturals by $F(0)=37$ and $F(n+1)=F(n+1)+1$ then I can produce a contradiction so I'd better only be allowed to use $F(n)$ and not $F(n+1)$ in my definition of $F(n+1)$.

This makes sense, but how is Agda able to remain consistent without this restriction?

[nrs]

i.e. the above restriction is not due to type theoretical considerations, but due to Lean itself, right? or is this not right?

[Kevin Buzzard]

nrs said:

Kevin Buzzard said:

If I'm allowed to define a function from the naturals to the naturals by $F(0)=37$ and $F(n+1)=F(n+1)+1$ then I can produce a contradiction so I'd better only be allowed to use $F(n)$ and not $F(n+1)$ in my definition of $F(n+1)$.

This makes sense, but how is Agda able to remain consistent without this restriction?

That sounds like a question for the Agda people!

[nrs]

Kevin Buzzard said:

nrs said:

Kevin Buzzard said:

If I'm allowed to define a function from the naturals to the naturals by $F(0)=37$ and $F(n+1)=F(n+1)+1$ then I can produce a contradiction so I'd better only be allowed to use $F(n)$ and not $F(n+1)$ in my definition of $F(n+1)$.

This makes sense, but how is Agda able to remain consistent without this restriction?

That sounds like a question for the Agda people!

hm right, ty for the help!

[Kevin Buzzard]

I'm not sure I've been much help! Hopefully someone here who understands inductive types beyond Nat will be able to say something useful. My impression was that Agda was less concerned about consistency and more concerned with being an experimental sandbox for type theory whereas lean is more conservative in this regard.

[Kevin Buzzard]

docs#Effect

[Kevin Buzzard]

PS your example doesn't compile, I don't think, as it stands (and not just because of the induction issue -- definition of Effect is missing). Are you able to edit your original post to make it a #mwe ? Experience shows that this is the best way to ask a question here.

[nrs]

Kevin Buzzard said:

PS your example doesn't compile, I don't think, as it stands (and not just because of the induction issue -- definition of Effect is missing). Are you able to edit your original post to make it a #mwe ? Experience shows that this is the best way to ask a question here.

I think it works if you add unsafe, I have no clue what this means however

[Kevin Buzzard]

Oh yeah unsafe switches off the checks and this means something like: you get your function and can run it on whatever input you like, but you can't prove theorems using it.

[nrs]

Kevin Buzzard said:

Oh yeah unsafe switches off the checks and this means something like: you get your function and can run it on whatever input you like, but you can't prove theorems using it.

hm I see, is the only difference the ability to have recursive occurrences in positions that are not strictly positive?

[nrs]

@Kevin Buzzard

somehow the people over at the Agda zulip fixed my Lean code: it will typecheck if we make A an index instead of a parameter:

inductive Prog (Δ γ : Effect) : Type -> Type _
| return : A -> Prog Δ γ A
| call (op : Δ.op) (k : Δ.ret op -> Prog Δ γ A) : Prog Δ γ A
| enter {B : Type} (op : γ.op)  (sc : γ.ret op -> Prog Δ γ B) (k : B -> Prog Δ γ A) : Prog Δ γ A

I was mistaken, the issue is not about polarity

[Jannis Limperg]

Agda also enforces strict positivity, but it may be slightly more liberal. The exact formulation of the strict positivity condition differs between proof assistants.

[nrs]

Jannis Limperg said:

Agda also enforces strict positivity, but it may be slightly more liberal. The exact formulation of the strict positivity condition differs between proof assistants.

Someone described the problem parameter in the initial piece of code as non-regular, maybe Agda infers something about a well-typed form from this fact. Would you happen to know if regularity of parameters is at all related to what we might mean by positivity?

[nrs]

or what I'm trying to get at is, how it is that we can think of a type system as being more/less liberal about strict positivity. This is a property of the inference algorithm, right?

[Trebor Huang]

If you replace (A : Type) by : Type -> Type 1 where, and prepend (A : Type) in the type of each constructor, does it work?

[Jannis Limperg]

Probably by "non-regular parameter" they mean a parameter that can vary in the domains of constructors, but not in the codomains. Here the parameter A is instantiated with A in all constructor codomains (so it's a parameter rather than an index), but it's instantiated with B in the domain of Prog.call (so it's not "regular"). I've also heard such parameter called "non-uniform". It appears that Agda allows non-uniform parameters but Lean doesn't.

Strict positivity is a condition that ensures that an inductive type declaration corresponds to a meaningful mathematical object. (Technically: that the least fixed point of the functor induced by the declaration is defined.) This is a sufficient but not necessary condition, so there can be slight variations in what is considered strictly positive.

[Jason Gross]

Presumably Lean's elaborator could elaborate inductives with non-regular parameters to inductives with only regular parameters?

[Kyle Miller]

In this message, Mario was saying that non-uniform parameters can be simulated with recursive definitions

[Mario Carneiro]

This inductive is already strictly positive, but it needs a universe bump

axiom Effect : Type
axiom Effect.op : Effect → Type
axiom Effect.ret (E : Effect) : E.op → Type

inductive Prog (Δ γ : Effect) : (A : Type) → Type 1
| return {A} : A -> Prog Δ γ A
| call {A} (op : Δ.op) (k : Δ.ret op -> Prog Δ γ A) : Prog Δ γ A
| enter {A} {B : Type} (op : γ.op)  (sc : γ.ret op -> Prog Δ γ B) (k : B -> Prog Δ γ A) : Prog Δ γ A

[Mario Carneiro]

This is not a non-uniform parameter that can be simulated by recursive definitions, because enter rule has no restrictions on what B is, it really is embedding Type in the inductive

[Mario Carneiro]

Proof that it cannot consistently live in Type:

axiom E : Effect
axiom O : E.op
noncomputable example (A : Type) (e : Prog E E Unit ≃ A) : False := by
  have : Cardinal.{0} ↪ Prog E E Unit := {
    toFun := fun κ =>
      let α := (Order.succ κ).out
      have : Nonempty α := Cardinal.mk_ne_zero_iff.1 (by simp [α]; apply Order.succ_ne_bot)
      .enter O (fun _ => .return this.some) (fun _ => .return ())
    inj' := fun _ _ eq => by simp at eq; exact Order.succ_injective eq.1
  }
  have := Cardinal.lift_mk_le.{1}.2 ⟨this.trans e.toEmbedding⟩
  simp at this
  exact this.not_lt (Cardinal.lift_lt_univ _)

[Mario Carneiro]

nrs said:

This makes sense, but how is Agda able to remain consistent without this restriction?

As far as I can tell, Agda has the stated restriction, and the inductive below is not accepted:

data Prog (A : Set) : Set where
  ret : A -> Prog A
  enter : (B : Set) -> (Prog B) -> (B -> Prog A) -> Prog A

/home/guest/hello.agda:3,3-8
Set₁ is not less or equal than Set
when checking that the type Set of an argument to the constructor
enter fits in the sort Set of the datatype.

[Mario Carneiro]

Kevin Buzzard said:

My impression was that Agda was less concerned about consistency and more concerned with being an experimental sandbox for type theory whereas lean is more conservative in this regard.

I think this is slightly overstated. Agda people definitely do care about consistency, but Agda also has a bunch of additional flags to control the behavior of the kernel, and not all of them are sound.