diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index b254335ab..1770da0e5 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -323,9 +323,6 @@ withFile filename mode onError onOpen = closeFile h pure res -try : Monad m => m (Either FileError a) -> (a -> m (Either FileError b)) -> m (Either FileError b) -try a f = a >>= either (pure . Left) f - readLinesOnto : HasIO io => (acc : List String) -> (offset : Nat) -> (fuel : Fuel) -> @@ -336,8 +333,8 @@ readLinesOnto acc offset (More fuel) h = do False <- fEOF h | True => pure $ Right (True, reverse acc) case offset of - (S offset') => try (fSeekLine h) (const $ readLinesOnto acc offset' (More fuel) h) - 0 => try (fGetLine h) (\str => readLinesOnto (str :: acc) 0 fuel h) + (S offset') => (fSeekLine h *> readLinesOnto acc offset' (More fuel) h) @{Applicative.Compose} + 0 => (fGetLine h >>= \str => readLinesOnto (str :: acc) 0 fuel h) @{Monad.Compose} ||| Read a chunk of a file in a line-delimited fashion. ||| You can use this function to read an entire file diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 43ee24d60..ea8447688 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -107,9 +107,9 @@ ignore = map (const ()) namespace Functor ||| Composition of functors is a functor. - export + public export [Compose] (Functor f, Functor g) => Functor (f . g) where - map fun = map (map fun) + map = map . map ||| Bifunctors ||| @f The action of the Bifunctor on pairs of objects @@ -165,12 +165,11 @@ a *> b = map (const id) a <*> b namespace Applicative ||| Composition of applicative functors is an applicative functor. - export + public export [Compose] (Applicative f, Applicative g) => Applicative (f . g) using Functor.Compose where pure = pure . pure - - fun <*> x = ((<*>) <$> fun <*> x) + fun <*> x = [| fun <*> x |] public export interface Applicative f => Alternative f where @@ -368,6 +367,14 @@ public export choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b choiceMap f = foldr (\e, a => f e <|> a) empty +namespace Foldable + ||| Composition of foldables is foldable. + public export + [Compose] (Foldable t, Foldable f) => Foldable (t . f) where + foldr = foldr . flip . foldr + foldl = foldl . foldl + null tf = null tf || all (force . null) tf + public export interface (Functor t, Foldable t) => Traversable t where ||| Map each element of a structure to a computation, evaluate those @@ -383,3 +390,17 @@ sequence = traverse id public export for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b) for = flip traverse + +namespace Traversable + ||| Composition of traversables is traversable. + public export + [Compose] (Traversable t, Traversable f) => Traversable (t . f) + using Foldable.Compose Functor.Compose where + traverse = traverse . traverse + +namespace Monad + ||| Composition of a traversable monad and a monad is a monad. + public export + [Compose] (Monad m, Monad t, Traversable t) => Monad (m . t) + using Applicative.Compose where + a >>= f = a >>= map join . traverse f diff --git a/tests/Main.idr b/tests/Main.idr index 9f58740f9..05fd99abb 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -85,7 +85,7 @@ idrisTestsInterface = MkTestPool [] "interface009", "interface010", "interface011", "interface012", "interface013", "interface014", "interface015", "interface016", "interface017", "interface018", "interface019", "interface020", - "interface021", "interface022"] + "interface021", "interface022", "interface023"] idrisTestsLinear : TestPool idrisTestsLinear = MkTestPool [] diff --git a/tests/idris2/interface023/AppComp.idr b/tests/idris2/interface023/AppComp.idr new file mode 100644 index 000000000..10b57f67f --- /dev/null +++ b/tests/idris2/interface023/AppComp.idr @@ -0,0 +1,36 @@ +module AppComp + +import Control.Monad.Error.Either +import Control.Monad.Identity + +-- Errorful monadic functions -- + +f1 : Monad m => Int -> m (Either String Int) +f1 5 = pure $ Right 0 +f1 _ = pure $ Left "fail 1" + +f2 : Monad m => Int -> m (Either String Int) +f2 6 = pure $ Right 0 +f2 _ = pure $ Left "fail 2" + +-- Compositions -- + +c1 : Monad m => m (Either String Int) +c1 = f1 1 *> f2 1 + +c2 : Monad m => m (Either String Int) +c2 = (f1 1 *> f2 1) @{Applicative.Compose} + +c3 : Monad m => m (Either String Int) +c3 = runEitherT $ MkEitherT {m} (f1 1) *> MkEitherT {m} (f2 1) + +-- These checks are meant to be true -- + +r1 : Bool +r1 = runIdentity c1 == Left "fail 2" + +r2 : Bool +r2 = runIdentity c2 == Left "fail 1" + +r3 : Bool +r3 = runIdentity c3 == Left "fail 1" diff --git a/tests/idris2/interface023/expected b/tests/idris2/interface023/expected new file mode 100644 index 000000000..b3fb6d293 --- /dev/null +++ b/tests/idris2/interface023/expected @@ -0,0 +1,5 @@ +1/1: Building AppComp (AppComp.idr) +AppComp> True +AppComp> True +AppComp> True +AppComp> Bye for now! diff --git a/tests/idris2/interface023/input b/tests/idris2/interface023/input new file mode 100644 index 000000000..4f37bec29 --- /dev/null +++ b/tests/idris2/interface023/input @@ -0,0 +1,4 @@ +r1 +r2 +r3 +:q diff --git a/tests/idris2/interface023/run b/tests/idris2/interface023/run new file mode 100644 index 000000000..4c94f3194 --- /dev/null +++ b/tests/idris2/interface023/run @@ -0,0 +1,3 @@ +$1 --no-banner --no-color --console-width 0 AppComp.idr < input + +rm -rf build