pipelining as first class citizens?

Stream: lean4

[Gabriel DORIATH DÖHLER]

Hello,
|>, <| and $ are just syntactic sugar (https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L157).
In Haskell they are functions. This is helpful to learn what they do (you can just look at their types).
Is there a good reason for defining pipelining with syntactic sugar in lean4?

[Kyle Miller]

The impression I've had, which might have no bearing on reality, is that it's out of a combination of performance (there aren't additional functions that have to run, though these could be inlined) and making it so they're completely indistinguishable from a function application, which has consequences for typeclass inference and writing proofs. I've been curious about this, too, though, especially the args.push optimization (is this to show off fbip?)

[Mac]

There are a couple of important pieces here:

1. In Haskell, operators (i.e., symbols like +,-,$ are just a specific class of identifiers which default to being written infix (e.g., a + b) with prefix use (e.g., (+) a b) requiring parentheses whereas normal alphanumeric identifiers (foo, bar) default to being written prefix foo a b and requiring backticks for infix use (e.g., a `mod` b . In Lean, all operators are not identifiers but rather custom notation / macros / elaborators, that may, in some cases, expand to identifiers (i.e., a + b expands to HAdd.hAdd a b), but that is not a requirement.

2. Functions are costly for both the compiler and proofs. If |>, <|, and $ were functions, the compiler would need to determine whether to inline them and proofs would need to unfold them and show their equivalence. Making them syntactic sugar avoids all this unnecessary complexity.

3. In Lean, syntactic sugar -- that is syntax, macros, and elaborators -- are first class concepts. Lean supports go-to-def and docstrings on hover for syntactic sugar. Thus is possible to document sugar just as well as a function.