Zulip Chat Archive

Stream: new members

Topic: Named type params (`inductive`)


Max Nowak (May 19 2022 at 09:57):

I would have expected the following two inductive definitions to be identical. The only difference is that I assign ohno as a name to the vector length parameter and simply never use it. Or so I thought. Apparently there is a difference and Lean4 forces me to use ohno. Why is this distinction important? I am hoping this will bring me insights into DTT and Lean4's inner workings :D

inductive Vec (α: Type u) (ohno: Nat) : Type u
  | nil  : Vec α 0 -- inductive datatype parameter mismatch 0 expected ohno
  | cons : α -> Vec α n -> Vec α (n+1)

inductive Vect (α: Type u) : Nat -> Type u
  | nil  : Vect α 0
  | cons : α -> Vect α n -> Vect α (n+1)

Cameron Torrance (May 19 2022 at 10:15):

Lean automatically fills in parameters left of the colon, if you want to use a variable as an index put it to the right.

Kevin Buzzard (May 19 2022 at 10:15):

Is the answer to this simply that the very syntax for inductive types depends on what's on either side of the colon?

Max Nowak (May 19 2022 at 10:20):

Thanks for the answers :).
What do you mean with using a variable as an index?

Cameron Torrance (May 19 2022 at 10:23):

I'm not a computer scientist but I think the distinction is that a parameter only says what kinds of stuff live in your type whereas indices control the structure of the type.
edit: I said this wrong, this should help https://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices

Max Nowak (May 19 2022 at 10:35):

Ahhhhh, yeah that makes so much sense now!
The key distinction is then that parameters need to be uniform everywhere, but indices can differ in each constructor, because, well, we can use them to fiddle with which constructors are viable in e.g. pattern matching.

Max Nowak (May 19 2022 at 10:36):

Thank you :)


Last updated: Dec 20 2023 at 11:08 UTC