[ new ] Add Compose instances for Bi* interfaces, analogous to present

CHANGELOG.md

@@ -62,7 +62,7 @@
   file will not lead to a positivity error anymore.
 
 * Fixed a bug in the positivity checker that meant `Lazy` could be used
-  to hide negative occurences.
+  to hide negative occurrences.
 
 * Made sure that the positivity checker now respects `assert_total` annotations.
 
@@ -90,9 +90,13 @@
 * Improved performance of functions `isNL`, `isSpace`, and `isHexDigit`.
 
 * Implements `Foldable` and `Traversable` for pairs, right-biased as `Functor`.
+
 * Added a constructor (`MkInterpolation`) to `Interpolation`.
+
 * Added an `Interpolation` implementation for `Void`.
 
+* Added `Compose` instances for `Bifunctor`, `Bifoldable` and `Bitraversable`.
+
 #### Base
 
 * Deprecates `setByte` and `getByte` from `Data.Buffer` for removal in a future
@@ -104,9 +108,9 @@
 * Add `Show` instance to `Data.Vect.Quantifiers.All` and add a few helpers for listy
   computations on the `All` type.
 * Add an alias for `HVect` to `All id` in `Data.Vect.Quantifiers.All`. This is the
-  approach to getting a heterogeneous Vect of elements that is generall preferred by
+  approach to getting a heterogeneous `Vect` of elements that is general preferred by
   the community vs. a standalone type as seen in `contrib`.
-* Add Data.List.HasLength from the compiler codebase slash contrib library but
+* Add `Data.List.HasLength` from the compiler codebase slash contrib library but
   adopt the type signature from the compiler codebase and some of the naming
   from the contrib library. The type ended up being `HasLength n xs` rather than
   `HasLength xs n`.

libs/prelude/Prelude/Interfaces.idr

@@ -160,6 +160,15 @@ public export
 mapHom : Bifunctor f => (a -> b) -> f a a -> f b b
 mapHom f = bimap f f
 
+namespace Bifunctor
+
+  ||| Composition of a bifunctor and a functor is a bifunctor.
+  public export %inline
+  [Compose] (l : Functor f) => (r : Bifunctor g) => Bifunctor (f .: g) where
+    bimap = map .: bimap
+    mapFst = map . mapFst
+    mapSnd = map . mapSnd
+
 public export
 interface Functor f => Applicative f where
   constructor MkApplicative
@@ -520,6 +529,15 @@ public export
 bifoldMapFst : Monoid acc => Bifoldable p => (a -> acc) -> p a b -> acc
 bifoldMapFst f = bifoldMap f (const neutral)
 
+namespace Bifoldable
+
+  ||| Composition of a bifoldable and a foldable is bifoldable.
+  public export
+  [Compose] (l : Foldable f) => (r : Bifoldable p) => Bifoldable (f .: p) where
+    bifoldr = foldr .: flip .: bifoldr
+    bifoldl = foldl .: bifoldl
+    binull fp = null fp || all binull fp
+
 public export
 interface (Functor t, Foldable t) => Traversable t where
   constructor MkTraversable
@@ -565,6 +583,14 @@ namespace Traversable
     using Foldable.Compose Functor.Compose where
       traverse = traverse . traverse
 
+namespace Bitraveresable
+
+  ||| Composition of a bitraversable and a traversable is bitraversable.
+  public export
+  [Compose] (l : Traversable t) => (r : Bitraversable p) => Bitraversable (t .: p)
+    using Bifoldable.Compose Bifunctor.Compose where
+      bitraverse = traverse .: bitraverse
+
 namespace Monad
   ||| Composition of a traversable monad and a monad is a monad.
   public export

tests/idris2/spec001/expected

@@ -1,12 +1,12 @@
 1/1: Building Mult3 (Mult3.idr)
