Zulip Chat Archive

Stream: maths

Topic: Can a constructor in an inductive family take in an index


view this post on Zulip Golol (Oct 18 2020 at 09:59):

Let's say I have an inductive family

inductive vector (α : Type u) :   Type u
| nil  : vector 0
| succ : Π n, vector n  vector (n + 1)

I found that the constructors of an inductive family indexed over \y should have type

 foo.constructor : Π (a : α) (b : β), foo a t

, where t_i : \y.
So the constructors does not take arguments from \y, the indices.
But it seems like in the above example succ depends on n. What's going on here?
(I got my information about the constructur from https://leanprover.github.io/reference/declarations.html 4.5)

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:04):

the indices in that description are the tᵢ, while additional constructor arguments are (b : βᵢ). The tᵢ are terms in terms of the a and b arguments, and in particular you are allowed to just use a constructor argument as the value of an index

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:07):

In this case, set (a : α) to (α : Type u), (b : βᵢ) to (n : nat) (_ : vector n), and tᵢ to n + 1 to type vector.succ

view this post on Zulip Golol (Oct 18 2020 at 10:11):

As I understand it (b : \b_i) should be a telescope in the context of (a : \a) and (vector : Π (n : Nat), Sort u),
but then none of the types \b_i,j can be nat?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:11):

nat is valid in the empty context

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:12):

the environment is a global parameter on the typing judgment

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:12):

and it supplies the set of well typed constants, such as nat

view this post on Zulip Golol (Oct 18 2020 at 10:12):

because it is in some sense globally defined?
What if instead of nat the index family was be a type which is not valid in the empty context?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:12):

then it would be a parameter to the inductive type, like (α : Type u)

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:13):

and you would still be able to use it in the betas

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:14):

alternatively, it could be neither, but you could introduce it as a constructor argument, like this:

inductive vector : Π (α : Type u),   Type u
| nil  : Π (α : Type u), vector 0
| succ : Π (α : Type u) n, vector n  vector (n + 1)

view this post on Zulip Golol (Oct 18 2020 at 10:15):

That's surprising to me

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:15):

This is actually not valid though, it violates universe level restrictions

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:15):

you would have to do this instead

inductive vector : Π (α : Type u),   Type (u + 1)
| nil  : Π (α : Type u), vector 0
| succ : Π (α : Type u) n, vector n  vector (n + 1)

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:15):

which part is surprising?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:18):

Here's a version of vector that uses a local variable instead of the global constant nat:

universe u
inductive vector'
  (Nat : Type)
  (zero : Nat)
  (succ : Nat  Nat)
  (α : Type u) : Nat  Type u
| nil : vector' zero
| cons :  n : Nat, vector' n  vector' (succ n)

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:19):

you should think of the parameters as being stuck to the left of all the visible arguments to the constructor

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:20):

so the types of nil and cons are allowed to refer to those parameters

view this post on Zulip Golol (Oct 18 2020 at 10:20):

well I'm trying to understand what exactly makes inductive families necessary, basically why is it

inductive vector : (A : Type u) : nat -> Type (u+1)

and not

inductive vector :  (A : Type u) (n : nat) : Type(u+1)

Then I figured the crucial difference must be how A and n can be used as arguments in the constructor, noticing that a constructor can set the type of its output according to a fixed index t_i, but can not take indices as inputs itself, while it can take arguments of type A.
But the difference in needing a family seems to be about the question if the index Type is in the empty context?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:21):

Yes, that's right. Logically, the indices are the things that are "allowed to change" in application of the constructors

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:22):

Note that Nat is still not allowed to change in vector', because it is a parameter not an index

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:22):

So parameters are much more like constants in that respect

view this post on Zulip Golol (Oct 18 2020 at 10:22):

Mario Carneiro said:

Here's a version of vector that uses a local variable instead of the global constant nat:

universe u
inductive vector'
  (Nat : Type)
  (zero : Nat)
  (succ : Nat  Nat)
  (α : Type u) : Nat  Type u
| nil : vector' zero
| cons :  n : Nat, vector' n  vector' (succ n)

Okay now this seems much more like I would imagine things work... you just put the indices before the colon too.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:23):

Well the index Nat -> is still right of the colon

view this post on Zulip Golol (Oct 18 2020 at 10:24):

yea but now that it is also on the left it feels more acceptable for me to use it for constructor arguments :D

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:24):

You should imagine that you are in a giant context of pis introducing all the definitions in the environment

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:25):

This doesn't quite work out formally though, because definitions in the environment can be universe polymorphic and pis can't

view this post on Zulip Golol (Oct 18 2020 at 10:28):

inductive vector : Π (α : Type u),   Type (u + 1)
| nil  : Π (α : Type u), vector 0
| succ : Π (α : Type u) n, vector n  vector (n + 1)

Is this an inductive type or an inductive family? If it is an inductive type, how can you specify vector 0 in the definition of nil.
As I thought for an inductive type he nil should be sort of a function like \Pi (a : \a) (n : nat) : vector a n.
Thanks a lot for the help btw!

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:29):

