Add test for #25

tests/Main.idr

@@ -36,7 +36,7 @@ idrisTests
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
        "interface001", "interface002", "interface003", "interface004",
-       "interface005",
+       "interface005", "interface006",
        "lazy001",
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",

tests/idris2/interface006/Apply.idr

@@ -0,0 +1,90 @@
+module Apply
+
+-- These are not Biapplicatives.  Those are in Data.Biapplicative
+
+import Bifunctor
+
+infixl 4 <<$>>, <<&>>, <<.>>, <<., .>>, <<..>>
+
+||| Primarily used to make the definitions of bilift2 and bilift3 pretty
+|||
+||| ```idris example
+||| bimap const const <<$>> (1, 2) <<.>> (3, 4) == (1, 2)
+||| ```
+|||
+export
+(<<$>>) : (a -> b) -> a -> b
+(<<$>>) = id
+
+||| <<$>> with the arguments reversed
+|||
+||| ```idris example
+||| (1, 2) <<&>> bimap const const <<.>> (3, 4) == (1, 2)
+||| ```
+|||
+(<<&>>) : a -> (a -> b) -> b
+(<<&>>) = flip id
+
+||| Biapplys (not to be confused with Biapplicatives)
+||| @p The action of the Biapply on pairs of objects
+public export
+interface Bifunctor p => Biapply (p : Type -> Type -> Type) where
+
+  ||| Applys a Bifunctor of functions to another Bifunctor of the same type
+  |||
+  ||| ````idris example
+  ||| (reverse, (\x => x + 1)) <<.>> ("hello", 1) == ("olleh", 2)
+  ||| ````
+  |||
+  (<<.>>) : p (a -> b) (c -> d) -> p a c -> p b d
+
+  ||| Given two Bifunctors, sequences them leftwards
+  |||
+  ||| ````idris example
+  ||| ("hello", 1) <<. ("goodbye", 2) == ("hello", 1)
+  ||| ````
+  |||
+  (<<.) : p a b -> p c d -> p a b
+  a <<. b = bimap const const <<$>> a <<.>> b
+
+  ||| Given two Bifunctors, sequences them rightwards
+  |||
+  ||| ````idris example
+  ||| ("hello", 1) <<. ("goodbye", 2) == ("goodbye", 2)
+  ||| ````
+  |||
+  (.>>) : p a b -> p c d -> p c d
+  a .>> b = bimap (const id) (const id) <<$>> a <<.>> b
+
+||| Lifts a pair of binary functions into a Bifunctor
+|||
+||| ````idris example
+||| bilift2 (++) (+) ("hello", 1) ("goodbye", 2) == ("hellogoodbye", 3)
+||| ````
+|||
+bilift2 : Biapply p => (a -> b -> c) -> (d -> e -> f) -> p a d -> p b e -> p c f
+bilift2 f g a b = bimap f g <<$>> a <<.>> b
+
+||| Lifts a pair of ternary functions into a Bifunctor
+|||
+||| ````idris example
+||| bilift3 (\x,y,z => x ++ (y ++ z)) (\x,y,z => x + (y + z))
+|||         ("hello", 1) ("goodbye", 2) ("hello again", 3) ==
+||| ("hellogoodbyehello again", 6)
+||| ````
+|||
+bilift3 : Biapply p => (a -> b -> c -> d) -> (e -> f -> g -> h)
+        -> p a e -> p b f -> p c g -> p d h
+bilift3 f g a b c = bimap f g <<$>> a <<.>> b <<.>> c
+
+||| Applies the second of two Bifunctors to the first
+|||
+||| ````idris example
+||| ("hello", 1) <<..>> (reverse, (\x => x + 1)) == ("olleh", 2)
+||| ````
+|||
+(<<..>>): Biapply p => p a c -> p (a -> b) (c -> d) -> p b d
+(<<..>>) = flip (<<.>>)
+
+implementation Biapply Pair where
+  (f, g) <<.>> (a, b) = (f a, g b)

tests/idris2/interface006/Biapplicative.idr

