andThen operator

Stream: lean4

[Juan Pablo Romero]

Quick question: is there an operator in the std library that implements this?

def andThen (f: A -> B) (g: B -> C): A -> C := g ∘ f

[Henrik Böving]

f $ g x, f <| g x, flip Function.comp come to mind

[Adam Topaz]

Is $\circ$ insufficient for what you want to do?

[Juan Pablo Romero]

oh, it's just that oftentimes I find it easier to reason from left to right

[Adam Topaz]

Ah then the pipes that Henrik mentioned would be helpful: |> and <|.

[Juan Pablo Romero]

yeah, I like those, but they require an argument.

[Kevin Buzzard]

The definition of function.comp also requires an argument, but it's supplied with a lambda.

[Adam Topaz]

Ah I see what you want here. Maybe we can use mathlib3's notation for composition of morphisms?

[Adam Topaz]

docs#quiver.hom.comp I think?

[Adam Topaz]

https://github.com/leanprover-community/mathlib/blob/8c9342fd8949ec8421ed6649685d5233a19e0c08/src/category_theory/category/basic.lean#L84

[Adam Topaz]

Does haskell have a standard ascii symbol for this?

[Juan Pablo Romero]

yeah, exactly!

[Juan Pablo Romero]

But ≫ probably will be used in mathlib 4 as well, so we'd need another symbol for plain function composition, no?

[Juan Pablo Romero]

lol, a quick Hoogle query revealed > 7 notations for this:
https://hoogle.haskell.org/?hoogle=(a%20-%3E%20b)%20-%3E%20(b%20-%3E%20c)%20-%3E%20(a%20-%3E%20c)

[Adam Topaz]

Unfortunately, I don't know enough about notation overloading in Lean4 to say whether we could use the same unicode symbol for both plain functions and morphisms in a category.

[Henrik Böving]

We could make a notation that is smart enough for this type of stuff without difficulty yes.

[Henrik Böving]

It might have some interesting interactions with type inference but generally speaking there is no obvious reason why it shouldn't work

[Mario Carneiro]

I was going to suggest ∘> which is similar to many of the haskell versions

[Jason Rute]

I personally question the need for all these fancy Haskell symbols especially now that Lean has |>, |>., and <|and (<- …) which are intuitive to read and remember. I remember when I was a Scala programmer, an experienced software engineer at my company saying that a lot of bad Scala code looks like “Haskell fan fiction”. I feel having to memorize all the Haskell symbols adds a lot of cognitive burden. Of course to each their own, and it is great that Lean lets you easily add in custom notation, especially for mathematics, where we need symbols to look like standard ones. Anyway, as with what Kevin said, you can accomplish this in a readable way with a lambda at the cost of a few extra symbols (and then you can also use |>. which is quite useful):

#eval [0,11,222].map (fun x =>
    Int.ofNat x
    |>.mod 10
    |> (. - 3)
    |> reprStr
  )  -- ["-3", "-2", "-1"]

[Leonardo de Moura]

I feel having to memorize all the Haskell symbols adds a lot of cognitive burden.

I feel the same.

BTW, we don't need the parentheses around fun in Lean 4. We can write

#eval [0,11,222].map fun x =>
    Int.ofNat x
    |>.mod 10
    |> (. - 3)
    |> reprStr

[Juan Pablo Romero]

Agreed with symbol explosion in Haskell. In the Scala community there's been a big push to use symbolic operators much more judiciously in the past few years. One major library (ZIO) even removed >>= recently, as it is totally alien to 99% of programmers.