Rename ∘ to << and add >>, |> and <| functions (#103)

This PR replaces the unicode composition function name with `<<` and
adds similar functions `>>`, `|>` and `<|`. Inspired by
[elm](https://package.elm-lang.org/packages/elm/core/latest/Basics#(%3C%3C)).

The `$` function is now called `<|`.

The `>>>` (builtin seq) function is now called `>->`.

The `>> : IO -> IO -> IO` function is now called `>>>`.

* Closes #59

Stdlib/Data/List/Base.juvix

@@ -204,7 +204,7 @@ quickSort {A} {{Ord A}} : List A → List A :=
       | nil := nil
       | xs@(_ :: nil) := xs
       | (x :: xs) :=
-        case partition (isGT ∘ Ord.cmp x) xs of
+        case partition (Ord.cmp x >> isGT) xs of
           l1, l2 := go l1 ++ x :: go l2;
   in go;
 
@@ -219,7 +219,7 @@ syntax iterator concatMap {init := 0; range := 1};
 --- Applies a function to every item on a ;List; and concatenates the result.
 --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.
 concatMap {A B} (f : A -> List B) : List A -> List B :=
-  flatten ∘ map f;
+  map f >> flatten;
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : List (List A) -> List (List A)

Stdlib/Data/String/Base.juvix

@@ -10,4 +10,4 @@ concatStr : List String -> String := foldl (++str) "";
 
 --- Joins a ;List; of ;String;s with "\n".
 unlines : List String -> String :=
-  concatStr ∘ intersperse "\n";
+  intersperse "\n" >> concatStr;

Stdlib/Function.juvix

@@ -4,11 +4,17 @@ import Stdlib.Data.Fixity open;
 import Stdlib.Data.Nat.Base open;
 import Stdlib.Data.Pair.Base open;
 
-syntax operator ∘ composition;
+syntax operator << composition;
 
---- Function composition.
+--- Function composition, passing results from the second function to the first.
 {-# inline: 2 #-}
-∘ {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);
+<< {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);
+
+syntax operator >> lcomposition;
+
+--- Function composition, passing results from the first function to the second.
+{-# inline: 2 #-}
+>> {A B C} (f : A → B) (g : B → C) (x : A) : C := g (f x);
 
 --- Always returns the first argument.
 {-# inline: 1 #-}
@@ -21,11 +27,17 @@ id {A} (a : A) : A := a;
 {-# inline: 1 #-}
 flip {A B C} (f : A → B → C) (b : B) (a : A) : C := f a b;
 
-syntax operator $ rapp;
+syntax operator <| rapp;
 
 --- Application operator with right associativity. Usually used as a syntactical
 --- facility.
-$ {A B} (f : A → B) (x : A) : B := f x;
+<| {A B} (f : A → B) (x : A) : B := f x;
+
+syntax operator |> lapp;
+
+--- Application operator with left associativity. Usually used as a syntactical
+--- facility.
+|> {A B} (x : A) (f : A → B) : B := f x;
 
 --- Applies a function n times.
 iterate {A} : Nat -> (A -> A) -> A -> A
@@ -38,8 +50,8 @@ syntax operator on lapp;
 on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C :=
   f (g a) (g b);
 
-syntax operator >>> seq;
+syntax operator >-> seq;
 
 builtin seq
->>> : {A B : Type} → A → B → B
+>-> : {A B : Type} → A → B → B
   | x y := y;

Stdlib/System/IO/Base.juvix

@@ -5,6 +5,6 @@ import Stdlib.Data.Fixity open;
 builtin IO
 axiom IO : Type;
 
-syntax operator >> seq;
+syntax operator >>> seq;
 builtin IO-sequence
-axiom >> : IO → IO → IO;
+axiom >>> : IO → IO → IO;

Stdlib/System/IO/Bool.juvix

@@ -8,4 +8,4 @@ builtin bool-print
 axiom printBool : Bool → IO;
 
 printBoolLn (b : Bool) : IO :=
-  printBool b >> printString "\n";
+  printBool b >>> printString "\n";

Stdlib/System/IO/Int.juvix

@@ -7,4 +7,5 @@ import Stdlib.System.IO.String open;
 builtin int-print
 axiom printInt : Int → IO;
 
-printIntLn (i : Int) : IO := printInt i >> printString "\n";
+printIntLn (i : Int) : IO :=
+  printInt i >>> printString "\n";

Stdlib/System/IO/Nat.juvix

@@ -7,4 +7,5 @@ import Stdlib.System.IO.String open;
 builtin nat-print
 axiom printNat : Nat → IO;
 
-printNatLn (n : Nat) : IO := printNat n >> printString "\n";
+printNatLn (n : Nat) : IO :=
+  printNat n >>> printString "\n";

Stdlib/System/IO/String.juvix

@@ -10,4 +10,4 @@ builtin IO-readline
 axiom readLn : (String → IO) → IO;
 
 printStringLn (s : String) : IO :=
-  printString s >> printString "\n";
+  printString s >>> printString "\n";

test/Package.juvix

@@ -9,5 +9,5 @@ package : Package :=
                      ; github
                        "anoma"
                        "juvix-quickcheck"
-                       "b6ca4d4bd80d62b95e2d7e28e881c5b547643564"
+                       "8068d58360d2adecba3674a31e031e7ad992e0e1"
                      ]};

test/juvix.lock.yaml

@@ -2,17 +2,17 @@
 # Do not edit this file manually.
 
 version: 2
-checksum: c311ba35a484fb649358719f7720cf706aa8b13d8066bb0fe600ef0d7bc4ca2c
+checksum: 5de68b52002fccbfacd5df82593d631368f3303203d03dc72f126e74a5997283
 dependencies:
 - path: ../
   dependencies: []
 - git:
     name: anoma_juvix-quickcheck
-    ref: b6ca4d4bd80d62b95e2d7e28e881c5b547643564
+    ref: 8068d58360d2adecba3674a31e031e7ad992e0e1
     url: https://github.com/anoma/juvix-quickcheck
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: 3f2c29880e749c7dd222011527a077b5f5050a95
+      ref: 290f67fc85b637ce4df886fc3cd1a5289b38db95
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []