# Zulip Chat Archive

## Stream: new members

### Topic: How to make Vec polymorphic over the universe levels?

#### Marko Grdinić (Nov 01 2019 at 13:26):

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 (Nov 01 2019 at 13:54):

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

#### Marko Grdinić (Nov 01 2019 at 13:57):

Thanks.

#### Marko Grdinić (Nov 01 2019 at 14:15):

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 (Nov 01 2019 at 14:17):

you need to let `n`

be part of the recursion

#### Marko Grdinić (Nov 01 2019 at 14:18):

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ć (Nov 01 2019 at 14:34):

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ć (Nov 01 2019 at 14:35):

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 (Nov 01 2019 at 14:35):

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

?

#### Marko Grdinić (Nov 01 2019 at 14:37):

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ć (Nov 01 2019 at 14:38):

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

#### Marko Grdinić (Nov 01 2019 at 15:43):

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 (Nov 01 2019 at 15:45):

yeah the type of `f`

is wrong

#### Kenny Lau (Nov 01 2019 at 15:45):

the type of `f`

depends on `P`

(yay for dependent type theory) but you changed `P`

#### Marko Grdinić (Nov 01 2019 at 15:47):

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 (Nov 01 2019 at 15:50):

also shouldn't you apply `f`

?

#### Kenny Lau (Nov 01 2019 at 15:51):

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

?

#### Kenny Lau (Nov 01 2019 at 15:51):

(deleted)

#### Marko Grdinić (Nov 01 2019 at 15:53):

also shouldn't you apply f?

That would be the `(f s x)`

part.

#### Kenny Lau (Nov 01 2019 at 15:53):

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

right

#### Kenny Lau (Nov 01 2019 at 15:55):

ok so here's `list.foldl`

:

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

#### Kenny Lau (Nov 01 2019 at 15:55):

lemme translate that

#### Kenny Lau (Nov 01 2019 at 15:57):

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 (Nov 01 2019 at 15:58):

Maybe `f`

shouldn't take `n`

as implicit var?

#### Johan Commelin (Nov 01 2019 at 15:59):

And can't the `n`

in the second argument to `@foldl`

be inferred from the type of `xs`

?

#### Marko Grdinić (Nov 01 2019 at 16:05):

@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ć (Nov 01 2019 at 16:06):

I mean, creating an `array`

that way.

#### Marko Grdinić (Nov 01 2019 at 16:17):

#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ć (Nov 01 2019 at 16:24):

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ć (Nov 01 2019 at 16:29):

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

#### Marko Grdinić (Nov 02 2019 at 08:42):

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.

Last updated: May 08 2021 at 09:11 UTC