{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2014-2015 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  Rank2Types
--
----------------------------------------------------------------------------
module Data.Profunctor.Choice
  (
  -- * Strength
    Choice(..)
  , TambaraSum(..)
  , tambaraSum, untambaraSum
  , PastroSum(..)
  -- * Costrength
  , Cochoice(..)
  , CotambaraSum(..)
  , cotambaraSum, uncotambaraSum
  , CopastroSum(..)
  ) where

import Control.Applicative hiding (WrappedArrow(..))
import Control.Arrow
import Control.Category
import Control.Comonad
import Data.Bifunctor.Joker (Joker(..))
import Data.Bifunctor.Product (Product(..))
import Data.Bifunctor.Sum (Sum(..))
import Data.Bifunctor.Tannen (Tannen(..))
import Data.Monoid hiding (Product, Sum)
import Data.Profunctor.Adjunction
import Data.Profunctor.Monad
import Data.Profunctor.Strong
import Data.Profunctor.Types
import Data.Profunctor.Unsafe
import Data.Tagged

#if __GLASGOW_HASKELL__ < 710
import Data.Traversable
import Prelude hiding (id,(.),sequence)
#else
import Prelude hiding (id,(.))
#endif

------------------------------------------------------------------------------
-- Choice
------------------------------------------------------------------------------

-- | The generalization of 'Costar' of 'Functor' that is strong with respect
-- to 'Either'.
--
-- Note: This is also a notion of strength, except with regards to another monoidal
-- structure that we can choose to equip Hask with: the cocartesian coproduct.
class Profunctor p => Choice p where
  -- | Laws:
  --
  -- @
  -- 'left'' ≡ 'dimap' swapE swapE '.' 'right'' where
  --   swapE :: 'Either' a b -> 'Either' b a
  --   swapE = 'either' 'Right' 'Left'
  -- 'rmap' 'Left' ≡ 'lmap' 'Left' '.' 'left''
  -- 'lmap' ('right' f) '.' 'left'' ≡ 'rmap' ('right' f) '.' 'left''
  -- 'left'' '.' 'left'' ≡ 'dimap' assocE unassocE '.' 'left'' where
  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
  --   assocE ('Left' ('Left' a)) = 'Left' a
  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
  --   assocE ('Right' c) = 'Right' ('Right' c)
  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
  --   unassocE ('Left' a) = 'Left' ('Left' a)
  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
  --   unassocE ('Right' ('Right' c)) = 'Right' c
  -- @
  left'  :: p a b -> p (Either a c) (Either b c)
  left' =  forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right'

  -- | Laws:
  --
  -- @
  -- 'right'' ≡ 'dimap' swapE swapE '.' 'left'' where
  --   swapE :: 'Either' a b -> 'Either' b a
  --   swapE = 'either' 'Right' 'Left'
  -- 'rmap' 'Right' ≡ 'lmap' 'Right' '.' 'right''
  -- 'lmap' ('left' f) '.' 'right'' ≡ 'rmap' ('left' f) '.' 'right''
  -- 'right'' '.' 'right'' ≡ 'dimap' unassocE assocE '.' 'right'' where
  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
  --   assocE ('Left' ('Left' a)) = 'Left' a
  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
  --   assocE ('Right' c) = 'Right' ('Right' c)
  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
  --   unassocE ('Left' a) = 'Left' ('Left' a)
  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
  --   unassocE ('Right' ('Right' c)) = 'Right' c
  -- @
  right' :: p a b -> p (Either c a) (Either c b)
  right' =  forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left'

  {-# MINIMAL left' | right' #-}

instance Choice (->) where
  left' :: forall a b c. (a -> b) -> Either a c -> Either b c
left' a -> b
ab (Left a
a) = forall a b. a -> Either a b
Left (a -> b
ab a
a)
  left' a -> b
_ (Right c
c) = forall a b. b -> Either a b
Right c
c
  {-# INLINE left' #-}
  right' :: forall a b c. (a -> b) -> Either c a -> Either c b
right' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
  {-# INLINE right' #-}

instance Monad m => Choice (Kleisli m) where
  left' :: forall a b c. Kleisli m a b -> Kleisli m (Either a c) (Either b c)
left' = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left
  {-# INLINE left' #-}
  right' :: forall a b c. Kleisli m a b -> Kleisli m (Either c a) (Either c b)
right' = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right
  {-# INLINE right' #-}

instance Applicative f => Choice (Star f) where
  left' :: forall a b c. Star f a b -> Star f (Either a c) (Either b c)
left' (Star a -> f b
f) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> f b
f) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right)
  {-# INLINE left' #-}
  right' :: forall a b c. Star f a b -> Star f (Either c a) (Either c b)
right' (Star a -> f b
f) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> f b
f)
  {-# INLINE right' #-}

-- | 'extract' approximates 'costrength'
instance Comonad w => Choice (Cokleisli w) where
  left' :: forall a b c.
Cokleisli w a b -> Cokleisli w (Either a c) (Either b c)
left' = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left
  {-# INLINE left' #-}
  right' :: forall a b c.
Cokleisli w a b -> Cokleisli w (Either c a) (Either c b)
right' = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right
  {-# INLINE right' #-}

instance Choice Tagged where
  left' :: forall a b c. Tagged a b -> Tagged (Either a c) (Either b c)
left' (Tagged b
b) = forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a b. a -> Either a b
Left b
b)
  {-# INLINE left' #-}
  right' :: forall a b c. Tagged a b -> Tagged (Either c a) (Either c b)
right' (Tagged b
b) = forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a b. b -> Either a b
Right b
b)
  {-# INLINE right' #-}

instance ArrowChoice p => Choice (WrappedArrow p) where
  left' :: forall a b c.
WrappedArrow p a b -> WrappedArrow p (Either a c) (Either b c)
left' (WrapArrow p a b
k) = forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
p a b -> WrappedArrow p a b
WrapArrow (forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left p a b
k)
  {-# INLINE left' #-}
  right' :: forall a b c.
WrappedArrow p a b -> WrappedArrow p (Either c a) (Either c b)
right' (WrapArrow p a b
k) = forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
p a b -> WrappedArrow p a b
WrapArrow (forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right p a b
k)
  {-# INLINE right' #-}

instance Monoid r => Choice (Forget r) where
  left' :: forall a b c. Forget r a b -> Forget r (Either a c) (Either b c)
left' (Forget a -> r
k) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> r
k (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty))
  {-# INLINE left' #-}
  right' :: forall a b c. Forget r a b -> Forget r (Either c a) (Either c b)
right' (Forget a -> r
k) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty) a -> r
k)
  {-# INLINE right' #-}

instance Functor f => Choice (Joker f) where
  left' :: forall a b c. Joker f a b -> Joker f (Either a c) (Either b c)
left' (Joker f b
fb) = forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left f b
fb)
  {-# INLINE left' #-}
  right' :: forall a b c. Joker f a b -> Joker f (Either c a) (Either c b)
right' (Joker f b
fb) = forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right f b
fb)
  {-# INLINE right' #-}

instance (Choice p, Choice q) => Choice (Product p q) where
  left' :: forall a b c.
Product p q a b -> Product p q (Either a c) (Either b c)
left' (Pair p a b
p q a b
q) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p a b
p) (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' q a b
q)
  {-# INLINE left' #-}
  right' :: forall a b c.
Product p q a b -> Product p q (Either c a) (Either c b)
right' (Pair p a b
p q a b
q) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' p a b
p) (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' q a b
q)
  {-# INLINE right' #-}

instance (Choice p, Choice q) => Choice (Sum p q) where
  left' :: forall a b c. Sum p q a b -> Sum p q (Either a c) (Either b c)
left' (L2 p a b
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p a b
p)
  left' (R2 q a b
q) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' q a b
q)
  {-# INLINE left' #-}
  right' :: forall a b c. Sum p q a b -> Sum p q (Either c a) (Either c b)
right' (L2 p a b
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' p a b
p)
  right' (R2 q a b
q) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' q a b
q)
  {-# INLINE right' #-}

instance (Functor f, Choice p) => Choice (Tannen f p) where
  left' :: forall a b c.
Tannen f p a b -> Tannen f p (Either a c) (Either b c)
left' (Tannen f (p a b)
fp) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' f (p a b)
fp)
  {-# INLINE left' #-}
  right' :: forall a b c.
Tannen f p a b -> Tannen f p (Either c a) (Either c b)
right' (Tannen f (p a b)
fp) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' f (p a b)
fp)
  {-# INLINE right' #-}

instance Choice p => Choice (Tambara p) where
  left' :: forall a b c. Tambara p a b -> Tambara p (Either a c) (Either b c)
left' (Tambara forall c. p (a, c) (b, c)
f) = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b c. (Either a b, c) -> Either (a, c) (b, c)
hither forall a c b. Either (a, c) (b, c) -> (Either a b, c)
yon forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' forall c. p (a, c) (b, c)
f where
    hither :: (Either a b, c) -> Either (a, c) (b, c)
    hither :: forall a b c. (Either a b, c) -> Either (a, c) (b, c)
