Style bikeshed: `<| ←` vs. `<|←`

Stream: mathlib4

[Thomas Murrills]

Currently, the style guidelines imply we ought to put spaces around infix notation, and indeed the prevailing style for the combo in the title is <| ←.

But—despite that!—I'd like to discuss a possible carve out in the style guidelines in favor of <|←. I think it adds a good amount of readability in meta code and other programming in monads. Compare e.g.

let e ← whnf <| ← instantiateMVars <| ← inferType e

let e ← whnf <|← instantiateMVars <|← inferType e

<|← becomes a sort of intuitive idiom for "monadic function application", saving on the number of discrete "tokens" your eye parses, while still being interpretable—especially in fonts that ligature <| into a triangle, which I imagine many programmers use.
E.g.

When a lot of code like this is on the page, I find pushing <| and ← together helps me focus on the more salient terms in between the interstitial notation instead of the notation itself.

But, I've used <|← consistently for a while, so maybe I just like it because I'm used to it! :) Is it really more readable, or is it "just me"?

[suhr]

Isn't this just =<<?

[Thomas Murrills]

Maybe, but I believe we stylistically try to avoid monadic notations like that when possible in Mathlib in favor of simpler do-block notation.

[Thomas Murrills]

Actually, is that written down anywhere? If not, should it be? :thinking: I certainly feel it's the style, but I'm not sure it's stated anywhere. (Sometimes I see <$>, but very rarely >>=, its reversed variant, or other similar monadic notation.) EDIT: See #mathlib4 > Style RFC: prefer do notation in monadic code

[Kim Morrison]

I think this is too bike-sheddy. For me it makes zero difference either way.

[Thomas Murrills]

Hmm, that might be a genuine difference in experience between us. It really does have some effect on how my eyes move over the screen/how easily my brain parses code, and it’s frequent enough in the code I look at for me to care; I swear I’m not just bikeshedding for bikeshedding’s sake! :)

(At the same time, I really don’t know how widely shared my experience here is. It might not be widely shared at all! And I recognize it’s pretty niche in absolute terms.)

[Adam Topaz]

I have a personal preference for <| ← foo mostly because I think of ← as being attached to foo as opposed to <|. But I don't think we need to make any guidelines and I agree with:

Kim Morrison said:

I think this is too bike-sheddy. For me it makes zero difference either way.

[Kenny Lau]

does anyone have a list of monadic notations?

[Adam Topaz]

A lot of it (but not all!) mimics Haskell’s ascii art, and I’m sure you can find a useful list from the Haskell side

[Robin Arnez]

I believe the full list is: <$>, <&>, <*, <*>, *>, <|>, >>=, =<<, >=>, <=<, >>, <&&>, <||>

[Kenny Lau]

and what do they do?

[Aaron Liu]

Kenny Lau said:

and what do they do?

functor map <$>, map but with the argument order swapped <&>, seqleft (seq left with right, but throw away left result and keep right result) <*, applicative seq <*>, seqright (seq left with right, but throw away right result and keep left result) *>, alternative orelse <|>, monadic bind >>=, bind but with the argument order swapped =<<, kleisli composition >=>, kleisli composition with the argument order swapped <=<, "and then" operation (monadically run left and then right, keeping right result and discarding left) >>, monadic and (Boolean and but monadic) <&&>, monadic or (Boolean or but monadic) <||>