## Stream: general

#### Brendan Zabarauskas (May 28 2018 at 03:13):

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

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

#### Andrew Ashworth (May 28 2018 at 03:15):

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

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

#### Mario Carneiro (May 28 2018 at 03:19):

I believe that operator is used for option.lhoare

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

#### Mario Carneiro (May 28 2018 at 03:21):

I think that lhoare and rhoare are surprisingly useless operators

#### Brendan Zabarauskas (May 28 2018 at 03:22):

what on earth is a hoare?

#### Mario Carneiro (May 28 2018 at 03:22):

I have never seen a use for them

as in tony

hoare logic?

#### 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 :(

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

#### Mario Carneiro (May 28 2018 at 03:24):

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

#### Mario Carneiro (May 28 2018 at 03:25):

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

#### Mario Carneiro (May 28 2018 at 03:26):

maybe I can get @Sebastian Ullrich to burninate it?

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

#### Mario Carneiro (May 28 2018 at 03:28):

the dollar's not going anywhere though

#### Andrew Ashworth (May 28 2018 at 03:28):

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

#### Johan Commelin (May 28 2018 at 03:33):

That seems more intuitive to me...

#### Johan Commelin (May 28 2018 at 03:34):

But then, I've never used OCaml

#### Johan Commelin (May 28 2018 at 03:38):

(No lean here, atm)

#### Andrew Ashworth (May 28 2018 at 03:39):

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

#### Mario Carneiro (May 28 2018 at 03:48):

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

lol

#### Mario Carneiro (May 28 2018 at 03:48):

well, it is obviously redundant...

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

nooo

#### Johan Commelin (May 28 2018 at 03:51):

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

#### Johan Commelin (May 28 2018 at 03:53):

Does Lean recognize 0-width space as whitespace?

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

#### Reid Barton (May 28 2018 at 03:57):

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

#### Reid Barton (May 28 2018 at 03:57):

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

#### Andrew Ashworth (May 28 2018 at 03:58):

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

#### Mario Carneiro (May 28 2018 at 03:58):

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


#### Mario Carneiro (May 28 2018 at 03:58):

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

#### 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 :)

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

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

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

#### Johan Commelin (May 28 2018 at 04:00):

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

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

#### Johan Commelin (May 28 2018 at 04:01):

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

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

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

#### Andrew Ashworth (May 28 2018 at 04:06):

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

#### Mario Carneiro (May 28 2018 at 04:07):

actually the type checking thing is a good point

#### Andrew Ashworth (May 28 2018 at 04:08):

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

#### Andrew Ashworth (May 28 2018 at 04:09):

actually the type checking thing is a good point

how so?

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

#### Mario Carneiro (May 28 2018 at 04:22):

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

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