Shorthand for function composition?

Stream: lean4

[Anurudh Peduri]

Hey,
Is there a point free version of the |>. notation?

For example, consider this implementation for count

def List.count (p : α → Bool) (l : List α) : Nat :=
  l.filter p |>.length

Instead, I would like to write something like:

def List.count' (p : α → Bool) : List α → Nat :=
  .filter p >>>.length

[Marcus Rossel]

Is either of these two what you're looking for?:

def List.count' (p : α → Bool) : List α → Nat :=
  length ∘ filter p

def List.count' (p : α → Bool) : List α → Nat :=
  (⋅.filter p |>.length)

[Anurudh Peduri]

Yep! the second one. Thanks a lot!

p.s. Is there some way to avoid the parenthesis? I guess not.

[Marcus Rossel]

No, you need the parentheses. The notation (foo ⋅ bar ⋅ baz ⋅) is shorthand for fun a b c => foo a bar b baz c.

[Trebor Huang]

Practically this may be what is needed, but that is not technically pointfree though.

[Mario Carneiro]

sure it is, there are no variable names in sight

[Mario Carneiro]

TBH I think that's just a much better way to do pointfree than haskell style ascii soup