How to make Vec polymorphic over the universe levels?

Stream: new members

[Marko Grdinić]

inductive Vec (α : Type*) : ℕ → Type*
| nil : ∀ {n : ℕ}, Vec n
| cons : ∀ {n : ℕ}, α → Vec n → Vec (n + 1)

Vec.lean:1:0: error
universe level of type_of(arg #3) of 'Vec.cons' is too big for the corresponding inductive datatype

What do I do here?

[Kenny Lau]

universes u

inductive Vec (α : Type u) : ℕ → Type u
| nil : ∀ {n : ℕ}, Vec n
| cons : ∀ {n : ℕ}, α → Vec n → Vec (n + 1)

[Marko Grdinić]

Thanks.

[Marko Grdinić]

universes a b c

inductive Vec (α : Type a) : ℕ → Type a
| nil : ∀ {n : ℕ}, Vec n
| cons : ∀ {n : ℕ}, α → Vec n → Vec (n + 1)

variables {α : Type a} {β : Type b}

def Vec.foldl {n : ℕ} (s : β) : Vec α n → β
| (Vec.nil x) := sorry
| (Vec.cons w e) := sorry

Vec.lean:11:17: error
ill-formed match/equation expression

I am having trouble not necessarily how to implement foldl, but just figuring out how to write out the pattern. It is not 3 or 4 arguments that it wants. It is not even something like (@Vec.cons n w e r). Just how am I supposed to destructure Vec here?

[Kenny Lau]

you need to let n be part of the recursion

[Marko Grdinić]

def Vec.foldl (s : β) : ∀ {n : ℕ}, Vec α n → β
| n (Vec.nil x) := sorry
| n (Vec.cons e r) := sorry

Ah, I see. Thanks again.

[Marko Grdinić]

def Vec.foldl (f : α → β → β) : ∀ {n : ℕ}, β → Vec α n → β
| n s (Vec.nil _) := s
| n s (Vec.cons x xs) := Vec.foldl (f x s) xs

Vec.lean:11:4: error
equation compiler failed to prove equation lemma (workaround: disable lemma generation using `set_option eqn_compiler.lemmas false`)

Sorry, I need a hand once again. What does this error mean?

[Marko Grdinić]

def Vec.foldl (f : α → β → β) : ∀ {n : ℕ}, β → Vec α n → β
| n s (Vec.nil _) := s
| (n + 1) s (Vec.cons x xs) := Vec.foldl (f x s) xs

Ah, I see. Nevermind. I did it wrong the first time around.

[Kenny Lau]

oh shouldn't you have | nil : Vec 0?

[Marko Grdinić]

open Vec

def Vec.foldl (f : α → β → β) : ∀ {n : ℕ}, β → Vec α n → β
| n s (nil _) := s
| (n + 1) s (cons x xs) := Vec.foldl (f x s) xs

Do you mean something like this, or are you referring to the fact that there is an extra argument for some reason? If it is the last one, I have no idea.

[Marko Grdinić]

Ah, you mean in the type definition? Ah, yes, well spotted. Yeah, that is what it should be.

[Marko Grdinić]

universes a b c

inductive Vec (α : Type a) : ℕ → Type a
| nil : Vec 0
| cons : ∀ {n : ℕ}, α → Vec n → Vec (n + 1)

variables {α : Type a} {β : Type b}

open Vec

def Vec.foldl : ∀ (P : ℕ → Type a) {n : nat}
    (f : ∀ {n}, P n → α → P (n+1)) (s : P 0)
    (l : Vec α n), P n
| P n f s (nil _) := s
| P (n+1) f s (cons x xs) := Vec.foldl (fun n, P (n+1)) f (f s x) xs

Vec.lean:15:29: error
type mismatch at application
  Vec.foldl (λ (n : ℕ), P (n + 1)) f
term
  f
has type
  P ?m_1 → α → P (?m_1 + 1)
but is expected to have type
  Π {n : ℕ}, (λ (n : ℕ), P (n + 1)) n → α → (λ (n : ℕ), P (n + 1)) (n + 1)

What is this error now?

[Kenny Lau]

yeah the type of f is wrong

[Kenny Lau]

the type of f depends on P (yay for dependent type theory) but you changed P

[Marko Grdinić]

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

I am trying to translate the Agda version into Lean. Where did I make a mistake?

[Kenny Lau]

also shouldn't you apply f?

[Kenny Lau]

in maths what is foldl f (x::xs)?

[Kenny Lau]

(deleted)

[Marko Grdinić]

also shouldn't you apply f?

That would be the (f s x) part.

[Kenny Lau]

so foldl (+) 0 (a::b::c::nil) = ((a+b)+c)+0 right

[Kenny Lau]

ok so here's list.foldl:

@[simp] def foldl (f : α → β → α) : α → list β → α
| a []       := a
| a (b :: l) := foldl (f a b) l

[Kenny Lau]

lemme translate that

[Kenny Lau]

universes u v

inductive Vec (α : Type u) : ℕ → Type u
| nil : Vec 0
| cons : ∀ {n : ℕ}, α → Vec n → Vec (n + 1)

variables {α : Type u}

namespace Vec

@[elab_as_eliminator]
def foldl : Π (P : ℕ → Type v) {n : ℕ}
  (f : Π {n}, P n → α → P (n+1)) (s : P 0)
  (l : Vec α n), P n
| P 0     f s (nil α)     := s
| P (n+1) f s (cons x xs) := @foldl _ n (λ n, @f (n+1)) (f s x) xs

end Vec

[Johan Commelin]

Maybe f shouldn't take n as implicit var?

[Johan Commelin]

And can't the n in the second argument to @foldl be inferred from the type of xs?

[Marko Grdinić]

@Kenny Lau
I am skeptical that your version is correct. Is incrementing n as it is passed to f really the right choice here? As you go from left to right over the vector, would that not make n constant in f? Imagine if you were iterating in an array that way.

[Marko Grdinić]

I mean, creating an array that way.

[Marko Grdinić]

#eval @foldl nat (fun i, nat) 3 (fun n s a, s + n) 0 (cons 11 (cons 11 (cons 11 (@nil nat))) -- 3

Hmmm, it is right.

[Marko Grdinić]

def foldl : ∀ (P : ℕ → Type a) {n : nat}
    (f : ∀ {n}, P n → α → P (n+1)) (s : P 0)
    (l : Vec α n), P n
| P 0 f s (nil _) := s
| P (n+1) f s (cons x xs) := foldl (fun n, P (n+1)) (λ n, @f (n+1)) (@f 0 s x) xs

Uf, I got tricked by Agda. I did not expect at all that this would be the true form of the function. Agda is really doing some sleight of hand to pass the correct implicit argument to n ⊕ x. I wonder how it is doing that?

[Marko Grdinić]

Well, thank you for the help. I'll try asking on SO about this to satisfy my curiosity.

[Marko Grdinić]

https://stackoverflow.com/questions/58662725/how-is-agda-inferring-the-implicit-argument-to-vec-foldl

So it turns out that Agda is doing the same thing as the Lean solution which is a complete surprise to me. I swear I am not too dumb to make foldl. It is just that between the mistaken assumption that f should be passed as is, and the unintelligible type error, I thought that Lean was doing something crazy.