inverse of $

Stream: general

[Andrew Ashworth]

is there an inverse of $? (the backwards pipe operator<|) i.e. instead of g (f x) being written as g $ f x I'd like to write f x <| g

[Brendan Zabarauskas]

I though $ was backwards pipe? Do you mean you'd like to write x |> f |> g?

[Brendan Zabarauskas]

(big fan of directional composition/application operators at any rate)

[Andrew Ashworth]

er, maybe it's a forwards pipe? but yes, I'd like to reverse the order that function arguments appear

[Andrew Ashworth]

in fact, I just googled and yeah, seems I have my directions mixed up, whoops

[Brendan Zabarauskas]

To be more precise, I'd also recommend saying 'apply' and 'application' rather than 'pipe', which is a little ambiguous.

[Mario Carneiro]

short answer: no

[Mario Carneiro]

I believe that operator is used for option.lhoare

[Andrew Ashworth]

eughhh. |> and <| have been around for ages to represent reverse and forward function application.... maybe I can steal them back after Lean 4 releases

[Mario Carneiro]

I think that lhoare and rhoare are surprisingly useless operators

[Brendan Zabarauskas]

what on earth is a hoare?

[Mario Carneiro]

I have never seen a use for them

[Mario Carneiro]

as in tony

[Brendan Zabarauskas]

hoare logic?

[Andrew Ashworth]