hither (Left a
y, c
s) = forall a b. a -> Either a b
Left (a
y, c
s)
    hither (Right b
z, c
s) = forall a b. b -> Either a b
Right (b
z, c
s)

    yon :: Either (a, c) (b, c) -> (Either a b, c)
    yon :: forall a c b. Either (a, c) (b, c) -> (Either a b, c)
yon (Left (a
y, c
s)) = (forall a b. a -> Either a b
Left a
y, c
s)
    yon (Right (b
z, c
s)) = (forall a b. b -> Either a b
Right b
z, c
s)


----------------------------------------------------------------------------
-- * TambaraSum
----------------------------------------------------------------------------

-- | TambaraSum is cofreely adjoins strength with respect to Either.
--
-- Note: this is not dual to 'Data.Profunctor.Tambara.Tambara'. It is 'Data.Profunctor.Tambara.Tambara' with respect to a different tensor.
newtype TambaraSum p a b = TambaraSum { forall (p :: * -> * -> *) a b.
TambaraSum p a b -> forall c. p (Either a c) (Either b c)
runTambaraSum :: forall c. p (Either a c) (Either b c) }

instance ProfunctorFunctor TambaraSum where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> TambaraSum p :-> TambaraSum q
promap p :-> q
f (TambaraSum forall c. p (Either a c) (Either b c)
p) = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum (p :-> q
f forall c. p (Either a c) (Either b c)
p)

instance ProfunctorComonad TambaraSum where
  proextract :: forall (p :: * -> * -> *). Profunctor p => TambaraSum p :-> p
proextract (TambaraSum forall c. p (Either a c) (Either b c)
p)   = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. a -> Either a b
Left forall a. Either a a -> a
fromEither forall c. p (Either a c) (Either b c)
p
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
TambaraSum p :-> TambaraSum (TambaraSum p)
produplicate (TambaraSum forall c. p (Either a c) (Either b c)
p) = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum (forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b c. Either (Either a b) c -> Either a (Either b c)
hither forall a b c. Either a (Either b c) -> Either (Either a b) c
yon forall c. p (Either a c) (Either b c)
p) where
    hither :: Either (Either a b) c -> Either a (Either b c)
    hither :: forall a b c. Either (Either a b) c -> Either a (Either b c)
hither (Left (Left a
x))   = forall a b. a -> Either a b
Left a
x
    hither (Left (Right b
y))  = forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left b
y)
    hither (Right c
z)         = forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right c
z)

    yon    :: Either a (Either b c) -> Either (Either a b) c
    yon :: forall a b c. Either a (Either b c) -> Either (Either a b) c
yon    (Left a
x)          = forall a b. a -> Either a b
Left (forall a b. a -> Either a b
Left a
x)
    yon    (Right (Left b
y))  = forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right b
y)
    yon    (Right (Right c
z)) = forall a b. b -> Either a b
Right c
z

