More compose instances and one usage of them (#1089)

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)
+            (S offset') => (fSeekLine h *> readLinesOnto acc offset' (More fuel) h) @{Applicative.Compose}
-            0           => try (fGetLine  h) (\str => readLinesOnto (str :: acc) 0 fuel h)
+            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

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

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 []

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"

tests/idris2/interface023/expected

@@ -0,0 +1,5 @@
+1/1: Building AppComp (AppComp.idr)
+AppComp> True
+AppComp> True
+AppComp> True
+AppComp> Bye for now!

tests/idris2/interface023/input

@@ -0,0 +1,4 @@
+r1
+r2
+r3
+:q

tests/idris2/interface023/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 AppComp.idr < input
+
+rm -rf build