From 1d99a281761b1d54c15a8b167aeeca236e3e5a65 Mon Sep 17 00:00:00 2001
From: Ruslan Feizerahmanov <russoulmc@gmail.com>
Date: Wed, 30 Sep 2020 12:51:07 +0300
Subject: [PATCH] Add Bifunctor interface (#701)

---
 idris2api.ipkg                              |  1 -
 libs/base/Data/Either.idr                   |  5 ---
 {src => libs/base}/Data/These.idr           | 20 +++++-----
 libs/base/base.ipkg                         |  1 +
 libs/prelude/Prelude/Interfaces.idr         | 41 ++++++++++++++++++--
 libs/prelude/Prelude/Types.idr              | 42 ++++++++++++---------
 src/Idris/Error.idr                         | 16 +++-----
 tests/idris2/interface006/Apply.idr         |  2 -
 tests/idris2/interface006/Biapplicative.idr |  1 -
 tests/idris2/interface006/Bifunctor.idr     | 40 --------------------
 tests/idris2/interface006/Bimonad.idr       |  1 -
 tests/idris2/interface006/expected          |  7 ++--
 12 files changed, 82 insertions(+), 95 deletions(-)
 rename {src => libs/base}/Data/These.idr (82%)
 delete mode 100644 tests/idris2/interface006/Bifunctor.idr

diff --git a/idris2api.ipkg b/idris2api.ipkg
index 840b84955..27dc669a0 100644
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@@ -65,7 +65,6 @@ modules =
     Data.NameMap,
     Data.StringMap,
     Data.StringTrie,
-    Data.These,
 
     Data.Bool.Extra,
 
diff --git a/libs/base/Data/Either.idr b/libs/base/Data/Either.idr
index d99b8627d..81ff22bc4 100644
--- a/libs/base/Data/Either.idr
+++ b/libs/base/Data/Either.idr
@@ -94,11 +94,6 @@ mirror (Right x) = Left x
 --------------------------------------------------------------------------------
 -- Bifunctor
 
-export
-bimap : (a -> c) -> (b -> d) -> Either a b -> Either c d
-bimap l r (Left a) = Left (l a)
-bimap l r (Right b) = Right (r b)
-
 export
 pushInto : c -> Either a b -> Either (c, a) (c, b)
 pushInto c = bimap (\ a => (c, a)) (\ b => (c, b))
diff --git a/src/Data/These.idr b/libs/base/Data/These.idr
similarity index 82%
rename from src/Data/These.idr
rename to libs/base/Data/These.idr
index 4a4d47915..f99af5fd8 100644
--- a/src/Data/These.idr
+++ b/libs/base/Data/These.idr
@@ -27,25 +27,23 @@ these l r lr (This a)   = l a
 these l r lr (That b)   = r b
 these l r lr (Both a b) = lr a b
 
-public export
-bimap : (f : a -> b) -> (g : c -> d) -> These a c -> These b d
-bimap f g (This a)   = This (f a)
-bimap f g (That b)   = That (g b)
-bimap f g (Both a b) = Both (f a) (g b)
-
 public export
 (Show a, Show b) => Show (These a b) where
   showPrec d (This x)   = showCon d "This" $ showArg x
   showPrec d (That x)   = showCon d "That" $ showArg x
   showPrec d (Both x y) = showCon d "Both" $ showArg x ++ showArg y
 
+%inline
+public export
+Bifunctor These where
+  bimap f g (This a)   = This (f a)
+  bimap f g (That b)   = That (g b)
+  bimap f g (Both a b) = Both (f a) (g b)
+
+%inline
 public export
 Functor (These a) where
-  map = bimap id
-
-public export
-mapFst : (f : a -> b) -> These a c -> These b c
-mapFst f = bimap f id
+  map = mapSnd
 
 public export
 bifold : Monoid m => These m m -> m
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 6bd6288eb..259d2ab3e 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -40,6 +40,7 @@ modules = Control.App,
           Data.So,
           Data.Stream,
           Data.Strings,
+          Data.These,
           Data.Vect,
           Data.Vect.Elem,
           Data.Vect.Quantifiers,
diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr
index 22a1107d2..6bbbede8b 100644
--- a/libs/prelude/Prelude/Interfaces.idr
+++ b/libs/prelude/Prelude/Interfaces.idr
@@ -69,9 +69,9 @@ export
 shiftR : Int -> Int -> Int
 shiftR = prim__shr_Int
 
-----------------------------------------------
--- FUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
-----------------------------------------------
+---------------------------------------------------------
+-- FUNCTOR, BIFUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
+---------------------------------------------------------
 
 ||| Functors allow a uniform action over a parameterised type.
 ||| @ f a parameterised type
@@ -105,6 +105,41 @@ public export
 ignore : Functor f => f a -> f ()
 ignore = map (const ())
 
+||| Bifunctors
+||| @f The action of the Bifunctor on pairs of objects
+public export
+interface Bifunctor f where
+  ||| The action of the Bifunctor on pairs of morphisms
+  |||
+  ||| ````idris example
+  ||| bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")
+  ||| ````
+  |||
+  bimap : (a -> c) -> (b -> d) -> f a b -> f c d
+  bimap f g = mapFst f . mapSnd g
+
+  ||| The action of the Bifunctor on morphisms pertaining to the first object
+  |||
+  ||| ````idris example
+  ||| mapFst (\x => x + 1) (1, "hello") == (2, "hello")
+  ||| ````
+  |||
+  mapFst : (a -> c) -> f a b -> f c b
+  mapFst f = bimap f id
+
+  ||| The action of the Bifunctor on morphisms pertaining to the second object
+  |||
+  ||| ````idris example
+  ||| mapSnd reverse (1, "hello") == (1, "olleh")
+  ||| ````
+  |||
+  mapSnd : (b -> d) -> f a b -> f a d
+  mapSnd = bimap id
+
+public export
+mapHom : Bifunctor f => (a -> b) -> f a a -> f b b
+mapHom f = bimap f f
+
 public export
 interface Functor f => Applicative f where
   pure : a -> f a
diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
index 96cd07bdd..7f2442b4f 100644
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@@ -85,13 +85,15 @@ natToInteger (S k) = 1 + natToInteger k
 -- PAIRS --
 -----------
 
+%inline
+public export
+Bifunctor Pair where
+  bimap f g (x, y) = (f x, g y)
+
+%inline
 public export
 Functor (Pair a) where
-  map f (x, y) = (x, f y)
-
-public export
-mapFst : (a -> c) -> (a, b) -> (c, b)
-mapFst f (x, y) = (f x, y)
+  map = mapSnd
 
 -----------
 -- MAYBE --
@@ -157,10 +159,10 @@ Applicative Maybe where
 
 public export
 Alternative Maybe where
-    empty = Nothing
+  empty = Nothing
 
-    (Just x) <|> _ = Just x
-    Nothing  <|> v = v
+  (Just x) <|> _ = Just x
+  Nothing  <|> v = v
 
 public export
 Monad Maybe where
@@ -235,17 +237,23 @@ Functor (Either e) where
 
 %inline
 public export
-Applicative (Either e) where
-    pure = Right
+Bifunctor Either where
+  bimap f _ (Left x) = Left (f x)
+  bimap _ g (Right y) = Right (g y)
 
-    (Left a) <*> _          = Left a
-    (Right f) <*> (Right r) = Right (f r)
-    (Right _) <*> (Left l)  = Left l
+%inline
+public export
+Applicative (Either e) where
+  pure = Right
+
+  (Left a) <*> _          = Left a
+  (Right f) <*> (Right r) = Right (f r)
+  (Right _) <*> (Left l)  = Left l
 
 public export
 Monad (Either e) where
-    (Left n) >>= _ = Left n
-    (Right r) >>= f = f r
+  (Left n) >>= _ = Left n
+  (Right r) >>= f = f r
 
 public export
 Foldable (Either e) where
@@ -327,8 +335,8 @@ Applicative List where
 
 public export
 Alternative List where
-    empty = []
-    (<|>) = (++)
+  empty = []
+  (<|>) = (++)
 
 public export
 Monad List where
diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr
index aafadbff7..cea399fec 100644
--- a/src/Idris/Error.idr
+++ b/src/Idris/Error.idr
@@ -59,8 +59,8 @@ ploc : {auto o : Ref ROpts REPLOpts} ->
        FC -> Core (Doc IdrisAnn)
 ploc EmptyFC = pure emptyDoc
 ploc fc@(MkFC fn s e) = do
-    let (sr, sc) = bimap (fromInteger . cast) s
-    let (er, ec) = bimap (fromInteger . cast) e
+    let (sr, sc) = mapHom (fromInteger . cast) s
+    let (er, ec) = mapHom (fromInteger . cast) e
     let nsize = length $ show (er + 1)
     let head = annotate FileCtxt (pretty fc)
     source <- lines <$> getCurrentElabSource
@@ -72,8 +72,6 @@ ploc fc@(MkFC fn s e) = do
          pure $ vsep [emptyDoc, head, firstRow, annotate FileCtxt (space <+> pretty (sr + 1)) <++> align (vsep [line, emph]), emptyDoc]
        else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line
   where
-    bimap : (a -> b) -> (a, a) -> (b, b)
-    bimap f (x, y) = (f x, f y)
     extractRange : Nat -> Nat -> List String -> List String
     extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
     pad : Nat -> String -> String
@@ -88,10 +86,10 @@ ploc2 : {auto o : Ref ROpts REPLOpts} ->
 ploc2 fc EmptyFC = ploc fc
 ploc2 EmptyFC fc = ploc fc
 ploc2 (MkFC fn1 s1 e1) (MkFC fn2 s2 e2) =
-    do let (sr1, sc1) = bimap (fromInteger . cast) s1
-       let (sr2, sc2) = bimap (fromInteger . cast) s2
-       let (er1, ec1) = bimap (fromInteger . cast) e1
-       let (er2, ec2) = bimap (fromInteger . cast) e2
+    do let (sr1, sc1) = mapHom (fromInteger . cast) s1
+       let (sr2, sc2) = mapHom (fromInteger . cast) s2
+       let (er1, ec1) = mapHom (fromInteger . cast) e1
+       let (er2, ec2) = mapHom (fromInteger . cast) e2
        if (er2 > the Nat (er1 + 5))
           then pure $ !(ploc (MkFC fn1 s1 e1)) <+> line <+> !(ploc (MkFC fn2 s2 e2))
           else do let nsize = length $ show (er2 + 1)
@@ -134,8 +132,6 @@ ploc2 (MkFC fn1 s1 e1) (MkFC fn2 s2 e2) =
                          pure $ vsep $ [emptyDoc, head, firstRow] ++ top ++ [fileCtxt (space <+> pretty (sr2 + 1)) <++> align (vsep [line, emph]), emptyDoc]
                        (_, _, _) => pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr1 (pretty <$> extractRange sr1 er2 source)) <+> line
   where