i don't have a problem with useless library files, but the problem is you can't unset global notation :(

[Brendan Zabarauskas]

Also a big fan of >> and << for composition (as in F#, Elm), but those are often stolen by haskell-like langs for monady stuff. I just say use *> and <* from applicative instead.

[Mario Carneiro]

looks like lhoare and rhoare are not used anywhere in core either

[Mario Carneiro]

rhoare is almost the same as option.guard but its logic is reversed

[Mario Carneiro]

maybe I can get @Sebastian Ullrich to burninate it?

[Andrew Ashworth]

for symmetry reasons I'd vote for that, |> and <| is more pleasant to look at than dollar signs

[Mario Carneiro]

the dollar's not going anywhere though

[Andrew Ashworth]

and whatever arbitrary unicode symbol i would pick to replace <|

[Mario Carneiro]

what about <$?

[Andrew Ashworth]

yea, I know the dollar sign is one character and from haskell

[Mario Carneiro]

that is more obviously related to application

[Mario Carneiro]

I assume <| and |> have something to do with orelse

[Mario Carneiro]

and the hoare things are also orelsey

[Andrew Ashworth]

|> and <| is ocaml notation

[Andrew Ashworth]

does haskell have a <| equiv

[Mario Carneiro]

I assume that haskell has a meaning for every sequence of <= 3 punctuation chars

[Andrew Ashworth]

I can get behind <$ if $ is sticking around

[Johan Commelin]

But don't you want $> ?

[Johan Commelin]

That seems more intuitive to me...

[Johan Commelin]

But then, I've never used OCaml

[Andrew Ashworth]

as in g (f x) would be written f x $> g?

[Johan Commelin]

Yes...

[Johan Commelin]

The > conveys in which way the arguments flow

[Johan Commelin]

Just like in Bash...

[Johan Commelin]

if you write to a file

[Andrew Ashworth]

i can see that some might prefer that, i always thought of it as moving the top function instead of the arguments

[Johan Commelin]

Ok, that also makes sense...

[Mario Carneiro]

I was thinking $ with a reversal, so a backward arrow to indicate that

[Mario Carneiro]

oh, <$ is taken...

[Mario Carneiro]

functor.map_const

[Johan Commelin]

What about $< ?

[Johan Commelin]

(No lean here, atm)

[Andrew Ashworth]

i prefer the bracket to be on the correct side of the dollar sign, haha

[Mario Carneiro]

$< is clear

[Mario Carneiro]

yeah, that's why it's taken :P

[Mario Carneiro]

I guess <$ is named similar to <$>

[Andrew Ashworth]

when lean 4 is released I will have to be very quick and reserve |> and <| as fast as possible in some large library most users install...

[Andrew Ashworth]

since it seems those might have a chance of being deleted anyway

[Andrew Ashworth]

or maybe there's some unicode variant of the eq.subst triangle hanging around

[Mario Carneiro]

there is unicode for everything

[Mario Carneiro]

◁ ?

[Mario Carneiro]

= \lhd

[Mario Carneiro]

but mathematicians are also jockeying for these symbols

[Andrew Ashworth]

this operator is so commonly used I'm boggled nobody has complained about it yet in this chat

[Johan Commelin]

I hope in Lean 4 there will be a way to selectively import notation

[Johan Commelin]

import foo with bar as xyzzy

[Johan Commelin]

Like in python

[Andrew Ashworth]

am I really the first person to miss the dual of $

[Mario Carneiro]

for CS things I prefer ascii because mathematicians won't lower themselves to use them

[Johan Commelin]

lol

[Mario Carneiro]

well, it is obviously redundant...

[Johan Commelin]

@Andrew Ashworth So plug a zero-width char in between, an create a keyboard shortcut to type the 3-char-combo. Or does VScode not render 0-width-chars with 0 width?

[Mario Carneiro]

nooo

[Johan Commelin]

Or use local notation to override the global stuff. I did that with [n].

[Johan Commelin]

Does Lean recognize 0-width space as whitespace?

[Andrew Ashworth]

i guess.. but when people do more actual programming, it's nice to write something like [1..10] |> map f (with the arrow the way Johan likes it)

[Reid Barton]

I was going to say, isn't |> the flipped application?

[Reid Barton]

But in lean, can't you write [1..10].map f?

[Andrew Ashworth]

[1..10] might be some arbitrary expression that spans multiple lines

[Mario Carneiro]

def «te​st» := 1
#print «te​st»

[Mario Carneiro]

it doesn't like it as a space or as an identifier

[Andrew Ashworth]

also I've completely got the application directions mixed up in my head, if I could delete it all I would :)

[Reid Barton]

I don't really see what you gain over using parentheses or a variety of other options

[Johan Commelin]

/me should prove fermаt_lаst_theorem in a couple lines, after importing https://github.com/formalabstracts/formalabstracts/blob/master/fabstract/Wiles_A_and_Taylor_R_FermatLast/fabstract.lean, and some other obscure libraries... :stuck_out_tongue_winking_eye:

[Reid Barton]

The uses I know of for flipped application are when you have left-to-right type inference / overloading resolution (Haskell doesn't have this, Lean might, not sure) or you want the order of effects to be left-to-right (Haskell has >>=)

[Johan Commelin]

No-one will notice that I used a Cyrillic a in fermat

[Reid Barton]

And of course it can be a style thing. One can debate the merits of having more styles available versus having fewer styles available

[Johan Commelin]

Just want to point out that I am a mathematician who loves ascii

[Andrew Ashworth]

it is a little redundant, yes, you can argue field notation, $, and parens should be all you need, for me it's a stylistic issue v0v

[Andrew Ashworth]

it's a bigger deal in F# because as you mentioned type checking is done left-to-right

[Andrew Ashworth]

but it enables you to build up nice looking data transformation definitions that look natural

[Mario Carneiro]

actually the type checking thing is a good point

[Andrew Ashworth]

with no parentheses like you might need with Lean's field notation

[Andrew Ashworth]

actually the type checking thing is a good point

how so?

[Mario Carneiro]

hm, I'm having trouble coming up with an example of a difference from the order change

[Mario Carneiro]

but in theory there should be some differences due to the parse order, which does matter

[Andrew Ashworth]

consider this F# snippet:

let res =
  [ 1 .. 10 ]
  |> List.filter isEven
  |> List.map formatInt

writing this in Lean using field notation is a little cumbersome, and doesn't look as pretty