Lean Manual: Monads documentation question/suggestion

Stream: lean4

[Tom]

Hi,

I've been reading through the writeup on Monads in the Lean manual (Thanks @Chris Lovett !), and it's really great. I'd like to make a small observation about the Functor section: The original Haskell document uses Functors from the very beginning, because even the initial examples (such as lists and options) all use fmap, which uses the Functor typeclass.

However, to the best of my understanding, all the initial examples in the Lean manual do not use a functor. Since they all say things like [1,2,3].map and (some 3).map, my current understanding is that what's happening is the map functions are being found via the the type in the namespace of the LHS argument, so here it's List.map and Option.map rather than via the Functor typeclass instance.

I am not sure if this matters but am curious whether it's worth calling that out for pedagogical reasons. Functor.map doesn't get mentioned until about 3/4 of the way through, and only in relation to the <$> operator.

In my mind, e.g. the two examples

["elephant", "tiger", "giraffe"].map (fun s => s.length)

and

(fun s => s.length) <$> ["elephant", "tiger", "giraffe"]

are different because they find the map function in very different ways.

(Disclaimer: I'm a complete Lean noob so I don't know which way's up, so please ignore if the above doesn't make sense)

[Jason Rute]

Functors aside, it is common in Lean to handle notation via type classes. In particular, 0, +, <, <$> are all governed via type classes. If one enters 0 + 0 ≤ 0 that is not the same as Nat.lt (Nat.zero + Nat.zero) Nat.zero but I don't think the user has to think about this at least until they get very advanced. In particular, type classes are set up so that 0 + 0 ≤ 0 is definitionally equal to Nat.lt (Nat.zero + Nat.zero) Nat.zero and ["elephant", "tiger", "giraffe"].map (fun s => s.length) is definitional equal to (fun s => s.length) <$> ["elephant", "tiger", "giraffe"], so both expressions reduce and compute to the same thing.

Moreover if one has a function on general functors, e.g.

def Functor.map_thrice
  [Functor F] (x : F α)
  (f1 : α -> β) (f2 : β -> γ) (f3 : γ -> δ) : F δ :=
f3 <$> f2 <$> f1 <$> x

Then it can be applied to any instance of Functor, e.g.

Functor.map_thrice ["a","bb","ccc"] (String.length) (· + 1) (· * 2)

(Unfortunately, one can't yet write ["a","bb","ccc"].map_thrice although @Sebastian Ullrich said it was a feature they thought about adding.)

[Jason Rute]

As an aside I'd love to see the use of <$> greatly reduced in Lean. If one doesn't have a strong need for the function to be on the left of the map, then one can use |>. instead which is much a more general notational pattern (along with |> and <|) and requires less memory of specific symbols.

["a","bb","ccc"] |>.map (String.length) |>.map (· + 1) |>.map (· * 2)

This is similar to the pattern I used all the time in Scala. (Again, however it would be hard to avoid <$>with arbitrary functors like in my map_thrice example, since even if we have[Functor F] (x : F α) we can't write x.map f yet, but we can write f <$> x.)

[Damiano Testa]

@Jason Rute, thanks for this explanation: I did not know about this subtlety with typeclasses vs direct applications.

Just to make sure that I am following, those Nat.lt are Nat.le, right?

[Jason Rute]

Yes, that is what happens when I hyper-edit my comments. :face_palm: Fixed now.

[Chris Lovett]

So where does this leave us in terms of the Monad Functor documentation. I agree with Tom that technically my examples of calling List.map directly are not technically Functor.map calls, but then again I was kind of glossing over that difference because it is kind of an advanced detail. Also, I didn't technically say that my List.map calls were Functor.map calls, instead I said "List has a specialized version of map defined as follows:` then I showed later on line 90 how that "specialized implementation" can be used to implement the List Functor map operation. So I'm inclined to leave it as is, unless folks really think this is too confusing? How would I fix it exactly?

[Mario Carneiro]

I would leave it mostly uncommented besides saying that [a, b, c].map f and f <$> [a, b, c] are alternate syntaxes for the same thing

[Tom]

@Chris Lovett

Thanks for your reply. I don't know the best way to proceed and you're right, perhaps it is immaterial or not relevant for the audience at this level. If I were to be super picky, I might say something along the lines of

'These structures above have the same "interface" which is generalized/provided by the functor class.'
and show the equivalent functor call.

My main issue was that if I didn't already understand functors, I could be asking "why do I need the instance of Functor, when (most of) the code works without it?"

However, it may also not be worth it, so YMMV.

Thanks!

PS: When I try to copy and paste the code from the examples (both in the VSCode documentation view and directly from a browser), every token is separated by a newline, so I have to do a lot of manual editing after the paste. Do you know how to "fix" that? I don't think there's a magic "copy" button like in TPIL, so right now I'm stuck retyping them. Any suggestions?

[Chris Lovett]

Thanks for the bug report on the code snippets, we do indeed have some missing features in LeanInk. We need to get back the "Copy to clipboard" button and the "Try It" button when inside VS Code. See https://github.com/leanprover/LeanInk/issues/35. In the meantime, I would recommend just going straight to the source code at https://github.com/leanprover/lean4/tree/master/doc/monads and open that folder directly into VS code and all the snippets will just work.

[Chris Lovett]

My main issue was that if I didn't already understand functors, I could be asking "why do I need the instance of Functor, when (most of) the code works without it?"

This is an excellent point and we do need to do a better job of explaining that one. I think it is the case that List.map by itself is fine, it doesn't really need to be associated with the Functor type class. But the Functor type class exists to create the interface to the map function, and establish the base type class for what follows, Applicatives, and Monads. So, at the beginning, yes, you kind of have to be patient. It's like "ok, so you defined the map interface, now what?". Well, why does one define interfaces in any language? Hopefully by the time you are done with the whole chapter you get to the point of thinking, ok, monads a cool, I can see how they are useful, and I can see how Functors were just the beginning of this whole thing which is fine... One thing I've been wondering about is the usage of the term "abstract mathematical structures" instead of just "interface". The former is more mathematical, whereas the latter will make more sense to programmers that are coming to Lean with a background in other programming languages...

[Mario Carneiro]

I'd rather the documentation not muddy up the terminology with names from other languages. We should call them "typeclasses" consistently, say they are introduced with the class keyword, and in the introductory material mention that these are similar to interfaces in Java / C#, concepts in C++, and traits in Rust.

[Mario Carneiro]

"Abstract mathematical structure" isn't a name, it's a descriptor which is not very helpful to anyone other than to hat tip to the fact that we know it's abstract and probably confusing