List Nat versus "List Nat: Type (max o m.2332) ?

Stream: new members

[Omri Schwarz]

Hello, all. I have a quickly plagiarized function that looks like this:

def sum (xs : List Nat) : Nat :=
  xs.foldl (init := 0) (·+·)

def match1 (xs : List Nat ) ( y: Nat) : Nat :=
  y * sum [ y | for a in xs, if a = y]

And the complaint I get is

20:25:
application type mismatch
  List.map xs
argument
  xs
has type
  List Nat : Type
but is expected to have type
  ?m.2300 → List Nat : Type (max 0 ?u.2299)

How do I interpret this message?

[Omri Schwarz]

( yes, it's an AOC attempt. Got Python and Haskell running. Now trying Lean. Using Kyle Miller (wave) for the list comprehension.

[Kevin Buzzard]

"List.map wants to eat a function but you fed it a list"

[Omri Schwarz]

So I'm using the comprehension wrong.

[Kevin Buzzard]

Your syntax used in match1 is incomprehensible to me, if that helps

[Kevin Buzzard]

You seem to be using several things that aren't actually things in lean

[Kevin Buzzard]

eg "for"

[Omri Schwarz]

The comprehension is defined here: https://github.com/leanprover-community/lean4-samples/tree/main/ListComprehension

[Omri Schwarz]

I pasted the syntax clauses to get this:

declare_syntax_cat compClause
syntax "for " term " in " term : compClause
syntax "if " term : compClause

syntax "[" term " | " compClause,* "]" : term

macro_rules
  | `([$t:term |]) => `([$t])
  | `([$t:term | for $x in $xs]) => `(List.map $xs  (λ $x => $t))
  | `([$t:term | if $x]) => `(if $x then [$t] else [])
  | `([$t:term | $c, $cs,*]) => `(List.join [[$t | $cs,*] | $c])

def match1 (xs : List Nat ) ( y: Nat) : Nat :=
  sum [ y | for a in xs, if a = y]

[Kevin Buzzard]

Oh ok, "for" is defined in that file.

[Omri Schwarz]

(natural consequence of first writing an AOC puzzle in Python, then porting to Haskell, then porting to Lean, as being the type to bite off more plagiarism than one can chew
)

[Kevin Buzzard]

Well I guess now we can understand the error. docs#List.map

[Kyle Miller]

Make sure to copy it from https://github.com/leanprover-community/lean4-samples/blob/main/ListComprehension/ListComprehension.lean rather than the readme. It looks like the issue is that List.map has a different argument order.

[Kyle Miller]

I guess List.join has been deprecated in the meantime as well. Here:

declare_syntax_cat compClause
syntax "for " term " in " term : compClause
syntax "if " term : compClause

syntax "[" term " | " compClause,* "]" : term

def List.map' (xs : List α) (f : α → β) : List β := List.map f xs

macro_rules
  | `([$t:term |]) => `([$t])
  | `([$t:term | for $x in $xs]) => `(List.map' $xs (fun $x => $t))
  | `([$t:term | if $x]) => `(if $x then [$t] else [])
  | `([$t:term | $c, $cs,*]) => `(List.flatten [[$t | $cs,*] | $c])

[Kevin Buzzard]

As we can see from the code, you're feeding List.map a list and then a function, but according to the docs it wants to eat a function and then a list

[Omri Schwarz]

now it all compiles! Thanks, all

[Kyle Miller]

(If anyone is wondering why use List.map' rather than simply swap the argument order to the List.map, what I remember is that in practice this helps make sure type information flows from the list to the function's binder rather than the other way.)

[Eric Wieser]

Can you add a delta% annotation into the macro to ensure the generated term uses map?