Add Stdlib.Data.Result and find in Stdlib.Data.List (#106)

This PR adds implementations of the following, with corresponding tests:

* An `Result` type with associated functions to the standard library.
* A `find` function to `Stdlib.Data.List`

Requirements for both arose when writing Anoma applications.

NB: 

Adding the `{-# specialize: [1] #-}` pragma to `find` causes the
compiler to go into an infinite loop when compiling a `find` call with
predicate `const false`, e.g

```
find {Nat} (const false) [1;2;3]
```

So I've omitted that for now and ~~I'll raise a separate bug~~, I
suspect I was using the `specialize` pragma incorrectly.

Stdlib/Data/List/Base.juvix

@@ -16,6 +16,15 @@ elem {A} (eq : A → A → Bool) (s : A) : List A → Bool
   | nil := false
   | (x :: xs) := eq s x || elem eq s xs;
 
+--- 𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or
+--- nothing if there's no such element.
+find {A} (predicate : A → Bool) : List A → Maybe A
+  | nil := nothing
+  | (x :: xs) :=
+    if
+      | predicate x := just x
+      | else := find predicate xs;
+
 --- Right-associative fold.
 {-# specialize: [1] #-}
 foldr {A B} (f : A → B → B) (z : B) : List A → B

Stdlib/Data/Result.juvix

@@ -0,0 +1,26 @@
+module Stdlib.Data.Result;
+
+import Stdlib.Data.Result.Base open public;
+import Stdlib.Data.Bool.Base open;
+
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+
+instance
+ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
+  mkOrd@{
+    cmp : Result A B -> Result A B -> Ordering
+      | (error a1) (error a2) := Ord.cmp a1 a2
+      | (ok b1) (ok b2) := Ord.cmp b1 b2
+      | (error _) (ok _) := LT
+      | (ok _) (error _) := GT
+  };
+
+instance
+eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
+  mkEq@{
+    eq : Result A B -> Result A B -> Bool
+      | (error a1) (error a2) := a1 == a2
+      | (ok b1) (ok b2) := b1 == b2
+      | _ _ := false
+  };

Stdlib/Data/Result/Base.juvix

@@ -0,0 +1,60 @@
+module Stdlib.Data.Result.Base;
+
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.Maybe.Base open;
+import Stdlib.Function open;
+
+--- The Result type represents either a success with a value of `ok` or an error
+--- with value `error`.
+type Result E A :=
+  | error E
+  | ok A;
+
+--- Apply the onError function if the value is ;error; or apply the
+--- onOk function if the value is ;ok;.
+handleResult
+  {E A B}
+  (onError : E -> B)
+  (onOk : A -> B)
+  : Result E A -> B
+  | (error a) := onError a
+  | (ok a) := onOk a;
+
+--- Apply a function to the ;error; value of a Result.
+mapError
+  {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A :=
+  handleResult (f >> error) ok;
+
+--- Apply a function to the ;ok; value of a Result.
+mapOk {E A C} (f : A -> C) : Result E A -> Result E C :=
+  handleResult error (f >> ok);
+
+--- Return ;true; if the value is an ;error;, otherwise ;false;.
+isError {E A} : Result E A -> Bool
+  | (error _) := true
+  | (ok _) := false;
+
+--- Return ;true; if the value is ;ok;, otherwise ;false;.
+isOk {E A} : Result E A -> Bool
+  | (error _) := false
+  | (ok _) := true;
+
+--- Return the contents of an ;error; value, otherwise return a default.
+fromError {E A} (default : E) : Result E A -> E
+  | (error a) := a
+  | (ok _) := default;
+
+--- Return the contents of an ;ok; value, otherwise return a default.
+fromOk {E A} (default : A) : Result E A -> A
+  | (error _) := default
+  | (ok b) := b;
+
+--- Convert a Result to a Maybe. An ;error; value becomes `nothing`.
+resultToMaybe {E A} : Result E A -> Maybe A :=
+  handleResult (const nothing) just;
+
+--- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`.
+maybeToResult
+  {E A} (defaultError : E) : Maybe A -> Result E A
+  | nothing := error defaultError
+  | (just x) := ok x;

Stdlib/Prelude.juvix

@@ -12,6 +12,7 @@ import Stdlib.Data.Int open public;
 import Stdlib.Data.Field open public;
 import Stdlib.Data.Pair open public;
 import Stdlib.Data.String open public;
+import Stdlib.Data.Result open public;
 import Stdlib.Function open public;
 import Stdlib.System.IO open public;
 

test/Package.juvix

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

test/Test.juvix

@@ -9,6 +9,7 @@ import Data.String open;
 
 import Test.QuickCheckTest as QC;
 import Test.Arb as QC;
+import Test.StdlibTestExtra;
 
 prop-reverseDoesNotChangeLength : List Int -> Bool
   | xs := length (reverse xs) == length xs;
@@ -125,6 +126,89 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool
           | _ := null xs;
     in checkTxsRowXsCol && checkXsRowTxsCol;
 
+prop-foundElementSatisfiesPredicate
+  (p : Int -> Bool) (xs : List Int) : Bool :=
+  case find p xs of
+    | just x := p x
+    | nothing := true;
+
+prop-nonExistenceImpliesPredicateFalseForAll
+  (p : Int -> Bool) (xs : List Int) : Bool :=
+  case find p xs of
+    | just _ := true
+    | nothing := all (x in xs) not (p x);
+
+prop-findConsistentWithSplitAt
+  (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool :=
+  let
+    ys×zs := splitAt n xs;
+    ys := fst ys×zs;
+    zs := snd ys×zs;
+  in case find p xs of
+       | just x :=
+         if
+           | elem (==) x ys := find p ys == just x
+           | elem (==) x zs := find p zs == just x
+           | else := false
+       | nothing := true;
+
+prop-findWithEmptyList (p : Int -> Bool) : Bool :=
+  find p [] == nothing;
+
+prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool :=
+  if
+    | null xs := true
+    | else :=
+      case find (const true) xs of
+        | just _ := true
+        | nothing := false;
+
+prop-findWithAlwaysFalseIsNothing (xs : List Int) : Bool :=
+  find (const false) xs == nothing;
+
+prop-resultErrorApplication
+  (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
+  handleResult f g (error x) == f x;
+
+prop-resultOkApplication
+  (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
+  handleResult f g (ok x) == g x;
+
+prop-resultIsError : Result Int Bool -> Bool
+  | x@(error _) := isError x
+  | x@(ok _) := not (isError x);
+
+prop-resultIsOk : Result Int Bool -> Bool
+  | x@(error _) := not (isOk x)
+  | x@(ok _) := isOk x;
+
+prop-resultFromErrorDefault
+  (defaultError : Int) : Result Int Bool -> Bool
+  | e@(error x) := fromError defaultError e == x
+  | e@(ok _) := fromError defaultError e == defaultError;
+
+prop-resultFromOkDefault
+  (defaultOk : Bool) : Result Int Bool -> Bool
+  | e@(error _) := fromOk defaultOk e == defaultOk
+  | e@(ok x) := fromOk defaultOk e == x;
+
+prop-resultToMaybe : Result Int Bool -> Bool
+  | e@(error _) := resultToMaybe e == nothing
+  | e@(ok x) := resultToMaybe e == just x;
+
+prop-maybeToResult (def : Int) : Maybe Bool -> Bool
+  | m@(just x) := maybeToResult def m == ok x
+  | m@nothing := maybeToResult def m == error def;
+
+prop-resultMapError
+  (f : Int -> Int) : Result Int Int -> Bool
+  | e@(error x) := mapError f e == error (f x)
+  | e@(ok _) := mapError f e == e;
+
+prop-resultMapOk (f : Int -> Int) : Result Int Int -> Bool
+  | e@(error _) := mapOk f e == e
+  | e@(ok x) := mapOk f e == ok (f x);
+
 sortTest : String -> (List Int -> List Int) -> QC.Test
   | sortName sort :=
     QC.mkTest
@@ -200,26 +284,118 @@ transposeMatrixDimentionsTest : QC.Test :=
     "transpose: transpose swaps dimensions"
     prop-transposeMatrixDimensions;
 
+findFoundElementSatisfiesPredicate : QC.Test :=
+  QC.mkTest
+    "find: found element satisfies predicate"
+    prop-foundElementSatisfiesPredicate;
+
+findNonExistenceImpliesPredicateFalseForAll : QC.Test :=
+  QC.mkTest
+    "find: non existence implies predicate false for all"
+    prop-nonExistenceImpliesPredicateFalseForAll;
+
+findConsistentWithSplitAt : QC.Test :=
+  QC.mkTest
+    "find: consistent with splitAt"
+    prop-findConsistentWithSplitAt;
+
+findOnEmptyListIsNothing : QC.Test :=
+  QC.mkTest
+    "find: called with empty list is nothing"
+    prop-findWithEmptyList;
+
+findWithAlwaysTrueIsJust : QC.Test :=
+  QC.mkTest
+    "find: always true predicate returns just"
+    prop-findWithAlwaysTrueIsJust;
+
+findWithAlwaysFalseIsNothing : QC.Test :=
+  QC.mkTest
+    "find: always false predicate returns nothing"
+    prop-findWithAlwaysFalseIsNothing;
+
+resultResultErrorApplication : QC.Test :=
+  QC.mkTest
+    "result: result error application"
+    prop-resultErrorApplication;
+
+resultResultOkApplication : QC.Test :=
+  QC.mkTest
+    "result: result ok application"
+    prop-resultOkApplication;
+
+resultIsError : QC.Test :=
+  QC.mkTest
+    "result: isError detects error"
+    prop-resultIsError;
+
+resultIsOk : QC.Test :=
+  QC.mkTest "result: isOk detects ok" prop-resultIsOk;
+
+resultFromError : QC.Test :=
+  QC.mkTest
+    "result: fromError uses default"
+    prop-resultFromErrorDefault;
+
+resultFromOk : QC.Test :=
+  QC.mkTest
+    "result: fromOk uses default"
+    prop-resultFromOkDefault;
+
+resultResultToMaybe : QC.Test :=
+  QC.mkTest "result: resultToMaybe" prop-resultToMaybe;
+
+resultMaybeToResult : QC.Test :=
+  QC.mkTest "result: maybeToResult" prop-maybeToResult;
+
+resultMapError : QC.Test :=
+  QC.mkTest "result: mapError" prop-resultMapError;
+
+resultMapOk : QC.Test :=
+  QC.mkTest "result: mapOk" prop-resultMapOk;
+
 main : IO :=
   readLn
     \ {seed :=
-      QC.runTestsIO
-        100
-        (stringToNat seed)
-        [ partitionTest
-        ; reverseLengthTest
-        ; reverseReverseIdTest
-        ; splitAtRecombineTest
-        ; splitAtLengthTest
-        ; mergeSumLengthsTest
-        ; tailLengthOneLessTest
-        ; equalCompareToEqTest
-        ; zipTest
-        ; zipWithTest
-        ; snocTest
-        ; dropTest
-        ; sortTest "mergeSort" mergeSort
-        ; sortTest "quickSort" quickSort
-        ; transposeMatrixIdTest
-        ; transposeMatrixDimentionsTest
-        ]};
+      let
+        seedNat := stringToNat seed;
+      in QC.runTestsIO
+          100
+          seedNat
+          [ partitionTest
+          ; reverseLengthTest
+          ; reverseReverseIdTest
+          ; splitAtRecombineTest
+          ; splitAtLengthTest
+          ; mergeSumLengthsTest
+          ; tailLengthOneLessTest
+          ; equalCompareToEqTest
+          ; zipTest
+          ; zipWithTest
+          ; snocTest
+          ; dropTest
+          ; sortTest "mergeSort" mergeSort
+          ; sortTest "quickSort" quickSort
+          ; transposeMatrixIdTest
+          ; transposeMatrixDimentionsTest
+          ; findFoundElementSatisfiesPredicate
+          ; findNonExistenceImpliesPredicateFalseForAll
+          ; findConsistentWithSplitAt
+          ; findOnEmptyListIsNothing
+          ; findWithAlwaysTrueIsJust
+          ; findWithAlwaysFalseIsNothing
+          ]
+        >>> QC.runTestsIO
+          100
+          seedNat
+          [ resultResultErrorApplication
+          ; resultResultOkApplication
+          ; resultIsError
+          ; resultIsOk
+          ; resultFromError
+          ; resultFromOk
+          ; resultResultToMaybe
+          ; resultMaybeToResult
+          ; resultMapError
+          ; resultMapOk
+          ]};

test/Test/StdlibTestExtra.juvix

@@ -0,0 +1,12 @@
+module Test.StdlibTestExtra;
+
+import Stdlib.Prelude open;
+
+instance
+eitherShow
+  {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
+  mkShow@{
+    show : Result A B -> String
+      | (error x) := "Error (" ++str Show.show x ++str ")"
+      | (ok x) := "Ok (" ++str Show.show x ++str ")"
+  };

test/juvix.lock.yaml

@@ -1,18 +1,18 @@
-# This file was autogenerated by Juvix version 0.6.2.
+# This file was autogenerated by Juvix version 0.6.3.
 # Do not edit this file manually.
 
 version: 2
-checksum: 5de68b52002fccbfacd5df82593d631368f3303203d03dc72f126e74a5997283
+checksum: 8013d01c2b6d46596d97438913b23987618efe1f7a6e54e7abd22dd5e0ae7f43
 dependencies:
 - path: ../
   dependencies: []
 - git:
     name: anoma_juvix-quickcheck
-    ref: 8068d58360d2adecba3674a31e031e7ad992e0e1
+    ref: 8e5d49682fb0b861fc0a1aed95cfebab03231d85
     url: https://github.com/anoma/juvix-quickcheck
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: 290f67fc85b637ce4df886fc3cd1a5289b38db95
+      ref: 95f93e60e1033046d950414a805f7a4bc75adb62
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []