Style question: space between '|>' and '.'?

Stream: mathlib4

[Michael Stoll]

In #18923, @David Loeffler just asked me to change ... |>.false into ... |> .false. I think I like the version without space better when dot notation follows. Is there a convention/consensus on how this should be formatted in Mathlib?

[Michael Stoll]

mstoll:~/lean4/mathlib4$ git grep '|>\.' | wc -l
983
mstoll:~/lean4/mathlib4$ git grep '|> \.' | wc -l
3

[Michael Stoll]

Statistics seem to be in favor of no space...

[Joachim Breitner]

These are different syntaxes!

opaque A : Type
opaque B : Type

axiom a : A
axiom A.f : A → B
axiom B.f : A → B

set_option pp.fieldNotation.generalized false

/-- info: B.f a : B -/
#guard_msgs in
#check (a |> .f : B)

/-- info: A.f a : B -/
#guard_msgs in
#check (a |>.f : B)

Without space uses the namespace of the argument coming from the left, with space uses the namespace of the expected type.

[Michael Stoll]

Should I know this?

[Joachim Breitner]

Probably? Lean has a large language surface.
Eventually we’ll be able to point to https://lean-lang.org/doc/reference/latest/Terms/#terms

[Michael Stoll]

So a |>.f is equivalent to a.f, but a .f is illegal...

[Michael Stoll]

Joachim Breitner said:

Probably? Lean has a large language surface.
Eventually we’ll be able to point to https://lean-lang.org/doc/reference/latest/Terms/#terms

I guess the point is that one has to realize first that there might be a difference...

[Damiano Testa]

I think that is written .f a.

[Michael Stoll]

and .f |> a is also illegal...

[Damiano Testa]

docs#Lean.Parser.Term.dotIdent does not have a doc-string...

[David Loeffler]

In the original PR, I believe "the namespace of the argument coming from the left" and "the namespace of the expected type" were the same – presumably this is not such an uncommon situation.

[Michael Stoll]

I wonder if there is a difference at the three places where Mathlib uses a space.

[Damiano Testa]

Or at the 983 where it doesn't! :upside_down:

[Michael Stoll]

Anyway, my impression is that the inofficial convention is to not use a space (except perhaps when it makes a difference and you want the other syntax?).

[Eric Wieser]

I'd propose using a |>.f where you would have otherwise written a.f, and a |> .f where you would have otherwise written .f a. I would guess the latter is quite rare.

[Eric Wieser]

Does mathlib use |> at all besides as |>. and the three cases above?

[Michael Stoll]

$ git grep '|> [^\.]' | wc -l
119

if this is an indication...

[David Loeffler]

I suspect the relative rarity of |> .f is probably because "anonymous" dot-notation (dot-notating off the expected type) is a fairly recent introduction, and there are a lot of places in mathlib where it could be used but isn't.

[Joachim Breitner]

Michael Stoll said:

and .f |> a is also illegal...

Not illegal. If lean can infer the expected type of .f it will use it:

/-- info: !true : Bool -/
#guard_msgs in
#check .true |> not

[Michael Stoll]

.f <| a does work :smile: (in the earlier example).

[Michael Stoll]

Are there any subtleties around <| as well?

[Joachim Breitner]

Both <| and |> are rather simple, and are orthogonal to the .f notation, so one can understand them separately.

It’s e |>.f x y that’s a bit unexpected, but if you think of |>. as it’s own thing, separate from |>, it’s not too confusing I’d say.

[David Loeffler]

Both <| and |> are rather simple

I'm actually not a fan of them myself, particularly |>: I find it disturbs reading the code because you have to back-track to work out where the implicit left-parenthesis should go. Is there any chance we could make VSCode indicate this visually (like it does with coloured parentheses)?

[Eric Wieser]

Does hovering over <| not already show what you want?

[David Loeffler]

Eric Wieser said:

Does hovering over <| not already show what you want?

No, it doesn't. Is it supposed to?

(It shows a box with a general docstring about <| and |>, and the type of the expression in which it occurs, but it doesn't make any attempt to show you where the hidden opposite parenthesis goes.)

[Eric Wieser]

I get a dark blue highlight around the extent of the <|:
image.png

[Michael Stoll]

Here are the three lines using |> .:

~/lean4/mathlib4$ git grep '|> \.'
Cache/Hashing.lean:  let imps := s.imports.map (·.module.components |> .map toString)
Mathlib/Analysis/Complex/Tietze.lean:  Basis.ofVectorSpace 𝕜 E |>.equivFun.toContinuousLinearEquiv.toHomeomorph |> .of_homeo
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean:  .setOf_finite |> .compl

The middle one even uses both versions!

[David Loeffler]

Eric Wieser said:

I get a dark blue highlight around the extent of the <|:
image.png

Sorry, you're right: the highlight is there, it's just so faint that it's almost invisible to my middle-aged eyesight so I had never noticed it before. (I'll have to see if I can tinker with the VSCode settings to turn the contrast up.)

[Filippo A. E. Nuccio]

David Loeffler said:

I suspect the relative rarity of |> .f is probably because "anonymous" dot-notation (dot-notating off the expected type) is a fairly recent introduction, and there are a lot of places in mathlib where it could be used but isn't.

I agree that in lot of places "it could be used", but I would argue that short of a proper doc (perhaps on the community website) it is perhaps better to refrain from using it. It makes the code harder to understand and harder to review for people who are not comfortable with it, creating a barrier that does not seem justified by limited the number of characters saved by using the anonymous dot notation.

[Eric Wieser]

Anonymous dot notation can save quite a lot of characters for things like .add (.mul _ _) (.mul _ _) vs Foo.add (Bar.mul _ _) (Baz.mul _ _)

[Mario Carneiro]

characters and thinking time to find the right namespace

[Kyle Miller]

It's never occurred to me that one could write x |> .f before. I've used x |>.f occasionally, but in programming contexts, not math ones. It's useful for chaining operations on a single object, like d |>.insert key1 val1 |>.insert key2 val2.

I see mathlib has been using |>. notation in math. First I found was subset_tsupport _ |>.trans (tsupport_subset f), instead of (subset_tsupport _).trans (tsupport_subset f). It saves parentheses at the cost of an extra space character :-)

[Michael Stoll]

I find it useful when (...).something would exceed the line length limit; instead I can write

  ...
  |>.something

which I usually find easier to read than breaking the long ... somewhere in the middle.

[Eric Wieser]

|>.trans <| is a very handy pattern for chaining term mode equalities without having to back to the start of the line and add another (

[Jireh Loreaux]

I use |>.comp <| and |>.trans <| a lot, and |>. in general.

[Sebastian Ullrich]

Kyle Miller said:

It's never occurred to me that one could write x |> .f before

Me neither, and I'm to be blamed for both notations!