diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix index 9ac1bd11..d5c17ba1 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; 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/Applicative.juvix b/Stdlib/Trait/Applicative.juvix index 815860f3..54f08164 100644 --- a/Stdlib/Trait/Applicative.juvix +++ b/Stdlib/Trait/Applicative.juvix @@ -2,6 +2,8 @@ module Stdlib.Trait.Applicative; import Stdlib.Data.Fixity open; import Stdlib.Trait.Functor open; +import Stdlib.Trait.Foldable.Polymorphic open; +import Stdlib.Data.Unit.Base open; trait type Applicative (f : Type -> Type) := @@ -17,3 +19,14 @@ open Applicative public; --- 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; + +syntax iterator mapM_ {init := 0; range := 1}; +mapM_ + {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};