Add Applicative trait (#115)

- Add `Applicative` trait.
- Add instances for `List`, `Maybe`, `Result`.

---------

Co-authored-by: Paul Cadman <[email protected]>

Makefile

@@ -14,6 +14,7 @@ html:
 PHONY: clean
 clean:
 	rm -rf docs
+	$(MAKE) -C test/ clean
 
 .PHONY: test
 test:

Stdlib/Data/List.juvix

@@ -8,7 +8,7 @@ import Stdlib.Function open;
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
-import Stdlib.Trait.Functor open;
+import Stdlib.Trait open;
 import Stdlib.Trait.Partial open;
 import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable};
 
@@ -75,3 +75,12 @@ polymorphicFoldableListI : Polymorphic.Foldable List :=
 {-# specialize: true, inline: true #-}
 instance
 foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
+
+instance
+applicativeListI : Applicative List :=
+  mkApplicative@{
+    pure {A} (a : A) : List A := [a];
+    ap {A B} : List (A -> B) -> List A -> List B
+      | [] _ := []
+      | (f :: fs) l := map f l ++ ap fs l
+  };

Stdlib/Data/Maybe.juvix

@@ -6,6 +6,7 @@ import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Applicative open;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
@@ -51,3 +52,12 @@ functorMaybeI : Functor Maybe :=
 {-# specizalize: true, inline: true #-}
 instance
 monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;
+
+instance
+applicativeMaybeI : Applicative Maybe :=
+  mkApplicative@{
+    pure := just;
+    ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
+      | (just f) (just x) := just (f x)
+      | _ _ := nothing
+  };

Stdlib/Data/Result.juvix

@@ -5,7 +5,7 @@ import Stdlib.Data.Bool.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
-import Stdlib.Trait.Functor open;
+import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
 instance
@@ -39,3 +39,13 @@ functorResultI {err} : Functor (Result err) :=
 instance
 monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res :=
   fromPolymorphicFunctor;
+
+instance
+applicativeResultI {err} : Applicative (Result err) :=
+  mkApplicative@{
+    pure := ok;
+    ap {A B} : Result err (A -> B) -> Result err A -> Result err B
+      | (ok f) (ok x) := ok (f x)
+      | (ok _) (error e) := error e
+      | (error e) _ := error e
+  };

Stdlib/Data/Unit.juvix

@@ -1,17 +1,14 @@
 --- The unit type.
 module Stdlib.Data.Unit;
 
+import Stdlib.Data.Unit.Base open public;
 import Stdlib.Data.Bool.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Foldable open;
 
-type Unit :=
-  --- The only constructor of ;Unit;.
-  unit;
-
 instance
 eqUnitI : Eq Unit := mkEq λ {unit unit := true};
 

Stdlib/Data/Unit/Base.juvix

@@ -0,0 +1,13 @@
+--- The unit type.
+module Stdlib.Data.Unit.Base;
+
+import Stdlib.Data.Bool.Base open;
+
+import Stdlib.Trait.Eq open;
+import Stdlib.Trait.Ord open;
+import Stdlib.Trait.Show open;
+import Stdlib.Trait.Foldable open;
+
+type Unit :=
+  --- The only constructor of ;Unit;.
+  unit;

Stdlib/Trait.juvix

@@ -4,6 +4,7 @@ import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
 import Stdlib.Trait.Show as Show open using {Show; module Show} public;
 import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public;
 import Stdlib.Trait.Functor open public;
+import Stdlib.Trait.Applicative open public;
 import Stdlib.Trait.Foldable open public;
 import Stdlib.Trait.Partial open public;
 import Stdlib.Trait.Natural open public;

Stdlib/Trait/Applicative.juvix

@@ -0,0 +1,49 @@
+module Stdlib.Trait.Applicative;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Function open;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.List.Base open;
+import Stdlib.Data.Unit.Base open;
+import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Foldable.Polymorphic open;
+import Stdlib.Data.Unit.Base open;
+
+trait
+type Applicative (f : Type -> Type) :=
+  mkApplicative {
+    {{functor}} : Functor f;
+    pure : {A : Type} -> A -> f A;
+    ap : {A B : Type} -> f (A -> B) -> f A -> f B
+  };
+
+open Applicative public;
+
+--- Sequences computations.
+--- Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.
+applicativeSeq {f : Type -> Type} {{Applicative f}} {A B : Type} (fa : f A) (fb : f B) : f B :=
+  ap (map λ {_ b := b} fa) fb;
+
+--- lifts a binary function to ;Applicative;
+liftA2 {f : Type -> Type} {{Applicative f}} {A B C} (fun : A -> B -> C) : f A -> f B -> f C :=
+  map fun >> ap;
+
+syntax iterator mapA_ {init := 0; range := 1};
+mapA_
+  {t : Type -> Type}
+  {f : Type -> Type}
+  {A B}
+  {{Foldable t}}
+  {{Applicative f}}
+  (fun : A -> f B)
+  (l : t A)
+  : f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc};
+
+replicateA {f : Type -> Type} {A} {{Applicative f}} : Nat -> f A -> f (List A)
+  | zero _ := pure []
+  | (suc n) x := liftA2 (::) x (replicateA n x);
+
+when {f : Type -> Type} {{Applicative f}} : Bool -> f Unit -> f Unit
+  | false _ := pure unit
+  | true a := a;

test/Package.juvix

@@ -6,5 +6,5 @@ package : Package :=
   defaultPackage@?{
     name := "stdlib-test";
     dependencies :=
-      [path "../"; github "anoma" "juvix-quickcheck" "eca0d109869eeb7b708162634f4917f270139da1"]
+      [path "../"; github "anoma" "juvix-quickcheck" "104c749950480ed5dad42c7385a020ff31ca8875"]
   };

test/juvix.lock.yaml

@@ -1,18 +1,18 @@
-# This file was autogenerated by Juvix version 0.6.4.
+# This file was autogenerated by Juvix version 0.6.5.
 # Do not edit this file manually.
 
 version: 2
-checksum: fe279cadfedcac3f17d3557f5b1bbc168a153b29b6876bd56df33e21aad59ee5
+checksum: 74c7b4f7ff78859f15da9fa14ede6df5397c698d1efdcd5cc0f435d5cbb59e9d
 dependencies:
 - path: ../
   dependencies: []
 - git:
     name: anoma_juvix-quickcheck
-    ref: eca0d109869eeb7b708162634f4917f270139da1
+    ref: 104c749950480ed5dad42c7385a020ff31ca8875
     url: https://github.com/anoma/juvix-quickcheck
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: 297601a98dcace657aaff6e42945f1430647885b
+      ref: 0ca2d5181e7c98eceace5c12bfd0a8cfb3d4d132
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []