breaking inductive

Stream: general

[Leonard Wiechmann]

hey all, i've been messing with inductive to test my understanding of the typing rules wrt universe levels.
i've found 2 cases that i'm unsure about:

-- 1: incomplete recursive arguments.

-- this doesn't and shouldn't work. `r: nat -> Sort 1`, which has type Sort 2, which is too large.
inductive T1: nat -> Sort 1
| c (r: T1): T1 0

-- but this should work, right? `r: nat -> Prop`, which has type Prop = Sort 0 and 0 <= 0.
inductive T0: nat -> Sort 0
| c (r: T0): T0 0
--           ^^
-- it gives me an error here:
--type expected at
--  T0
--term has type
--  ℕ → Prop
-- that error doesn't really make sense: `\N -> Prop` is a type?
-- if anything, i'd have expected `r: T0` to error.

-- 2: definition of Vec doesn't work for generic universe level.

-- this errors: arg 3 to cons (ts) is too large, which it isn't.
-- this same definition works when using Type instead of Sort.
inductive {u} Vec (T: Sort u): nat -> Sort u
| nil: Vec 0
| cons (t: T) (n: nat) (ts: Vec n): Vec n.succ

-- but the definition for any concrete universe level is valid...
-- works.
inductive Vec0 (T: Sort 0): nat -> Sort 0
| nil: Vec0 0
| cons (t: T) (n: nat) (ts: Vec0 n): Vec0 n.succ

-- works.
inductive Vec1 (T: Sort 1): nat -> Sort 1
| nil: Vec1 0
| cons (t: T) (n: nat) (ts: Vec1 n): Vec1 n.succ

-- works.
inductive Vec42 (T: Sort 42): nat -> Sort 42
| nil: Vec42 0
| cons (t: T) (n: nat) (ts: Vec42 n): Vec42 n.succ

[Leonard Wiechmann]

i think both examples should work.
which is bugged: my understanding or lean?

[Reid Barton]

In 1, both r : T1 and r : T0 don't make any sense. I guess Lean's error reporting got confused.

[Reid Barton]

In 2, it is not a bug, but maybe a limitation? You can't create an inductive which is a Prop for some values of the universe parameters, and a Type for others--I think it has something to do with what recursor to generate.

[Leonard Wiechmann]

yeah, example 1 doesn't make sense semantically.
but shouldn't r: T0 for T0: nat -> Prop work? -- just according to the universe levels. so make sense "syntactically"?

[Reid Barton]

no

[Leonard Wiechmann]

Reid Barton said:

In 2, it is not a bug, but maybe a limitation? You can't create an inductive which is a Prop for some values of the universe parameters, and a Type for others--I think it has something to do with what recursor to generate.

ok, that makes sense. it can't generate both recursors.

[Reid Barton]

in r : T0, T0 had better be a type, but whoops it is a function T0 : nat -> Prop instead

[Reid Barton]

Has nothing to do with universes.

[Mario Carneiro]

Reid Barton said:

In 2, it is not a bug, but maybe a limitation? You can't create an inductive which is a Prop for some values of the universe parameters, and a Type for others--I think it has something to do with what recursor to generate.

Actually you can, it's just not advisable

[Leonard Wiechmann]

oh, I think I see where I got confused.
i thought T0 = nat -> Prop and just substituted.

[Mario Carneiro]

Lean 4 disallows this in the elaborator now but you can still create them if you ask the kernel directly

[Leonard Wiechmann]

Mario Carneiro said:

Lean 4 disallows this in the elaborator now but you can still create them if you ask the kernel directly

does it generate the recursor for Type, or both?

[Mario Carneiro]

It generates the recursor for Prop

[Leonard Wiechmann]

well, that makes sense :D

[Mario Carneiro]

that is, it is a small eliminating type

[Mario Carneiro]

it's a recursor for all variations of the type, but the motive targets Prop

[Leonard Wiechmann]

right, because it isn't LE for all universe levels

[Mario Carneiro]

inductive {u} foo : Sort u
| a : foo
| b : foo

set_option pp.universes true
#print foo.rec
-- protected eliminator {u} foo.rec : ∀ {motive : foo.{u} → Prop}, motive foo.a.{u} → motive foo.b.{u} → ∀ (n : foo.{u}), motive n

[Leonard Wiechmann]

you need 2 constructors to not be subsingleton, right?

[Mario Carneiro]

right

[Mario Carneiro]

or other things

[Leonard Wiechmann]

ok, I think i've cleared up my confusion, thanks guys!

[Mario Carneiro]

the fun part I like to show with this example is that foo.a.{1} and foo.b.{1} are neither provably equal nor provably distinct

[Reid Barton]

ah right, I was misremembering how the example I wanted to work fails

inductive {u} M (X : Sort u) : Sort u
| mk : X → M

[Reid Barton]

This seems like it should be large-eliminating but Lean still makes an eliminator into Prop only

[Mario Carneiro]

