Rank-polymorphic fmap on Lists

Stream: lean4

[Ioannis Konstantoulas]

This question came up in a recent Lean thread on HN. A user asked if Lean supports list comprehensions; the main motivation is as follows: with list comprehensions, for a k-ary function, the notation

[ Function Arguments | arg_1 <-List_1 ... arg_k List_k ]

works irrespective of the "rank" k; this is very convenient for numerical functions with many arguments. Do we have something like this? If not, is it easy to code such variadic notation?

[Adam Topaz]

You can do this with do notation quite easily, I think…

[Ioannis Konstantoulas]

It is definitely doable, but a one-liner polymorphic notation would be much nicer. By the way, I yanked the terminology "rank polymorphism" from array languages, and the programmers using them have excellent arguments for its utility.

[Adam Topaz]

import Mathlib.Data.List.Basic

example (L1 L2 L3 : List ℕ) (f : ℕ → ℕ → ℕ → α) : List α := do
  let a ← L1
  let b ← L2
  let c ← L3
  return f a b c

[Adam Topaz]

You can put those on one line with ; if you really want a one-liner.

[Eric Wieser]

(to be clear, that is (do let a ← L1; let b ← L2; let c ← L3; return f a b c))

[Eric Wieser]

Though you can also write the even shorter do return f (← L1) (← L2) (← L3) which de-sugars to the above

[Adam Topaz]

Even this works:

example (L1 L2 L3 : List ℕ) (f : ℕ → ℕ → ℕ → α) : List α :=
  return f (← L1) (← L2) (← L3)

[Adam Topaz]

Lean4 is magic.

[James Gallicchio]

note that this does only work for List, while the do for-in notation works for lots more types. but there are generic ways to get the same List-like behavior with other types, it just requires mac's itertools or my leancolls :P

[Eric Wieser]

@Adam Topaz, what's going on with the lack of do there?

[Adam Topaz]

return does more than just pure

[James Gallicchio]

i don't know if it's .. desirable.......... that the one without do works, but it's certainly interesting that it does!

[Ioannis Konstantoulas]

The return trick is fantastic.

[Mario Carneiro]

James Gallicchio said:

i don't know if it's .. desirable.......... that the one without do works, but it's certainly interesting that it does!

Desirability aside, it is deliberate, return is a term constructor that automatically acts like do return

[Jannis Limperg]

FYI, return also short-circuits. E.g. a return in a for loop ends the loop. So it's really more like C's return than Haskell's.