instance Profunctor p => Profunctor (TambaraSum p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> TambaraSum p b c -> TambaraSum p a d
dimap a -> b
f c -> d
g (TambaraSum forall c. p (Either b c) (Either c c)
p) = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left a -> b
f) (forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left c -> d
g) forall c. p (Either b c) (Either c c)
p
  {-# INLINE dimap #-}

instance Profunctor p => Choice (TambaraSum p) where
  left' :: forall a b c.
TambaraSum p a b -> TambaraSum p (Either a c) (Either b c)
left' TambaraSum p a b
p = forall (p :: * -> * -> *) a b.
TambaraSum p a b -> forall c. p (Either a c) (Either b c)
runTambaraSum forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> t (t p)
produplicate TambaraSum p a b
p
  {-# INLINE left' #-}

instance Category p => Category (TambaraSum p) where
  id :: forall a. TambaraSum p a a
id = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  TambaraSum forall c. p (Either b c) (Either c c)
p . :: forall b c a.
TambaraSum p b c -> TambaraSum p a b -> TambaraSum p a c
. TambaraSum forall c. p (Either a c) (Either b c)
q = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum (forall c. p (Either b c) (Either c c)
p forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall c. p (Either a c) (Either b c)
q)

instance Profunctor p => Functor (TambaraSum p a) where
  fmap :: forall a b. (a -> b) -> TambaraSum p a a -> TambaraSum p a b
fmap = forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap

-- |
-- @
-- 'tambaraSum' '.' 'untambaraSum' ≡ 'id'
-- 'untambaraSum' '.' 'tambaraSum' ≡ 'id'
-- @
tambaraSum :: Choice p => (p :-> q) -> p :-> TambaraSum q
tambaraSum :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Choice p =>
(p :-> q) -> p :-> TambaraSum q
tambaraSum p :-> q
f p a b
p = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum forall a b. (a -> b) -> a -> b
$ p :-> q
f forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p a b
p

-- |
-- @
-- 'tambaraSum' '.' 'untambaraSum' ≡ 'id'
-- 'untambaraSum' '.' 'tambaraSum' ≡ 'id'
-- @
untambaraSum :: Profunctor q => (p :-> TambaraSum q) -> p :-> q
untambaraSum :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Profunctor q =>
(p :-> TambaraSum q) -> p :-> q
untambaraSum p :-> TambaraSum q
f p a b
p = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. a -> Either a b
Left forall a. Either a a -> a
fromEither forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b.
TambaraSum p a b -> forall c. p (Either a c) (Either b c)
runTambaraSum forall a b. (a -> b) -> a -> b
$ p :-> TambaraSum q
f p a b
p

fromEither :: Either a a -> a
fromEither :: forall a. Either a a -> a
fromEither = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

----------------------------------------------------------------------------
-- * PastroSum
----------------------------------------------------------------------------

-- | PastroSum -| TambaraSum
--
-- PastroSum freely constructs strength with respect to Either.
data PastroSum p a b where
  PastroSum :: (Either y z -> b) -> p x y -> (a -> Either x z) -> PastroSum p a b

instance Functor (PastroSum p a) where
  fmap :: forall a b. (a -> b) -> PastroSum p a a -> PastroSum p a b
fmap a -> b
f (PastroSum Either y z -> a
l p x y
m a -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum (a -> b
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Either y z -> a
l) p x y
m a -> Either x z
r

instance Profunctor (PastroSum p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> PastroSum p b c -> PastroSum p a d
dimap a -> b
f c -> d
g (PastroSum Either y z -> c
l p x y
m b -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum (c -> d
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Either y z -> c
l) p x y
m (b -> Either x z
r forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)
  lmap :: forall a b c. (a -> b) -> PastroSum p b c -> PastroSum p a c
lmap a -> b
f (PastroSum Either y z -> c
l p x y
m b -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either y z -> c
l p x y
m (b -> Either x z
r forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)
  rmap :: forall b c a. (b -> c) -> PastroSum p a b -> PastroSum p a c
rmap b -> c
g (PastroSum Either y z -> b
l p x y
m a -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum (b -> c
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Either y z -> b
l) p x y
m a -> Either x z
r
  q b c
w #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> PastroSum p a b -> PastroSum p a c
#. PastroSum Either y z -> b
l p x y
m a -> Either x z
r = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum (q b c
w forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. Either y z -> b
l) p x y
m a -> Either x z
r
  PastroSum Either y z -> c
l p x y
m b -> Either x z
r .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
PastroSum p b c -> q a b -> PastroSum p a c
.# q a b
w = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either y z -> c
l p x y
m (b -> Either x z
r forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# q a b
w)

instance ProfunctorAdjunction PastroSum TambaraSum where
  counit :: forall (p :: * -> * -> *).
Profunctor p =>
PastroSum (TambaraSum p) :-> p
counit (PastroSum Either y z -> b
f (TambaraSum forall c. p (Either x c) (Either y c)
g) a -> Either x z
h) = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> Either x z
h Either y z -> b
f forall c. p (Either x c) (Either y c)
g
  unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> TambaraSum (PastroSum p)
unit p a b
p = forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum forall a b. (a -> b) -> a -> b
$ forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id p a b
p forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

instance ProfunctorFunctor PastroSum where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> PastroSum p :-> PastroSum q
promap p :-> q
f (PastroSum Either y z -> b
l p x y
m a -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either y z -> b
l (p :-> q
f p x y
m) a -> Either x z
r

instance ProfunctorMonad PastroSum where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> PastroSum p
proreturn p a b
p = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum forall a. Either a a -> a
fromEither p a b
p forall a b. a -> Either a b
Left
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
PastroSum (PastroSum p) :-> PastroSum p
projoin (PastroSum Either y z -> b
l (PastroSum Either y z -> y
m p x y
n x -> Either x z
o) a -> Either x z
q) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either y (Either z z) -> b
lm p x y
n a -> Either x (Either z z)
oq where
    oq :: a -> Either x (Either z z)
oq a
a = case a -> Either x z
q a
a of
      Left x
b -> forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x -> Either x z
o x
b
      Right z
z -> forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right z
z)
    lm :: Either y (Either z z) -> b
lm (Left y
x) = Either y z -> b
l forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Either y z -> y
m forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left y
x
    lm (Right (Left z
y)) = Either y z -> b
l forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Either y z -> y
m forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right z
y
    lm (Right (Right z
z)) = Either y z -> b
l forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right z
z

instance Choice (PastroSum p) where
  left' :: forall a b c.
PastroSum p a b -> PastroSum p (Either a c) (Either b c)
left' (PastroSum Either y z -> b
l p x y
m a -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either y (Either z c) -> Either b c
l' p x y
m Either a c -> Either x (Either z c)
r' where
    r' :: Either a c -> Either x (Either z c)
r' = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either x z
r) (forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right)
    l' :: Either y (Either z c) -> Either b c
l' (Left y
y)          = forall a b. a -> Either a b
Left (Either y z -> b
l (forall a b. a -> Either a b
Left y
y))
    l' (Right (Left z
z))  = forall a b. a -> Either a b
Left (Either y z -> b
l (forall a b. b -> Either a b
Right z
z))
    l' (Right (Right c
c)) = forall a b. b -> Either a b
Right c
c
  right' :: forall a b c.
PastroSum p a b -> PastroSum p (Either c a) (Either c b)
right' (PastroSum Either y z -> b
l p x y
m a -> Either x z
r) = forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either y (Either c z) -> Either c b
l' p x y
m Either c a -> Either x (Either c z)
r' where
    r' :: Either c a -> Either x (Either c z)
r' = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either x z
r)
    l' :: Either y (Either c z) -> Either c b
l' (Right (Left c
c))  = forall a b. a -> Either a b
Left c
c
    l' (Right (Right z
z)) = forall a b. b -> Either a b
Right (Either y z -> b
l (forall a b. b -> Either a b
Right z
z))
    l' (Left y
y)          = forall a b. b -> Either a b
Right (Either y z -> b
l (forall a b. a -> Either a b
Left y
y))

--------------------------------------------------------------------------------
-- * Costrength for Either
--------------------------------------------------------------------------------

class Profunctor p => Cochoice p where
  -- | Laws:
  --
  -- @
  -- 'unleft' ≡ 'unright' '.' 'dimap' swapE swapE where
  --   swapE :: 'Either' a b -> 'Either' b a
  --   swapE = 'either' 'Right' 'Left'
  -- 'rmap' ('either' 'id' 'absurd') ≡ 'unleft' '.' 'lmap' ('either' 'id' 'absurd')
  -- 'unfirst' '.' 'rmap' ('second' f) ≡ 'unfirst' '.' 'lmap' ('second' f)
  -- 'unleft' '.' 'unleft' ≡ 'unleft' '.' 'dimap' assocE unassocE where
  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
  --   assocE ('Left' ('Left' a)) = 'Left' a
  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
  --   assocE ('Right' c) = 'Right' ('Right' c)
  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
  --   unassocE ('Left' a) = 'Left' ('Left' a)
  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
  --   unassocE ('Right' ('Right' c)) = 'Right' c
  -- @
  unleft  :: p (Either a d) (Either b d) -> p a b
  unleft = forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left)

  -- | Laws:
  --
  -- @
  -- 'unright' ≡ 'unleft' '.' 'dimap' swapE swapE where
  --   swapE :: 'Either' a b -> 'Either' b a
  --   swapE = 'either' 'Right' 'Left'
  -- 'rmap' ('either' 'absurd' 'id') ≡ 'unright' '.' 'lmap' ('either' 'absurd' 'id')
  -- 'unsecond' '.' 'rmap' ('first' f) ≡ 'unsecond' '.' 'lmap' ('first' f)
  -- 'unright' '.' 'unright' ≡ 'unright' '.' 'dimap' unassocE assocE where
  --   assocE :: 'Either' ('Either' a b) c -> 'Either' a ('Either' b c)
  --   assocE ('Left' ('Left' a)) = 'Left' a
  --   assocE ('Left' ('Right' b)) = 'Right' ('Left' b)
  --   assocE ('Right' c) = 'Right' ('Right' c)
  --   unassocE :: 'Either' a ('Either' b c) -> 'Either' ('Either' a b) c
  --   unassocE ('Left' a) = 'Left' ('Left' a)
  --   unassocE ('Right' ('Left' b)) = 'Left' ('Right' b)
  --   unassocE ('Right' ('Right' c)) = 'Right' c
  -- @
  unright :: p (Either d a) (Either d b) -> p a b
  unright = forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left)

  {-# MINIMAL unleft | unright #-}

instance Cochoice (->) where
  unleft :: forall a d b. (Either a d -> Either b d) -> a -> b
unleft Either a d -> Either b d
f = Either a d -> b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left where go :: Either a d -> b
go = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Either a d -> b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Either a d -> Either b d
f
  unright :: forall d a b. (Either d a -> Either d b) -> a -> b
unright Either d a -> Either d b
f = Either d a -> b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right where go :: Either d a -> b
go = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either d a -> b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left) forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Either d a -> Either d b
f

