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)


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

(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):

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.