Zulip Chat Archive
Stream: new members
Topic: List Nat versus "List Nat: Type (max o m.2332) ?
Omri Schwarz (Dec 01 2024 at 18:33):
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 (Dec 01 2024 at 18:34):
( yes, it's an AOC attempt. Got Python and Haskell running. Now trying Lean. Using Kyle Miller (wave) for the list comprehension.
Kevin Buzzard (Dec 01 2024 at 18:34):
"List.map
wants to eat a function but you fed it a list"
Omri Schwarz (Dec 01 2024 at 18:37):
So I'm using the comprehension wrong.
Kevin Buzzard (Dec 01 2024 at 18:37):
Your syntax used in match1
is incomprehensible to me, if that helps
Kevin Buzzard (Dec 01 2024 at 18:38):
You seem to be using several things that aren't actually things in lean
Kevin Buzzard (Dec 01 2024 at 18:39):
eg "for"
Omri Schwarz (Dec 01 2024 at 18:39):
The comprehension is defined here: https://github.com/leanprover-community/lean4-samples/tree/main/ListComprehension
Omri Schwarz (Dec 01 2024 at 18:39):
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 (Dec 01 2024 at 18:40):
Oh ok, "for" is defined in that file.
Omri Schwarz (Dec 01 2024 at 18:40):
(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 (Dec 01 2024 at 18:44):
Well I guess now we can understand the error. docs#List.map
Kyle Miller (Dec 01 2024 at 18:45):
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 (Dec 01 2024 at 18:46):
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 (Dec 01 2024 at 18:46):
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 (Dec 01 2024 at 18:48):
now it all compiles! Thanks, all
Kyle Miller (Dec 01 2024 at 18:53):
(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 (Dec 01 2024 at 19:36):
Can you add a delta%
annotation into the macro to ensure the generated term uses map
?
Last updated: May 02 2025 at 03:31 UTC