-LOG specialise.declare:5: Specialising Main.smult ($resolved2551) -> _PE.PE_smult_4e8901402355876e by (0, Static (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))), (1, Dynamic)
+LOG specialise.declare:5: Specialising Main.smult ($resolved2645) -> _PE.PE_smult_4e8901402355876e by (0, Static (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))), (1, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_smult_4e8901402355876e: (n : Prelude.Types.Nat) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
 ((Main.smult Prelude.Types.Z) n) = Prelude.Types.Z
 ((Main.smult (Prelude.Types.S Prelude.Types.Z)) n) = n
 ((Main.smult (Prelude.Types.S m)) n) = ((((Prelude.Num.+ [ty = Prelude.Types.Nat]) [__con = Prelude.Types.Num implementation at Prelude.Types:66:1--71:33]) n) ((Main.smult m) n))
 LOG specialise:5: New patterns for _PE.PE_smult_4e8901402355876e:
-(_PE.PE_smult_4e8901402355876e $_pe0) = (($resolved2551 (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) _pe0)
+(_PE.PE_smult_4e8901402355876e $_pe0) = (($resolved2645 (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) _pe0)
 LOG specialise:5: New RHS: (Prelude.Types.plus _pe0[0] (Prelude.Types.plus _pe0[0] _pe0[0]))
 LOG specialise:5: Already specialised _PE.PE_smult_4e8901402355876e
 /* Main.main : IO () */
@@ -16,7 +16,7 @@ function Main_main($0) {
  return Prelude_IO_prim__putStr((Prelude_Show_show_Show_Nat(($4+($4+$4)))+'\n'), $0);
 }
 1/1: Building Desc (Desc.idr)
-LOG specialise.declare:5: Specialising Desc.fold ($resolved2664) -> _PE.PE_fold_3a845f1ca594c582 by (0, Dynamic), (1, Static (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))), (2, Dynamic)
+LOG specialise.declare:5: Specialising Desc.fold ($resolved2758) -> _PE.PE_fold_3a845f1ca594c582 by (0, Dynamic), (1, Static (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))), (2, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_3a845f1ca594c582: {0 a : Type} -> ({arg:936} : ({arg:938} : (Desc.Meaning (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)) a[0])) -> a[1]) -> ({arg:943} : (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) -> a[2]
 LOG specialise:5: Attempting to specialise:
 ((((Desc.fold [a = a]) [d = d]) alg) ((Desc.MkMu [d = d]) t)) = (alg (((((Desc.fmap [b = a]) [a = ?a]) d) ((Builtin.assert_total [a = ?a]) (((Desc.fold [a = a]) [d = d]) alg))) t))
@@ -27,13 +27,13 @@ LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.bimap (Builtin.Pair a[1] a[1]) (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) Builtin.Unit Builtin.Unit (Prelude.Basics.id Builtin.Unit) \({arg:2} : (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))))) => (Prelude.Types.bimap a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) {arg:2}[0]) t[2]))
 LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
 1/1: Building Desc2 (Desc2.idr)
-LOG specialise.declare:5: Specialising Main.fold ($resolved2574) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8743}[0]))), (3, Dynamic)
+LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8743}[0]))), (3, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
 (((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
 LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e:
 ((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) alg)) t))
-LOG specialise.declare:5: Specialising Main.fold ($resolved2574) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8743}[0]))), (3, Dynamic)
+LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8743}[0]))), (3, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
 (((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
@@ -47,7 +47,7 @@ LOG specialise:5: Already specialised _PE.PE_fold_8abb50b713fe8e5e
 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1]))
 LOG specialise:5: Already specialised _PE.PE_fold_8abb50b713fe8e5e
 1/1: Building Identity (Identity.idr)
-LOG specialise.declare:5: Specialising Main.identity ($resolved2551) -> _PE.PE_identity_3c7f5598e5c9b732 by (0, Static Prelude.Types.Nat), (1, Dynamic)
+LOG specialise.declare:5: Specialising Main.identity ($resolved2645) -> _PE.PE_identity_3c7f5598e5c9b732 by (0, Static Prelude.Types.Nat), (1, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_identity_3c7f5598e5c9b732: ({arg:813} : (Prelude.Basics.List Prelude.Types.Nat)) -> (Prelude.Basics.List Prelude.Types.Nat)
 LOG specialise:5: Attempting to specialise:
 ((Main.identity [a = a]) (Prelude.Basics.Nil [a = a])) = (Prelude.Basics.Nil [a = a])