Zulip Chat Archive

Stream: general

Topic: inverse of $


view this post on Zulip Andrew Ashworth (May 28 2018 at 03:10):

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

view this post on Zulip Brendan Zabarauskas (May 28 2018 at 03:13):

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

view this post on Zulip Brendan Zabarauskas (May 28 2018 at 03:13):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:14):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:15):

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

view this post on Zulip Brendan Zabarauskas (May 28 2018 at 03:16):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:19):

short answer: no

view this post on Zulip Mario Carneiro (May 28 2018 at 03:19):

I believe that operator is used for option.lhoare

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:21):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:21):

I think that lhoare and rhoare are surprisingly useless operators

view this post on Zulip Brendan Zabarauskas (May 28 2018 at 03:22):

what on earth is a hoare?

view this post on Zulip Mario Carneiro (May 28 2018 at 03:22):

I have never seen a use for them

view this post on Zulip Mario Carneiro (May 28 2018 at 03:22):

as in tony

view this post on Zulip Brendan Zabarauskas (May 28 2018 at 03:22):

hoare logic?

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:22):

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

view this post on Zulip Brendan Zabarauskas (May 28 2018 at 03:24):

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.

view this post on Zulip Mario Carneiro (May 28 2018 at 03:24):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:25):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:26):

maybe I can get @Sebastian Ullrich to burninate it?

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:27):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:28):

the dollar's not going anywhere though

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:28):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:28):

what about <$?

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:28):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:29):

that is more obviously related to application

view this post on Zulip Mario Carneiro (May 28 2018 at 03:29):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:29):

and the hoare things are also orelsey

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:30):

|> and <| is ocaml notation

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:30):

does haskell have a <| equiv

view this post on Zulip Mario Carneiro (May 28 2018 at 03:31):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:32):

I can get behind <$ if $ is sticking around

view this post on Zulip Johan Commelin (May 28 2018 at 03:33):

But don't you want $> ?

view this post on Zulip Johan Commelin (May 28 2018 at 03:33):

That seems more intuitive to me...

view this post on Zulip Johan Commelin (May 28 2018 at 03:34):

But then, I've never used OCaml

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:35):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:35):

Yes...

view this post on Zulip Johan Commelin (May 28 2018 at 03:35):

The > conveys in which way the arguments flow

view this post on Zulip Johan Commelin (May 28 2018 at 03:35):

Just like in Bash...

view this post on Zulip Johan Commelin (May 28 2018 at 03:36):

if you write to a file

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:36):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:37):

Ok, that also makes sense...

view this post on Zulip Mario Carneiro (May 28 2018 at 03:37):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:37):

oh, <$ is taken...

view this post on Zulip Mario Carneiro (May 28 2018 at 03:37):

functor.map_const

view this post on Zulip Johan Commelin (May 28 2018 at 03:38):

What about $< ?

view this post on Zulip Johan Commelin (May 28 2018 at 03:38):

(No lean here, atm)

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:39):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:39):

$< is clear

view this post on Zulip Mario Carneiro (May 28 2018 at 03:39):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:40):

I guess <$ is named similar to <$>

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:43):

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...

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:44):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:45):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:46):

there is unicode for everything

view this post on Zulip Mario Carneiro (May 28 2018 at 03:46):

?

view this post on Zulip Mario Carneiro (May 28 2018 at 03:46):

= \lhd

view this post on Zulip Mario Carneiro (May 28 2018 at 03:47):

but mathematicians are also jockeying for these symbols

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:47):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:47):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:48):

import foo with bar as xyzzy

view this post on Zulip Johan Commelin (May 28 2018 at 03:48):

Like in python

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:48):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:48):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:48):

lol

view this post on Zulip Mario Carneiro (May 28 2018 at 03:48):

well, it is obviously redundant...

view this post on Zulip Johan Commelin (May 28 2018 at 03:50):

@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?

view this post on Zulip Mario Carneiro (May 28 2018 at 03:50):

nooo

view this post on Zulip Johan Commelin (May 28 2018 at 03:51):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:53):

Does Lean recognize 0-width space as whitespace?

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:57):

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)

view this post on Zulip Reid Barton (May 28 2018 at 03:57):

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

view this post on Zulip Reid Barton (May 28 2018 at 03:57):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:58):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:58):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 03:58):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 03:58):

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

view this post on Zulip Reid Barton (May 28 2018 at 03:59):

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

view this post on Zulip Johan Commelin (May 28 2018 at 03:59):

/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:

view this post on Zulip Reid Barton (May 28 2018 at 04:00):

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 >>=)

view this post on Zulip Johan Commelin (May 28 2018 at 04:00):

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

view this post on Zulip Reid Barton (May 28 2018 at 04:01):

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

view this post on Zulip Johan Commelin (May 28 2018 at 04:01):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 04:04):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 04:05):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 04:06):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 04:07):

actually the type checking thing is a good point

view this post on Zulip Andrew Ashworth (May 28 2018 at 04:08):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 04:09):

actually the type checking thing is a good point

how so?

view this post on Zulip Mario Carneiro (May 28 2018 at 04:22):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 04:22):

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 04:23):

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


Last updated: May 14 2021 at 06:16 UTC