diff --git a/Makefile b/Makefile index 4322f9f3..d860051c 100644 --- a/Makefile +++ b/Makefile @@ -14,6 +14,7 @@ html: PHONY: clean clean: rm -rf docs + $(MAKE) -C test/ clean .PHONY: test test: diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index 67d46218..a4ff5b3a 100644 --- a/Stdlib/Data/List.juvix +++ b/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 + }; diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix index d10c21b8..1140a72a 100644 --- a/Stdlib/Data/Maybe.juvix +++ b/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 + }; diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix index d4195cc0..6c82211f 100644 --- a/Stdlib/Data/Result.juvix +++ b/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 + }; diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix index 3a882410..e3952ffe 100644 --- a/Stdlib/Data/Unit.juvix +++ b/Stdlib/Data/Unit.juvix @@ -1,6 +1,7 @@ --- 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; @@ -8,10 +9,6 @@ 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}; diff --git a/Stdlib/Data/Unit/Base.juvix b/Stdlib/Data/Unit/Base.juvix new file mode 100644 index 00000000..5f8df2c1 --- /dev/null +++ b/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; diff --git a/Stdlib/Trait.juvix b/Stdlib/Trait.juvix index 13e0c04a..8e3a99aa 100644 --- a/Stdlib/Trait.juvix +++ b/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; diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix new file mode 100644 index 00000000..d556da7c --- /dev/null +++ b/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; diff --git a/test/Package.juvix b/test/Package.juvix index 7eb65859..2aa5c8a7 100644 --- a/test/Package.juvix +++ b/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"] }; diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml index 0741d8af..77e7f93b 100644 --- a/test/juvix.lock.yaml +++ b/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: []