-    bimap : (a -> b) -> (a, a) -> (b, b)
-    bimap f (x, y) = (f x, f y)
     extractRange : Nat -> Nat -> List String -> List String
     extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
     pad : Nat -> String -> String
diff --git a/tests/idris2/interface006/Apply.idr b/tests/idris2/interface006/Apply.idr
index 01bb3e3a3..3183548e5 100644
--- a/tests/idris2/interface006/Apply.idr
+++ b/tests/idris2/interface006/Apply.idr
@@ -2,8 +2,6 @@ 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
diff --git a/tests/idris2/interface006/Biapplicative.idr b/tests/idris2/interface006/Biapplicative.idr
index 0168d19fb..00c564309 100644
--- a/tests/idris2/interface006/Biapplicative.idr
+++ b/tests/idris2/interface006/Biapplicative.idr
@@ -1,6 +1,5 @@
 module Biapplicative
 
-import Bifunctor
 import Apply
 
 infixl 4 <<*>>, <<*, *>>, <<**>>
diff --git a/tests/idris2/interface006/Bifunctor.idr b/tests/idris2/interface006/Bifunctor.idr
deleted file mode 100644
index 2b4f4a41f..000000000
--- a/tests/idris2/interface006/Bifunctor.idr
+++ /dev/null
@@ -1,40 +0,0 @@
-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)
diff --git a/tests/idris2/interface006/Bimonad.idr b/tests/idris2/interface006/Bimonad.idr
index bc200646a..cdaded2a0 100644
--- a/tests/idris2/interface006/Bimonad.idr
+++ b/tests/idris2/interface006/Bimonad.idr
@@ -1,6 +1,5 @@
 module Bimonad
 
-import Bifunctor
 import Biapplicative
 
 infixl 4 >>==
diff --git a/tests/idris2/interface006/expected b/tests/idris2/interface006/expected
index 4139aa00b..ff9bcc0ea 100644
--- a/tests/idris2/interface006/expected
+++ b/tests/idris2/interface006/expected
@@ -1,4 +1,3 @@
-1/4: Building Bifunctor (Bifunctor.idr)
-2/4: Building Apply (Apply.idr)
-3/4: Building Biapplicative (Biapplicative.idr)
-4/4: Building Bimonad (Bimonad.idr)
+1/3: Building Apply (Apply.idr)
+2/3: Building Biapplicative (Biapplicative.idr)
+3/3: Building Bimonad (Bimonad.idr)