Well there isn't much difference between those, lean only has one thing. If you mean does it have any indices, yes it has two

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:30):

The full type of nil there is vector.nil : Π (α : Type u), @vector α 0, which in this case is the same as the visible type because there are no parameters to adjoin

view this post on Zulip Golol (Oct 18 2020 at 10:31):

Ah, I was trying to find an example of inductive families being a strict extension to the concept of inductive type. Are they internally the same thing? inductive families are just an inductive type that we interpret in a bit of a different way?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:32):

it's the other way around; the core concept is an inductive which can have m parameters and n indices; we would usually call that an inductive family if n > 0 and an inductive type if n = 0

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:34):

It might help to look at https://gist.github.com/digama0/ff92084b58a8e669bb421829fcd04f55#file-induction-lean-L22-L47 , which is the definition of an inductive type that is "maximally general" in the sense that all other inductive types can be defined in terms of it

view this post on Zulip Golol (Oct 18 2020 at 10:35):

what the heck is that sorcery

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:38):

  variables {α : Sort i} {β : Sort j} {ξ : β  Sort k}
    (p : β  α) (π : Π (b : β), ξ b  α)
  inductive ind : Π (a : α), Sort (max j k l 1)
  | intro (b : β) : (Π (x : ξ b), ind (π b x))  ind (p b)

There is exactly one of each kind of thing going on in an inductive type (except parameters, which just go along for the ride). (a : α) is the indices of the family; (b : β) are the nonrecursive arguments to the constructor; p is the mapping from constructor arguments to indices. We haven't talked about recursive arguments but ξ is the domain of the recursive calls and π is the mapping to indices in those recursive calls

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:39):

there is an example further down showing how nat can be defined using ind

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:40):

It's useful to have something like this because it means that lean doesn't need infinitely many axioms (the inductive types), you can get the whole lot with just one very general inductive type

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:41):

My thesis spells out the details behind this construction a bit more

view this post on Zulip Golol (Oct 18 2020 at 10:59):

Can I find your thesis online?
I suppose it's probably not necessary to understand induction to this depth to get how vector works, but I always feel like I'm not getting it if I don't know the type of every object and why things can't be written in a different way.

view this post on Zulip Mario Carneiro (Oct 18 2020 at 10:59):

https://github.com/digama0/lean-type-theory/releases/tag/v1.0

view this post on Zulip Mario Carneiro (Oct 18 2020 at 11:00):

The precise rules for inductives are in chapter 2, the reduction to W types (aka ind above) is in chapter 5

view this post on Zulip Golol (Oct 18 2020 at 12:09):

I'll try to read chapter 2. One thing is a bit mysterious me so far: What would a specification be in practice in lean?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 12:18):

You mean an inductive specification, the spec judgment from the paper?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 12:19):

That would be the stuff after the first line of an inductive command:

| nil  : Π (α : Type u), vector 0
| succ : Π (α : Type u) n, vector n  vector (n + 1)

view this post on Zulip Mario Carneiro (Oct 18 2020 at 12:20):

This would get translated to the spec

(nil  : Π (α : Type u), vector 0) +
(succ : Π (α : Type u) n, vector n  vector (n + 1)) +
0

in the notation of the paper

view this post on Zulip Mario Carneiro (Oct 18 2020 at 12:21):

and the full vector type would be translated to

def vector :=
μ (vec : Π (α : Type u),   Type (u + 1)),
(nil  : Π (α : Type u), vec 0) +
(succ : Π (α : Type u) n, vec n  vec (n + 1)) +
0

view this post on Zulip Mario Carneiro (Oct 18 2020 at 12:22):

where μ is a binder that represents the inductive command (you won't find it in standard lean)

view this post on Zulip Marc Huisinga (Oct 18 2020 at 12:22):

some more examples in the notation of the paper:
image.png

view this post on Zulip Golol (Oct 18 2020 at 13:43):

I am not familiar with lambda-mu calculus, what would be an intuition for what mu does?

view this post on Zulip Golol (Oct 18 2020 at 13:48):

It seems to collect the type former and the specification together into one object

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:50):

It's another type former like pi. Intuitively, it has the type (Type -> Type) -> Type and gets the least fixed point of the passed in type functor

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:51):

it's not the same mu as the lambda mu calculus

view this post on Zulip Mario Carneiro (Oct 18 2020 at 13:52):

It's this mu -> https://en.wikipedia.org/wiki/Recursive_data_type#Theory

view this post on Zulip Golol (Oct 18 2020 at 14:01):

Okay hm, I'm imagining it as declaring that a type former together with a specification are now one object with the name mu t : F . K

view this post on Zulip Mario Carneiro (Oct 18 2020 at 14:07):

yes, that's right. K describes the actual form of the inductive type, and mu t : F. K is the inductive type so defined (and c_(mu t : F. K) and rec_(mu t : F. K) are the constructor and recursor for the type)


Last updated: May 18 2021 at 08:14 UTC