instance Applicative f => Cochoice (Costar f) where
  unleft :: forall a d b. Costar f (Either a d) (Either b d) -> Costar f a b
unleft (Costar f (Either a d) -> Either b d
f) = forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar (f (Either a d) -> b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left)
    where go :: f (Either a d) -> b
go = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (f (Either a d) -> b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f (Either a d) -> Either b d
f

-- NB: Another instance that's highly questionable
instance Traversable f => Cochoice (Star f) where
  unright :: forall d a b. Star f (Either d a) (Either d b) -> Star f a b
unright (Star Either d a -> f (Either d b)
f) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (Either d a -> f b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right)
    where go :: Either d a -> f b
go = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either d a -> f b
go forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left) forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Either d a -> f (Either d b)
f

instance (Functor f, Cochoice p) => Cochoice (Tannen f p) where
  unleft :: forall a d b.
Tannen f p (Either a d) (Either b d) -> Tannen f p a b
unleft (Tannen f (p (Either a d) (Either b d))
fp) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft f (p (Either a d) (Either b d))
fp)
  {-# INLINE unleft #-}
  unright :: forall d a b.
Tannen f p (Either d a) (Either d b) -> Tannen f p a b
unright (Tannen f (p (Either d a) (Either d b))
fp) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright f (p (Either d a) (Either d b))
fp)
  {-# INLINE unright #-}

instance (Cochoice p, Cochoice q) => Cochoice (Product p q) where
  unleft :: forall a d b.
Product p q (Either a d) (Either b d) -> Product p q a b
unleft (Pair p (Either a d) (Either b d)
p q (Either a d) (Either b d)
q) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft p (Either a d) (Either b d)
p) (forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft q (Either a d) (Either b d)
q)
  unright :: forall d a b.
