## Stream: general

### Topic: breaking inductive

#### Leonard Wiechmann (Feb 21 2022 at 14:30):

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 (Feb 21 2022 at 14:32):

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

#### Reid Barton (Feb 21 2022 at 14:32):

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

#### Reid Barton (Feb 21 2022 at 14:34):

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 (Feb 21 2022 at 14:34):

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"?

no

#### Leonard Wiechmann (Feb 21 2022 at 14:36):

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 (Feb 21 2022 at 14:36):

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

#### Reid Barton (Feb 21 2022 at 14:36):

Has nothing to do with universes.

#### Mario Carneiro (Feb 21 2022 at 14:37):

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 (Feb 21 2022 at 14:37):

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

#### Mario Carneiro (Feb 21 2022 at 14:38):

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

#### Leonard Wiechmann (Feb 21 2022 at 14:38):

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 (Feb 21 2022 at 14:39):

It generates the recursor for Prop

#### Leonard Wiechmann (Feb 21 2022 at 14:39):

well, that makes sense :D

#### Mario Carneiro (Feb 21 2022 at 14:39):

that is, it is a small eliminating type

#### Mario Carneiro (Feb 21 2022 at 14:39):

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

#### Leonard Wiechmann (Feb 21 2022 at 14:40):

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

#### Mario Carneiro (Feb 21 2022 at 14:40):

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 (Feb 21 2022 at 14:41):

you need 2 constructors to not be subsingleton, right?

right

or other things

#### Leonard Wiechmann (Feb 21 2022 at 14:42):

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

#### Mario Carneiro (Feb 21 2022 at 14:42):

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 (Feb 21 2022 at 14:44):

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 (Feb 21 2022 at 14:44):

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

#### Mario Carneiro (Feb 21 2022 at 14:46):

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

#### Mario Carneiro (Feb 21 2022 at 14:47):

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 (Feb 21 2022 at 14:49):

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 (Feb 21 2022 at 15:17):

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 (Feb 21 2022 at 17:27):

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

#### Mario Carneiro (Feb 21 2022 at 17:30):

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 (Feb 21 2022 at 17:31):

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 (Feb 21 2022 at 17:32):

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 (Feb 21 2022 at 17:33):

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

#### Leonard Wiechmann (Feb 22 2022 at 13:20):

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 (Feb 22 2022 at 13:21):

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 (Feb 22 2022 at 13:24):

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 (Feb 22 2022 at 13:39):

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 (Feb 22 2022 at 13:40):

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 (Feb 22 2022 at 13:42):

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 (Feb 24 2022 at 11:45):

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 (Feb 24 2022 at 11:45):

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.

Last updated: Dec 20 2023 at 11:08 UTC