Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Marko Grdinić (Nov 01 2019 at 13:57):

Thanks.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Nov 01 2019 at 14:17):

you need to let n be part of the recursion

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Nov 01 2019 at 14:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:45):

yeah the type of f is wrong

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:45):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:50):

also shouldn't you apply f?

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:51):

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

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:51):

(deleted)

view this post on Zulip Marko Grdinić (Nov 01 2019 at 15:53):

also shouldn't you apply f?

That would be the (f s x) part.

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:53):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 01 2019 at 15:55):

lemme translate that

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 01 2019 at 15:58):

Maybe f shouldn't take n as implicit var?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Marko Grdinić (Nov 01 2019 at 16:06):

I mean, creating an array that way.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Marko Grdinić (Nov 02 2019 at 08:42):

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.


Last updated: May 08 2021 at 09:11 UTC