Product p q (Either d a) (Either d b) -> Product p q a b
unright (Pair p (Either d a) (Either d b)
p q (Either d a) (Either d b)
q) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright p (Either d a) (Either d b)
p) (forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright q (Either d a) (Either d b)
q)

instance (Cochoice p, Cochoice q) => Cochoice (Sum p q) where
  unleft :: forall a d b. Sum p q (Either a d) (Either b d) -> Sum p q a b
unleft (L2 p (Either a d) (Either b d)
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft p (Either a d) (Either b d)
p)
  unleft (R2 q (Either a d) (Either b d)
q) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft q (Either a d) (Either b d)
q)
  unright :: forall d a b. Sum p q (Either d a) (Either d b) -> Sum p q a b
unright (L2 p (Either d a) (Either d b)
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright p (Either d a) (Either d b)
p)
  unright (R2 q (Either d a) (Either d b)
q) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright q (Either d a) (Either d b)
q)

instance Cochoice (Forget r) where
  unleft :: forall a d b. Forget r (Either a d) (Either b d) -> Forget r a b
unleft (Forget Either a d -> r
f) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (Either a d -> r
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. a -> Either a b
Left)
  unright :: forall d a b. Forget r (Either d a) (Either d b) -> Forget r a b
unright (Forget Either d a -> r
f) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (Either d a -> r
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. b -> Either a b
Right)

----------------------------------------------------------------------------
-- * CotambaraSum
----------------------------------------------------------------------------

-- | 'CotambaraSum' cofreely constructs costrength with respect to 'Either' (aka 'Choice')
data CotambaraSum q a b where
    CotambaraSum :: Cochoice r => (r :-> q) -> r a b -> CotambaraSum q a b

instance Profunctor (CotambaraSum p) where
  lmap :: forall a b c. (a -> b) -> CotambaraSum p b c -> CotambaraSum p a c
