Add pipeline operators

[observant2]

Description

Adds the pipeline operators |> and <| known from other functional languages like F# and Elixir.

Should this change go in the CHANGELOG?

• [x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[andrevidela]

Looks like there are some test to fix because now there are two conflicting fixity definitions for (<|)

[observant2]

Unfortunately I'm stuck here. When I execute "tests/idris2/operators/operators001/Test.idr" with %hide Prelude.Ops.infixr.(|>) I still get the errors:

1/1: Building Test (Test.idr)
[-Warning: operator fixity is ambiguous, we are picking Prelude.Ops.infixr.(|>) out of :-]
[- - Prelude.Ops.infixr.(|>), precedence level 9-]
[- - Test.infixr.(|>), precedence level 0-]

[-To remove this warning, use `%hide` with the fixity to remove-]
[-For example: %hide Prelude.Ops.infixr.(|>)-]

It suggests me to do what I already did.

[andrevidela]

Do the tests run locally? it seems there are still conflicting fixity definitions in the file Import.idr for the test idris2/misc/import009

[observant2]

Now they should pass.

[observant2]

Oh, I forgot, someone commented in Discord:

shouldn't (|>) be infixl in the prelude? also, I think it would make more sense if both pipeline operators had the same precedence

So should I make |> infixl? If they should get the same precedence, which should it be?

[buzden]

So should I make |> infixl?

You definitely should. Even example from your docstring shouldn't typecheck if this operator leaves infixr.

If they should get the same precedence, which should it be?

Precedence should be low enough to be able to form the value you are operating on. Again, in your docstring, you are, actually, applying |> after a bunch of :: (which [a, b c] desugars to), so |> should have a precedence lower than that (and now it's very high). I think that 0 for both is rather a good choice.

Maybe you should add the example from your docstring as a test in order to check that what you intended still works.

UPD: You should also check the resulting value in this test, because after changing only the fixity it may typecheck by applying the whole pipeline to the Nil at the end surprisingly not changing the list at all. I.e. with current precedence you will have [1] :: [2] :: [3] :: (Nil |> join |> map (* 2)) which I'm sure not something that was intended.

[observant2]

Okay, that's a good idea, where should this test go? Is there an existing file where it would fit or should I create a new operators011 folder?

[buzden]

Okay, that's a good idea, where should this test go? Is there an existing file where it would fit or should I create a new operators011 folder?

It should go here, I think: https://github.com/idris-lang/Idris2/tree/main/tests/prelude