The real reason your Vec example doesn't work is because lean doesn't know that imax 1 u <= u

[Mario Carneiro]

here's a way you can check level inequalities:

inductive {u} foo : Sort u
| a : pempty.{imax 1 u} → foo

this succeeds iff you put an expression v for the pempty such that v <= u is true

[Mario Carneiro]

The system given in my paper will validate imax 1 u <= u, because it does case disjunction when it can't make progress on the inequality. Lean doesn't, it uses a known-incomplete set of rewrite rules to normalize universe expressions, so you can get some spuriously rejected examples like this

[Leonard Wiechmann]

here is something else i'm unsure about:
why are only the universe levels of the constructor "arguments" validated and not also the "parameters"?

inductive foo (X: Sort 42): Sort 1
| ctor: foo
-- foo.ctor : Π {X : Type 41}, foo X

the full foo.ctor also takes X, but universe(X) > 1.
i probably don't understand this, because i don't really understand where the <= constraint for arguments comes from in the first place.
is there a somewhat simple answer that's not "because things work out that way, and everything else would be limiting or inconsistent"? maybe some paper that discusses the rationale?

[Mario Carneiro]

Well, it would be inconsistent to have a small type containing an injective copy of a large type

[Mario Carneiro]

like

inductive foo : Type
| ctor : set Type -> foo

Intuitively, this is cantor's paradox, although it doesn't immediately follow. The correct paradox to cite is Girard's paradox

[Mario Carneiro]

For parameters this isn't really what's happening. It's more like we have a construction of an inductive type which depends on some fixed parameters, i.e. a family of inductive constructions. These play the role of constants so you can't use them to pull any funny business

[Mario Carneiro]

In particular, foo is not injective with respect to its parameters. It took a discovered inconsistency in Agda to realize that this had to be the case, but it's pretty obvious if you look at your foo that it has to be noninjective

[Mario Carneiro]

You can't prove it in lean but it is consistent for foo X = unit for all values of X

[Leonard Wiechmann]

Mario Carneiro said:

Well, it would be inconsistent to have a small type containing an injective copy of a large type

ok, this seems to make sense:

inductive Trojan : Type
| intro (soldier: Type) : Trojan

def extract: Trojan -> Type :=
λ t, Trojan.rec (λ soldier, soldier) t

-- this is *effectively* `Type -> nat`, but it's type is Type, which is paradoxical.
def troy: Trojan -> nat :=
λ t, (λ soldier, ...) (extract t)

[Leonard Wiechmann]

Mario Carneiro said:

For parameters this isn't really what's happening. It's more like we have a construction of an inductive type which depends on some fixed parameters, i.e. a family of inductive constructions. These play the role of constants so you can't use them to pull any funny business

this seems to intuitively make sense, because the "callsite" also needs to know about the parameters (and thus their Sorts). so you can't do funny extraction business.

[Leonard Wiechmann]

the last 2, I don't really understand:
1: what does foo is not injective wrt its parameters mean? is there a link to said agda inconsistency?
2: what does foo X = unit mean? guessing this refers to my foo from above. inductive foo (X: Sort 42) : unit doesn't make sense, because unit is not a sort.

[Mario Carneiro]

Leonard Wiechmann said:

what does foo is not injective wrt its parameters mean? is there a link to said agda inconsistency?

Agda inconsistency: https://coq-club.inria.narkive.com/iDuSeltD/agda-with-the-excluded-middle-is-inconsistent
Injectivity here is saying that foo X = foo Y -> X = Y, i.e. foo is injective as a function on types

[Mario Carneiro]

This is not possible because there are too many possible values of X : Sort 42 compared to the number of values of foo X : Type, i.e. it's essentially a cardinality constraint

[Mario Carneiro]

When I say foo X = unit, I mean that you could add the axiom axiom foo_is_unit (X) : foo X = unit and the resulting system would still be consistent. (You can already prove that foo X ≃ unit using the way it has been defined, but type equalities are almost never provable in lean. This non-injectivity example is a rare case where you can actually prove an equality of types

[Leonard Wiechmann]

Mario Carneiro said:

When I say foo X = unit, I mean that you could add the axiom axiom foo_is_unit (X) : foo X = unit and the resulting system would still be consistent. (You can already prove that foo X ≃ unit using the way it has been defined, but type equalities are almost never provable in lean. This non-injectivity example is a rare case where you can actually prove an equality of types

oh, I see. because foo is basically unit, except with a parameter.

[Leonard Wiechmann]

Mario Carneiro said:

Leonard Wiechmann said:

what does foo is not injective wrt its parameters mean? is there a link to said agda inconsistency?

Agda inconsistency: https://coq-club.inria.narkive.com/iDuSeltD/agda-with-the-excluded-middle-is-inconsistent
Injectivity here is saying that foo X = foo Y -> X = Y, i.e. foo is injective as a function on types

ok, awesome, thanks! i'll check it out once i've got some time.