@@ -0,0 +1,70 @@
+module Biapplicative
+
+import Bifunctor
+import Apply
+
+infixl 4 <<*>>, <<*, *>>, <<**>>
+
+||| Biapplicatives
+||| @p the action of the Biapplicative on pairs of objects
+public export
+interface Bifunctor p => Biapplicative p where -- (p : Type -> Type -> Type) where
+
+  ||| Lifts two values into a Biapplicative
+  |||
+  ||| ````idris example
+  ||| bipure 1 "hello" = (1, "hello")
+  ||| ````
+  |||
+  bipure : a -> b -> p a b
+
+  ||| Applies a Biapplicative of functions to a second Biapplicative
+  |||
+  ||| ````idris example
+  ||| ( (\x => x + 1), reverse ) <<*>> (1, "hello") == (2, "olleh")
+  ||| ````
+  |||
+  (<<*>>) : p (a -> b) (c -> d) -> p a c -> p b d
+
+  ||| Sequences two Biapplicatives rightwards
+  |||
+  ||| ````idris example
+  ||| (1, "hello") *>> (2, "goodbye") = (2, "goodbye")
+  ||| ````
+  |||
+  (*>>) : p a b -> p c d -> p c d
+  a *>> b = bimap (const id) (const id) <<$>> a <<*>> b
+
+  ||| Sequences two Biapplicatives leftwards
+  |||
+  ||| ````idris example
+  ||| (1, "hello") <<* (2, "goodbye") = (1, "hello")
+  ||| ````
+  |||
+  (<<*) : p a b -> p c d -> p a b
+  a <<* b = bimap const const <<$>> a <<*>> b
+
+||| Applies the second of two Biapplicatives to the first
+|||
+||| ````idris example
+||| (1, "hello") <<**>> ( (\x => x + 1), reverse ) == (2, "olleh")
+||| ````
+|||
+export
+(<<**>>) : Biapplicative p => p a c -> p (a -> b) (c -> d) -> p b d
+(<<**>>) = flip (<<*>>)
+
+export
+biliftA2 : Biapplicative p => (a -> b -> c) ->
+                              (d -> e -> f) -> p a d -> p b e -> p c f
+biliftA2 f g a b = bimap f g <<$>> a <<*>> b
+
+export
+biliftA3 : Biapplicative p =>
+  (a -> b -> c -> d) -> (e -> f -> g -> h) -> p a e -> p b f -> p c g -> p d h
+biliftA3 f g a b c = bimap f g <<$>> a <<*>> b <<*>> c
+
+public export
+implementation Biapplicative Pair where
+  bipure a b          = (a, b)
+  (f, g) <<*>> (a, b) = (f a, g b)

tests/idris2/interface006/Bifunctor.idr

@@ -0,0 +1,40 @@
+module Bifunctor
+
+||| Bifunctors
+||| @p The action of the Bifunctor on pairs of objects
+public export
+interface Bifunctor (p : Type -> Type -> Type) where
+  ||| The action of the Bifunctor on pairs of morphisms
+  |||
+  ||| ````idris example
+  ||| bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")
+  ||| ````
+  |||
+  bimap : (a -> b) -> (c -> d) -> p a c -> p b d
+  bimap f g = first f . second g
+
+  ||| The action of the Bifunctor on morphisms pertaining to the first object
+  |||
+  ||| ````idris example
+  ||| first (\x => x + 1) (1, "hello") == (2, "hello")
+  ||| ````
+  |||
+  first : (a -> b) -> p a c -> p b c
+  first = flip bimap id
+
+  ||| The action of the Bifunctor on morphisms pertaining to the second object
+  |||
+  ||| ````idris example
+  ||| second reverse (1, "hello") == (1, "olleh")
+  ||| ````
+  |||
+  second : (a -> b) -> p c a -> p c b
+  second = bimap id
+
+implementation Bifunctor Either where
+  bimap f _ (Left  a) = Left  $ f a
+  bimap _ g (Right b) = Right $ g b
+
+public export
+implementation Bifunctor Pair where
+  bimap f g (a, b) = (f a, g b)

tests/idris2/interface006/Bimonad.idr

@@ -0,0 +1,24 @@
+module Bimonad
+
+import Bifunctor
+import Biapplicative
+
+infixl 4 >>==
+
+||| Bimonads
+||| @p the action of the first Bifunctor component on pairs of objects
+||| @q the action of the second Bifunctor component on pairs of objects
+interface (Biapplicative p, Biapplicative q) =>
+      Bimonad (p : Type -> Type -> Type) (q : Type -> Type -> Type) where
+
+  bijoin : (p (p a b) (q a b), q (p a b) (q a b)) -> (p a b, q a b)
+  bijoin p = p >>== (id, id)
+
+  (>>==) : (p a b, q a b) -> ((a -> p c d), (b -> q c d)) -> (p c d, q c d)
+  (pab, qab) >>== (f, g) = bijoin $ (bimap f g, bimap f g) <<*>> (pab, qab)
+
+biunit : (Bimonad p q) => a -> b -> (p a b, q a b)
+biunit a b = (bipure a b, bipure a b)
+
+implementation Bimonad Pair Pair where
+  bijoin = bimap fst snd

tests/idris2/interface006/expected

@@ -0,0 +1,4 @@
+1/4: Building Bifunctor (Bifunctor.idr)
+2/4: Building Apply (Apply.idr)
+3/4: Building Biapplicative (Biapplicative.idr)
+4/4: Building Bimonad (Bimonad.idr)

tests/idris2/interface006/run

@@ -0,0 +1,3 @@
+$1 --check Bimonad.idr
+
+rm -rf build