Style RFC: prefer do notation in monadic code

Stream: mathlib4

[Thomas Murrills]

I’d like to propose documenting a style preference for do notation over Haskell-style monadic operators like >>=.

As far as I can tell, we already do this for the most part, but haven’t written it down. I think using do notation helps make code more readable and maintainable. :)

There are a couple of Haskell-style operators we do use occasionally in specific circumstances, like <$>, boolean monadic operators, and occasionally <|>.

My proposal would be to mention those, and allow some discretion on the part of the contributor/reviewer to use one of these common-enough Haskell-style operators when significantly more readable. (Maybe we’d want to discuss which ones exactly would be allowed.)

It’s been mentioned that we should also have a reference for Haskell-style monadic notation, and we could include this together with their do translations for those used to Haskell-style notation. (Possibly this should info should be in the docstrings for the notation as well, but that’s a separate topic.) I think this is a good idea! We could link to it from this section of the style guide.

Up to details, does this sound reasonable?

[Michael Rothgang]

I personally am in favour: I don't come from a Haskell background, and do notation is significantly more readable to me.

[Eric Wieser]

Note that in theory <$> and <*> notation can express implementations that are faster than the >>= generated by donotation

[Eric Wieser]

Eg <$> on an array monad can preallocate up front, and on a state monad it can in theory elide a reference count

[Thomas Murrills]

Interesting!

in theory

Do they? :eyes:

[Thomas Murrills]

If so—or even if they might confer an advantage over do in the future—it would, imo, make sense to allow these specific combinators, especially in performance-critical pieces of code.

[Thomas Murrills]

(But I’d like to distinguish them from the ones which don’t! :grinning_face_with_smiling_eyes:)

[Eric Wieser]

Attempted test-case

import Batteries

def a : Array Nat := Array.replicate 10000000 1

instance : Monad Array where
  bind x f := Array.flatMap f x
  pure x := #[x]
  map := Array.map

set_option trace.profiler true in
#eval ((2 * ·) <$> a).size

set_option trace.profiler true in
#eval Array.size (return 2 * (← a))

[Eric Wieser]

Admittedly seems very marginal

[Thomas Murrills]

(I’ll also link the thread #lean4 > Alternative and do-notation as well as #lean4 > Applicative and do-notation here for good measure)