## Stream: maths

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

#### 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)

#### 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

#### 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

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

#### Mario Carneiro (Oct 18 2020 at 10:11):

nat is valid in the empty context

#### Mario Carneiro (Oct 18 2020 at 10:12):

the environment is a global parameter on the typing judgment

#### Mario Carneiro (Oct 18 2020 at 10:12):

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

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

#### Mario Carneiro (Oct 18 2020 at 10:12):

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

#### Mario Carneiro (Oct 18 2020 at 10:13):

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

#### 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)


#### Golol (Oct 18 2020 at 10:15):

That's surprising to me

#### Mario Carneiro (Oct 18 2020 at 10:15):

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

#### 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)


#### Mario Carneiro (Oct 18 2020 at 10:15):

which part is surprising?

#### 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)


#### 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

#### Mario Carneiro (Oct 18 2020 at 10:20):

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

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

#### 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

#### 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

#### Mario Carneiro (Oct 18 2020 at 10:22):

So parameters are much more like constants in that respect

#### 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.

#### Mario Carneiro (Oct 18 2020 at 10:23):

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

#### 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

#### 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

#### 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

#### 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!

#### 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

#### 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

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

#### 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

#### 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

#### Golol (Oct 18 2020 at 10:35):

what the heck is that sorcery

#### 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

#### Mario Carneiro (Oct 18 2020 at 10:39):

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

#### 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

#### Mario Carneiro (Oct 18 2020 at 10:41):

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

#### 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.

#### Mario Carneiro (Oct 18 2020 at 10:59):

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

#### 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

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

#### Mario Carneiro (Oct 18 2020 at 12:18):

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

#### 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)


#### 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

#### 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


#### 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)

#### Marc Huisinga (Oct 18 2020 at 12:22):

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

#### Golol (Oct 18 2020 at 13:43):

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

#### Golol (Oct 18 2020 at 13:48):

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

#### 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

#### Mario Carneiro (Oct 18 2020 at 13:51):

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

#### Mario Carneiro (Oct 18 2020 at 13:52):

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

#### 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

#### 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