Can a constructor in an inductive family take in an index

Stream: maths

[Golol]

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]

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]

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

[Golol]

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]

nat is valid in the empty context

[Mario Carneiro]

the environment is a global parameter on the typing judgment

[Mario Carneiro]

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

[Golol]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

That's surprising to me

[Mario Carneiro]

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

[Mario Carneiro]

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]

which part is surprising?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Golol]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

So parameters are much more like constants in that respect

[Golol]

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]

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

[Golol]

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]

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

[Mario Carneiro]

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

[Golol]

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]

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]

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]

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]

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]

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]

what the heck is that sorcery

[Mario Carneiro]

  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]

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

[Mario Carneiro]

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]

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

[Golol]

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]

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

[Mario Carneiro]

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

[Golol]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Marc Huisinga]

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

[Golol]

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

[Golol]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Golol]

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]

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)