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