lmap a -> b
f (CotambaraSum r :-> p
n r b c
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r :-> p
n (forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f r b c
p)
  rmap :: forall b c a. (b -> c) -> CotambaraSum p a b -> CotambaraSum p a c
rmap b -> c
g (CotambaraSum r :-> p
n r a b
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r :-> p
n (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
g r a b
p)
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> CotambaraSum p b c -> CotambaraSum p a d
dimap a -> b
f c -> d
g (CotambaraSum r :-> p
n r b c
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r :-> p
n (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> b
f c -> d
g r b c
p)

instance ProfunctorFunctor CotambaraSum where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> CotambaraSum p :-> CotambaraSum q
promap p :-> q
f (CotambaraSum r :-> p
n r a b
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum (p :-> q
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. r :-> p
n) r a b
p

instance ProfunctorComonad CotambaraSum where
  proextract :: forall (p :: * -> * -> *). Profunctor p => CotambaraSum p :-> p
proextract (CotambaraSum r :-> p
n r a b
p)  = r :-> p
n r a b
p
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
CotambaraSum p :-> CotambaraSum (CotambaraSum p)
produplicate (CotambaraSum r :-> p
n r a b
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r :-> p
n r a b
p)

instance Cochoice (CotambaraSum p) where
  unleft :: forall a d b.
CotambaraSum p (Either a d) (Either b d) -> CotambaraSum p a b
unleft (CotambaraSum r :-> p
n r (Either a d) (Either b d)
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r :-> p
n (forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft r (Either a d) (Either b d)
p)
  unright :: forall d a b.
CotambaraSum p (Either d a) (Either d b) -> CotambaraSum p a b
unright (CotambaraSum r :-> p
n r (Either d a) (Either d b)
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r :-> p
n (forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright r (Either d a) (Either d b)
p)

instance Functor (CotambaraSum p a) where
  fmap :: forall a b. (a -> b) -> CotambaraSum p a a -> CotambaraSum p a b
fmap = forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap

-- |
-- @
-- 'cotambaraSum' '.' 'uncotambaraSum' ≡ 'id'
-- 'uncotambaraSum' '.' 'cotambaraSum' ≡ 'id'
-- @
cotambaraSum :: Cochoice p => (p :-> q) -> p :-> CotambaraSum q
cotambaraSum :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Cochoice p =>
(p :-> q) -> p :-> CotambaraSum q
cotambaraSum p :-> q
f = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum p :-> q
f

-- |
-- @
-- 'cotambaraSum' '.' 'uncotambaraSum' ≡ 'id'
-- 'uncotambaraSum' '.' 'cotambaraSum' ≡ 'id'
-- @
uncotambaraSum :: Profunctor q => (p :-> CotambaraSum q) -> p :-> q
uncotambaraSum :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Profunctor q =>
(p :-> CotambaraSum q) -> p :-> q
uncotambaraSum p :-> CotambaraSum q
f p a b
p = forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract (p :-> CotambaraSum q
f p a b
p)

----------------------------------------------------------------------------
-- * Copastro
----------------------------------------------------------------------------

-- | CopastroSum -| CotambaraSum
--
-- 'CopastroSum' freely constructs costrength with respect to 'Either' (aka 'Choice')
newtype CopastroSum p a b = CopastroSum { forall (p :: * -> * -> *) a b.
CopastroSum p a b
-> forall (r :: * -> * -> *).
   Cochoice r =>
   (forall x y. p x y -> r x y) -> r a b
runCopastroSum :: forall r. Cochoice r => (forall x y. p x y -> r x y) -> r a b }

instance Functor (CopastroSum p a) where
  fmap :: forall a b. (a -> b) -> CopastroSum p a a -> CopastroSum p a b
fmap a -> b
f (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a a
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
f (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a a
h forall x y. p x y -> r x y
n)

instance Profunctor (CopastroSum p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> CopastroSum p b c -> CopastroSum p a d
dimap a -> b
f c -> d
g (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r b c
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> b
f c -> d
g (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r b c
h forall x y. p x y -> r x y
n)
  lmap :: forall a b c. (a -> b) -> CopastroSum p b c -> CopastroSum p a c
lmap a -> b
f (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r b c
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r b c
h forall x y. p x y -> r x y
n)
  rmap :: forall b c a. (b -> c) -> CopastroSum p a b -> CopastroSum p a c
rmap b -> c
g (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a b
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
g (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a b
h forall x y. p x y -> r x y
n)

instance ProfunctorAdjunction CopastroSum CotambaraSum where
 unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> CotambaraSum (CopastroSum p)
unit p a b
p = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn p a b
p)
 counit :: forall (p :: * -> * -> *).
Profunctor p =>
CopastroSum (CotambaraSum p) :-> p
counit (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. CotambaraSum p x y -> r x y) -> r a b
h) = forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. CotambaraSum p x y -> r x y) -> r a b
h forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

instance ProfunctorFunctor CopastroSum where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> CopastroSum p :-> CopastroSum q
promap p :-> q
f (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a b
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \forall x y. q x y -> r x y
n -> forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a b
h (forall x y. q x y -> r x y
n forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p :-> q
f)

instance ProfunctorMonad CopastroSum where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> CopastroSum p
proreturn p a b
p = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> forall x y. p x y -> r x y
n p a b
p
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
CopastroSum (CopastroSum p) :-> CopastroSum p
projoin CopastroSum (CopastroSum p) a b
p = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
c -> forall (p :: * -> * -> *) a b.
CopastroSum p a b
-> forall (r :: * -> * -> *).
   Cochoice r =>
   (forall x y. p x y -> r x y) -> r a b
runCopastroSum CopastroSum (CopastroSum p) a b
p (\CopastroSum p x y
x -> forall (p :: * -> * -> *) a b.
CopastroSum p a b
-> forall (r :: * -> * -> *).
   Cochoice r =>
   (forall x y. p x y -> r x y) -> r a b
runCopastroSum CopastroSum p x y
x forall x y. p x y -> r x y
c)

instance Cochoice (CopastroSum p) where
  unleft :: forall a d b.
CopastroSum p (Either a d) (Either b d) -> CopastroSum p a b
unleft (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r (Either a d) (Either b d)
p) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r (Either a d) (Either b d)
p forall x y. p x y -> r x y
n)
  unright :: forall d a b.
CopastroSum p (Either d a) (Either d b) -> CopastroSum p a b
unright (CopastroSum forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r (Either d a) (Either d b)
p) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
CopastroSum forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright (forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r (Either d a) (Either d b)
p forall x y. p x y -> r x y
n)