{-# 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' =  (Either a c -> Either c a)
-> (Either c b -> Either b c)
-> p (Either c a) (Either c b)
-> p (Either a c) (Either b c)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a -> Either c a) -> (c -> Either c a) -> Either a c -> Either c a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either c a
forall a b. b -> Either a b
Right c -> Either c a
forall a b. a -> Either a b
Left) ((c -> Either b c) -> (b -> Either b c) -> Either c b -> Either b c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either c -> Either b c
forall a b. b -> Either a b
Right b -> Either b c
forall a b. a -> Either a b
Left) (p (Either c a) (Either c b) -> p (Either a c) (Either b c))
-> (p a b -> p (Either c a) (Either c b))
-> p a b
-> p (Either a c) (Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p a b -> p (Either c a) (Either c b)
forall a b c. p a b -> p (Either c a) (Either c b)
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' =  (Either c a -> Either a c)
-> (Either b c -> Either c b)
-> p (Either a c) (Either b c)
-> p (Either c a) (Either c b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((c -> Either a c) -> (a -> Either a c) -> Either c a -> Either a c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either c -> Either a c
forall a b. b -> Either a b
Right a -> Either a c
forall a b. a -> Either a b
Left) ((b -> Either c b) -> (c -> Either c b) -> Either b c -> Either c b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> Either c b
forall a b. b -> Either a b
Right c -> Either c b
forall a b. a -> Either a b
Left) (p (Either a c) (Either b c) -> p (Either c a) (Either c b))
-> (p a b -> p (Either a c) (Either b c))
-> p a b
-> p (Either c a) (Either c b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p a b -> p (Either a c) (Either b c)
forall a b c. p a b -> p (Either a c) (Either b 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) = b -> Either b c
forall a b. a -> Either a b
Left (a -> b
ab a
a)
  left' a -> b
_ (Right c
c) = c -> Either b 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' = (a -> b) -> Either c a -> Either c b
forall a b. (a -> b) -> Either c a -> Either c b
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' = Kleisli m a b -> Kleisli m (Either a c) (Either b c)
forall a b c. Kleisli m a b -> Kleisli m (Either a c) (Either b c)
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' = Kleisli m a b -> Kleisli m (Either c a) (Either c b)
forall a b c. Kleisli m a b -> Kleisli m (Either c a) (Either c b)
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) = (Either a c -> f (Either b c)) -> Star f (Either a c) (Either b c)
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((Either a c -> f (Either b c))
 -> Star f (Either a c) (Either b c))
-> (Either a c -> f (Either b c))
-> Star f (Either a c) (Either b c)
forall a b. (a -> b) -> a -> b
$ (a -> f (Either b c))
-> (c -> f (Either b c)) -> Either a c -> f (Either b c)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((b -> Either b c) -> f b -> f (Either b c)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either b c
forall a b. a -> Either a b
Left (f b -> f (Either b c)) -> (a -> f b) -> a -> f (Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) (Either b c -> f (Either b c)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either b c -> f (Either b c))
-> (c -> Either b c) -> c -> f (Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c -> Either b 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) = (Either c a -> f (Either c b)) -> Star f (Either c a) (Either c b)
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((Either c a -> f (Either c b))
 -> Star f (Either c a) (Either c b))
-> (Either c a -> f (Either c b))
-> Star f (Either c a) (Either c b)
forall a b. (a -> b) -> a -> b
$ (c -> f (Either c b))
-> (a -> f (Either c b)) -> Either c a -> f (Either c b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either c b -> f (Either c b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either c b -> f (Either c b))
-> (c -> Either c b) -> c -> f (Either c b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c -> Either c b
forall a b. a -> Either a b
Left) ((b -> Either c b) -> f b -> f (Either c b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either c b
forall a b. b -> Either a b
Right (f b -> f (Either c b)) -> (a -> f b) -> a -> f (Either c b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
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' = Cokleisli w a b -> Cokleisli w (Either a c) (Either b c)
forall a b c.
Cokleisli w a b -> Cokleisli w (Either a c) (Either b c)
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' = Cokleisli w a b -> Cokleisli w (Either c a) (Either c b)
forall a b c.
Cokleisli w a b -> Cokleisli w (Either c a) (Either c b)
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) = Either b c -> Tagged (Either a c) (Either b c)
forall {k} (s :: k) b. b -> Tagged s b
Tagged (b -> Either b c
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) = Either c b -> Tagged (Either c a) (Either c b)
forall {k} (s :: k) b. b -> Tagged s b
Tagged (b -> Either c b
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) = p (Either a c) (Either b c)
-> WrappedArrow p (Either a c) (Either b c)
forall {k} {k1} (p :: k -> k1 -> *) (a :: k) (b :: k1).
p a b -> WrappedArrow p a b
WrapArrow (p a b -> p (Either a c) (Either b c)
forall b c d. p b c -> p (Either b d) (Either c d)
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) = p (Either c a) (Either c b)
-> WrappedArrow p (Either c a) (Either c b)
forall {k} {k1} (p :: k -> k1 -> *) (a :: k) (b :: k1).
p a b -> WrappedArrow p a b
WrapArrow (p a b -> p (Either c a) (Either c b)
forall b c d. p b c -> p (Either d b) (Either d c)
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) = (Either a c -> r) -> Forget r (Either a c) (Either b c)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget ((a -> r) -> (c -> r) -> Either a c -> r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> r
k (r -> c -> r
forall a b. a -> b -> a
const r
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) = (Either c a -> r) -> Forget r (Either c a) (Either c b)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget ((c -> r) -> (a -> r) -> Either c a -> r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (r -> c -> r
forall a b. a -> b -> a
const r
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) = f (Either b c) -> Joker f (Either a c) (Either b c)
forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker ((b -> Either b c) -> f b -> f (Either b c)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either b c
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) = f (Either c b) -> Joker f (Either c a) (Either c b)
forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker ((b -> Either c b) -> f b -> f (Either c b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either c b
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) = p (Either a c) (Either b c)
-> q (Either a c) (Either b c)
-> Product p q (Either a c) (Either b c)
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 (p a b -> p (Either a c) (Either b c)
forall a b c. p a b -> p (Either a c) (Either b c)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p a b
p) (q a b -> q (Either a c) (Either b c)
forall a b c. q a b -> q (Either a c) (Either b c)
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) = p (Either c a) (Either c b)
-> q (Either c a) (Either c b)
-> Product p q (Either c a) (Either c b)
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 (p a b -> p (Either c a) (Either c b)
forall a b c. p a b -> p (Either c a) (Either c b)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' p a b
p) (q a b -> q (Either c a) (Either c b)
forall a b c. q a b -> q (Either c a) (Either c b)
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) = p (Either a c) (Either b c) -> Sum p q (Either a c) (Either b c)
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (p a b -> p (Either a c) (Either b c)
forall a b c. p a b -> p (Either a c) (Either b c)
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) = q (Either a c) (Either b c) -> Sum p q (Either a c) (Either b c)
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (q a b -> q (Either a c) (Either b c)
forall a b c. q a b -> q (Either a c) (Either b c)
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) = p (Either c a) (Either c b) -> Sum p q (Either c a) (Either c b)
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (p a b -> p (Either c a) (Either c b)
forall a b c. p a b -> p (Either c a) (Either c b)
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) = q (Either c a) (Either c b) -> Sum p q (Either c a) (Either c b)
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (q a b -> q (Either c a) (Either c b)
forall a b c. q a b -> q (Either c a) (Either c b)
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) = f (p (Either a c) (Either b c))
-> Tannen f p (Either a c) (Either b c)
forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen ((p a b -> p (Either a c) (Either b c))
-> f (p a b) -> f (p (Either a c) (Either b c))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p a b -> p (Either a c) (Either b c)
forall a b c. p a b -> p (Either a c) (Either b c)
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) = f (p (Either c a) (Either c b))
-> Tannen f p (Either c a) (Either c b)
forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen ((p a b -> p (Either c a) (Either c b))
-> f (p a b) -> f (p (Either c a) (Either c b))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p a b -> p (Either c a) (Either c b)
forall a b c. p a b -> p (Either c a) (Either c b)
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 c. p (Either a c, c) (Either b c, c))
-> Tambara p (Either a c) (Either b c)
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. p (Either a c, c) (Either b c, c))
 -> Tambara p (Either a c) (Either b c))
-> (forall c. p (Either a c, c) (Either b c, c))
-> Tambara p (Either a c) (Either b c)
forall a b. (a -> b) -> a -> b
$ ((Either a c, c) -> Either (a, c) (c, c))
-> (Either (b, c) (c, c) -> (Either b c, c))
-> p (Either (a, c) (c, c)) (Either (b, c) (c, c))
-> p (Either a c, c) (Either b c, c)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Either a c, c) -> Either (a, c) (c, c)
forall a b c. (Either a b, c) -> Either (a, c) (b, c)
hither Either (b, c) (c, c) -> (Either b c, c)
forall a c b. Either (a, c) (b, c) -> (Either a b, c)
yon (p (Either (a, c) (c, c)) (Either (b, c) (c, c))
 -> p (Either a c, c) (Either b c, c))
-> p (Either (a, c) (c, c)) (Either (b, c) (c, c))
-> p (Either a c, c) (Either b c, c)
forall a b. (a -> b) -> a -> b
$ p (a, c) (b, c) -> p (Either (a, c) (c, c)) (Either (b, c) (c, c))
forall a b c. p a b -> p (Either a c) (Either b c)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p (a, c) (b, c)
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) = (a, c) -> Either (a, c) (b, c)
forall a b. a -> Either a b
Left (a
y, c
s)
    hither (Right b
z, c
s) = (b, c) -> Either (a, c) (b, c)
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)) = (a -> Either a b
forall a b. a -> Either a b
Left a
y, c
s)
    yon (Right (b
z, c
s)) = (b -> Either a b
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 c. q (Either a c) (Either b c)) -> TambaraSum q a b
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum (p (Either a c) (Either b c) -> q (Either a c) (Either b c)
p :-> q
f p (Either a c) (Either b c)
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)   = (a -> Either a b)
-> (Either b b -> b) -> p (Either a b) (Either b b) -> p a b
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> Either a b
forall a b. a -> Either a b
Left Either b b -> b
forall a. Either a a -> a
fromEither p (Either a b) (Either b b)
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 c. TambaraSum p (Either a c) (Either b c))
-> TambaraSum (TambaraSum p) a b
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum ((forall c. p (Either (Either a c) c) (Either (Either b c) c))
-> TambaraSum p (Either a c) (Either b c)
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum ((forall c. p (Either (Either a c) c) (Either (Either b c) c))
 -> TambaraSum p (Either a c) (Either b c))
-> (forall c. p (Either (Either a c) c) (Either (Either b c) c))
-> TambaraSum p (Either a c) (Either b c)
forall a b. (a -> b) -> a -> b
$ (Either (Either a c) c -> Either a (Either c c))
-> (Either b (Either c c) -> Either (Either b c) c)
-> p (Either a (Either c c)) (Either b (Either c c))
-> p (Either (Either a c) c) (Either (Either b c) c)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Either (Either a c) c -> Either a (Either c c)
forall a b c. Either (Either a b) c -> Either a (Either b c)
hither Either b (Either c c) -> Either (Either b c) c
forall a b c. Either a (Either b c) -> Either (Either a b) c
yon p (Either a (Either c c)) (Either b (Either c c))
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))   = a -> Either a (Either b c)
forall a b. a -> Either a b
Left a
x
    hither (Left (Right b
y))  = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (b -> Either b c
forall a b. a -> Either a b
Left b
y)
    hither (Right c
z)         = Either b c -> Either a (Either b c)
forall a b. b -> Either a b
Right (c -> Either b c
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)          = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (a -> Either a b
forall a b. a -> Either a b
Left a
x)
    yon    (Right (Left b
y))  = Either a b -> Either (Either a b) c
forall a b. a -> Either a b
Left (b -> Either a b
forall a b. b -> Either a b
Right b
y)
    yon    (Right (Right c
z)) = c -> Either (Either a b) c
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 c. p (Either a c) (Either d c)) -> TambaraSum p a d
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum ((forall c. p (Either a c) (Either d c)) -> TambaraSum p a d)
-> (forall c. p (Either a c) (Either d c)) -> TambaraSum p a d
forall a b. (a -> b) -> a -> b
$ (Either a c -> Either b c)
-> (Either c c -> Either d c)
-> p (Either b c) (Either c c)
-> p (Either a c) (Either d c)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a -> b) -> Either a c -> Either b c
forall a b c. (a -> b) -> Either a c -> Either b c
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left a -> b
f) ((c -> d) -> Either c c -> Either d c
forall a b c. (a -> b) -> Either a c -> Either b c
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left c -> d
g) p (Either b c) (Either c c)
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 = TambaraSum (TambaraSum p) a b
-> forall c. TambaraSum p (Either a c) (Either b c)
forall (p :: * -> * -> *) a b.
TambaraSum p a b -> forall c. p (Either a c) (Either b c)
runTambaraSum (TambaraSum (TambaraSum p) a b
 -> forall c. TambaraSum p (Either a c) (Either b c))
-> TambaraSum (TambaraSum p) a b
-> forall c. TambaraSum p (Either a c) (Either b c)
forall a b. (a -> b) -> a -> b
$ TambaraSum p a b -> TambaraSum (TambaraSum p) a b
TambaraSum p :-> TambaraSum (TambaraSum p)
forall (p :: * -> * -> *).
Profunctor p =>
TambaraSum p :-> TambaraSum (TambaraSum p)
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 c. p (Either a c) (Either a c)) -> TambaraSum p a a
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum p (Either a c) (Either a c)
forall a. p a a
forall c. p (Either a c) (Either a c)
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 c. p (Either a c) (Either c c)) -> TambaraSum p a c
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum (p (Either b c) (Either c c)
forall c. p (Either b c) (Either c c)
p p (Either b c) (Either c c)
-> p (Either a c) (Either b c) -> p (Either a c) (Either c c)
forall b c a. p b c -> p a b -> p a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p (Either a c) (Either b 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 = (a -> b) -> TambaraSum p a a -> TambaraSum p a b
forall b c a. (b -> c) -> TambaraSum p a b -> TambaraSum p a c
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 c. q (Either a c) (Either b c)) -> TambaraSum q a b
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum ((forall c. q (Either a c) (Either b c)) -> TambaraSum q a b)
-> (forall c. q (Either a c) (Either b c)) -> TambaraSum q a b
forall a b. (a -> b) -> a -> b
$ p (Either a c) (Either b c) -> q (Either a c) (Either b c)
p :-> q
f (p (Either a c) (Either b c) -> q (Either a c) (Either b c))
-> p (Either a c) (Either b c) -> q (Either a c) (Either b c)
forall a b. (a -> b) -> a -> b
$ p a b -> p (Either a c) (Either b c)
forall a b c. p a b -> p (Either a c) (Either b c)
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 = (a -> Either a b)
-> (Either b b -> b) -> q (Either a b) (Either b b) -> q a b
forall a b c d. (a -> b) -> (c -> d) -> q b c -> q a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> Either a b
forall a b. a -> Either a b
Left Either b b -> b
forall a. Either a a -> a
fromEither (q (Either a b) (Either b b) -> q a b)
-> q (Either a b) (Either b b) -> q a b
forall a b. (a -> b) -> a -> b
$ TambaraSum q a b -> forall c. q (Either a c) (Either b c)
forall (p :: * -> * -> *) a b.
TambaraSum p a b -> forall c. p (Either a c) (Either b c)
runTambaraSum (TambaraSum q a b -> forall c. q (Either a c) (Either b c))
-> TambaraSum q a b -> forall c. q (Either a c) (Either b c)
forall a b. (a -> b) -> a -> b
$ p a b -> TambaraSum q a b
p :-> TambaraSum q
f p a b
p

fromEither :: Either a a -> a
fromEither :: forall a. Either a a -> a
fromEither = (a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id a -> a
forall a. a -> a
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) = (Either y z -> b) -> p x y -> (a -> Either x z) -> PastroSum p 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 (a -> b
f (a -> b) -> (Either y z -> a) -> Either y z -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) = (Either y z -> d) -> p x y -> (a -> Either x z) -> PastroSum p a d
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 (c -> d) -> (Either y z -> c) -> Either y z -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 (b -> Either x z) -> (a -> b) -> a -> Either x z
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) = (Either y z -> c) -> p x y -> (a -> Either x z) -> PastroSum p a c
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 (b -> Either x z) -> (a -> b) -> a -> Either x z
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) = (Either y z -> c) -> p x y -> (a -> Either x z) -> PastroSum p a c
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 (b -> c) -> (Either y z -> b) -> Either y z -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 = (Either y z -> c) -> p x y -> (a -> Either x z) -> PastroSum p a c
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 q b c -> (Either y z -> b) -> Either y z -> c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> (a -> b) -> a -> c
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 = (Either y z -> c) -> p x y -> (a -> Either x z) -> PastroSum p a c
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 (b -> Either x z) -> q a b -> a -> Either x z
forall a b c (q :: * -> * -> *).
Coercible b a =>
(b -> c) -> q a b -> a -> c
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) = (a -> Either x z)
-> (Either y z -> b) -> p (Either x z) (Either y z) -> p a b
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
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 p (Either x z) (Either y z)
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 c. PastroSum p (Either a c) (Either b c))
-> TambaraSum (PastroSum p) a b
forall (p :: * -> * -> *) a b.
(forall c. p (Either a c) (Either b c)) -> TambaraSum p a b
TambaraSum ((forall c. PastroSum p (Either a c) (Either b c))
 -> TambaraSum (PastroSum p) a b)
-> (forall c. PastroSum p (Either a c) (Either b c))
-> TambaraSum (PastroSum p) a b
forall a b. (a -> b) -> a -> b
$ (Either b c -> Either b c)
-> p a b
-> (Either a c -> Either a c)
-> PastroSum p (Either a c) (Either b c)
forall r z b (p :: * -> * -> *) x a.
(Either r z -> b) -> p x r -> (a -> Either x z) -> PastroSum p a b
PastroSum Either b c -> Either b c
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id p a b
p Either a c -> Either a c
forall a. a -> a
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) = (Either y z -> b) -> q x y -> (a -> Either x z) -> PastroSum q 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 Either y z -> b
l (p x y -> q x y
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 = (Either b b -> b) -> p a b -> (a -> Either a b) -> PastroSum p 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 Either b b -> b
forall a. Either a a -> a
fromEither p a b
p a -> Either a b
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) = (Either y (Either z z) -> b)
-> p x y -> (a -> Either x (Either z z)) -> PastroSum p 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 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 -> z -> Either z z
forall a b. a -> Either a b
Left (z -> Either z z) -> Either x z -> Either x (Either z z)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x -> Either x z
o x
b
      Right z
z -> Either z z -> Either x (Either z z)
forall a b. b -> Either a b
Right (z -> Either z z
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 (Either y z -> b) -> Either y z -> b
forall a b. (a -> b) -> a -> b
$ y -> Either y z
forall a b. a -> Either a b
Left (y -> Either y z) -> y -> Either y z
forall a b. (a -> b) -> a -> b
$ Either y z -> y
m (Either y z -> y) -> Either y z -> y
forall a b. (a -> b) -> a -> b
$ y -> Either y z
forall a b. a -> Either a b
Left y
x
    lm (Right (Left z
y)) = Either y z -> b
l (Either y z -> b) -> Either y z -> b
forall a b. (a -> b) -> a -> b
$ y -> Either y z
forall a b. a -> Either a b
Left (y -> Either y z) -> y -> Either y z
forall a b. (a -> b) -> a -> b
$ Either y z -> y
m (Either y z -> y) -> Either y z -> y
forall a b. (a -> b) -> a -> b
$ z -> Either y z
forall a b. b -> Either a b
Right z
y
    lm (Right (Right z
z)) = Either y z -> b
l (Either y z -> b) -> Either y z -> b
forall a b. (a -> b) -> a -> b
$ z -> Either y z
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) = (Either y (Either z c) -> Either b c)
-> p x y
-> (Either a c -> Either x (Either z c))
-> PastroSum p (Either a c) (Either b c)
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' = (a -> Either x (Either z c))
-> (c -> Either x (Either z c))
-> Either a c
-> Either x (Either z c)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((z -> Either z c) -> Either x z -> Either x (Either z c)
forall a b. (a -> b) -> Either x a -> Either x b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap z -> Either z c
forall a b. a -> Either a b
Left (Either x z -> Either x (Either z c))
-> (a -> Either x z) -> a -> Either x (Either z c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) (Either z c -> Either x (Either z c)
forall a b. b -> Either a b
Right (Either z c -> Either x (Either z c))
-> (c -> Either z c) -> c -> Either x (Either z c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c -> Either z c
forall a b. b -> Either a b
Right)
    l' :: Either y (Either z c) -> Either b c
l' (Left y
y)          = b -> Either b c
forall a b. a -> Either a b
Left (Either y z -> b
l (y -> Either y z
forall a b. a -> Either a b
Left y
y))
    l' (Right (Left z
z))  = b -> Either b c
forall a b. a -> Either a b
Left (Either y z -> b
l (z -> Either y z
forall a b. b -> Either a b
Right z
z))
    l' (Right (Right c
c)) = c -> Either b 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) = (Either y (Either c z) -> Either c b)
-> p x y
-> (Either c a -> Either x (Either c z))
-> PastroSum p (Either c a) (Either c b)
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' = (c -> Either x (Either c z))
-> (a -> Either x (Either c z))
-> Either c a
-> Either x (Either c z)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either c z -> Either x (Either c z)
forall a b. b -> Either a b
Right (Either c z -> Either x (Either c z))
-> (c -> Either c z) -> c -> Either x (Either c z)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c -> Either c z
forall a b. a -> Either a b
Left) ((z -> Either c z) -> Either x z -> Either x (Either c z)
forall a b. (a -> b) -> Either x a -> Either x b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap z -> Either c z
forall a b. b -> Either a b
Right (Either x z -> Either x (Either c z))
-> (a -> Either x z) -> a -> Either x (Either c z)
forall b c a. (b -> c) -> (a -> b) -> a -> c
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))  = c -> Either c b
forall a b. a -> Either a b
Left c
c
    l' (Right (Right z
z)) = b -> Either c b
forall a b. b -> Either a b
Right (Either y z -> b
l (z -> Either y z
forall a b. b -> Either a b
Right z
z))
    l' (Left y
y)          = b -> Either c b
forall a b. b -> Either a b
Right (Either y z -> b
l (y -> Either y z
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 = p (Either d a) (Either d b) -> p a b
forall d a b. p (Either d a) (Either d b) -> p a b
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 a b)
-> (p (Either a d) (Either b d) -> p (Either d a) (Either d b))
-> p (Either a d) (Either b d)
-> p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 a d)
-> (Either b d -> Either d b)
-> p (Either a d) (Either b d)
-> p (Either d a) (Either d b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((d -> Either a d) -> (a -> Either a d) -> Either d a -> Either a d
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either d -> Either a d
forall a b. b -> Either a b
Right a -> Either a d
forall a b. a -> Either a b
Left) ((b -> Either d b) -> (d -> Either d b) -> Either b d -> Either d b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> Either d b
forall a b. b -> Either a b
Right d -> Either d b
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 = p (Either a d) (Either b d) -> p a b
forall a d b. p (Either a d) (Either b d) -> p a b
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 a b)
-> (p (Either d a) (Either d b) -> p (Either a d) (Either b d))
-> p (Either d a) (Either d b)
-> p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 d a)
-> (Either d b -> Either b d)
-> p (Either d a) (Either d b)
-> p (Either a d) (Either b d)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a -> Either d a) -> (d -> Either d a) -> Either a d -> Either d a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Either d a
forall a b. b -> Either a b
Right d -> Either d a
forall a b. a -> Either a b
Left) ((d -> Either b d) -> (b -> Either b d) -> Either d b -> Either b d
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either d -> Either b d
forall a b. b -> Either a b
Right b -> Either b d
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 (Either a d -> b) -> (a -> Either a d) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either a d
forall a b. a -> Either a b
Left where go :: Either a d -> b
go = (b -> b) -> (d -> b) -> Either b d -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Either a d -> b
go (Either a d -> b) -> (d -> Either a d) -> d -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Either a d
forall a b. b -> Either a b
Right) (Either b d -> b) -> (Either a d -> Either b d) -> Either a d -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 (Either d a -> b) -> (a -> Either d a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either d a
forall a b. b -> Either a b
Right where go :: Either d a -> b
go = (d -> b) -> (b -> b) -> Either d b -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either d a -> b
go (Either d a -> b) -> (d -> Either d a) -> d -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Either d a
forall a b. a -> Either a b
Left) b -> b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Either d b -> b) -> (Either d a -> Either d b) -> Either d a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) = (f a -> b) -> Costar f a b
forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar (f (Either a d) -> b
go (f (Either a d) -> b) -> (f a -> f (Either a d)) -> f a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Either a d) -> f a -> f (Either a d)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a d
forall a b. a -> Either a b
Left)
    where go :: f (Either a d) -> b
go = (b -> b) -> (d -> b) -> Either b d -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (f (Either a d) -> b
go (f (Either a d) -> b) -> (d -> f (Either a d)) -> d -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 -> f (Either a d)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either a d -> f (Either a d))
-> (d -> Either a d) -> d -> f (Either a d)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Either a d
forall a b. b -> Either a b
Right) (Either b d -> b)
-> (f (Either a d) -> Either b d) -> f (Either a d) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) = (a -> f b) -> Star f a b
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (Either d a -> f b
go (Either d a -> f b) -> (a -> Either d a) -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either d a
forall a b. b -> Either a b
Right)
    where go :: Either d a -> f b
go = (d -> f b) -> (f b -> f b) -> Either d (f b) -> f b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either d a -> f b
go (Either d a -> f b) -> (d -> Either d a) -> d -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Either d a
forall a b. a -> Either a b
Left) f b -> f b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (Either d (f b) -> f b)
-> (Either d a -> Either d (f b)) -> Either d a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f (Either d b) -> Either d (f b)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => f (m a) -> m (f a)
sequence (f (Either d b) -> Either d (f b))
-> (Either d a -> f (Either d b)) -> Either d a -> Either d (f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
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) = f (p a b) -> Tannen f p a b
forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen ((p (Either a d) (Either b d) -> p a b)
-> f (p (Either a d) (Either b d)) -> f (p a b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p (Either a d) (Either b d) -> p a b
forall a d b. p (Either a d) (Either b d) -> p a b
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) = f (p a b) -> Tannen f p a b
forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen ((p (Either d a) (Either d b) -> p a b)
-> f (p (Either d a) (Either d b)) -> f (p a b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p (Either d a) (Either d b) -> p a b
forall d a b. p (Either d a) (Either d b) -> p a b
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) = p a b -> q a b -> Product p q a b
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 (p (Either a d) (Either b d) -> p a b
forall a d b. p (Either a d) (Either b d) -> p a b
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) (q (Either a d) (Either b d) -> q a b
forall a d b. q (Either a d) (Either b d) -> q a b
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) = p a b -> q a b -> Product p q a b
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 (p (Either d a) (Either d b) -> p a b
forall d a b. p (Either d a) (Either d b) -> p a b
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) (q (Either d a) (Either d b) -> q a b
forall d a b. q (Either d a) (Either d b) -> q a b
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) = p a b -> Sum p q a b
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (p (Either a d) (Either b d) -> p a b
forall a d b. p (Either a d) (Either b d) -> p a b
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) = q a b -> Sum p q a b
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (q (Either a d) (Either b d) -> q a b
forall a d b. q (Either a d) (Either b d) -> q a b
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) = p a b -> Sum p q a b
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (p (Either d a) (Either d b) -> p a b
forall d a b. p (Either d a) (Either d b) -> p a b
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) = q a b -> Sum p q a b
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (q (Either d a) (Either d b) -> q a b
forall d a b. q (Either d a) (Either d b) -> q a b
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) = (a -> r) -> Forget r a b
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (Either a d -> r
f (Either a d -> r) -> (a -> Either a d) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either a d
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) = (a -> r) -> Forget r a b
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (Either d a -> r
f (Either d a -> r) -> (a -> Either d a) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Either d a
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) = (r :-> p) -> r a c -> CotambaraSum p a c
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r a b -> p a b
r :-> p
n ((a -> b) -> r b c -> r a c
forall a b c. (a -> b) -> r b c -> r a c
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) = (r :-> p) -> r a c -> CotambaraSum p a c
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r a b -> p a b
r :-> p
n ((b -> c) -> r a b -> r a c
forall b c a. (b -> c) -> r a b -> r a c
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) = (r :-> p) -> r a d -> CotambaraSum p a d
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r a b -> p a b
r :-> p
n ((a -> b) -> (c -> d) -> r b c -> r a d
forall a b c d. (a -> b) -> (c -> d) -> r b c -> r a d
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) = (r :-> q) -> r a b -> CotambaraSum q a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum (p a b -> q a b
p :-> q
f (p a b -> q a b) -> (r a b -> p a b) -> r a b -> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. r a b -> p a b
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 a b -> p a b
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) = (CotambaraSum p :-> CotambaraSum p)
-> CotambaraSum p a b -> CotambaraSum (CotambaraSum p) a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum CotambaraSum p a b -> CotambaraSum p a b
forall a. a -> a
CotambaraSum p :-> CotambaraSum p
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id ((r :-> p) -> r a b -> CotambaraSum p a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r a b -> p a b
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) = (r :-> p) -> r a b -> CotambaraSum p a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r a b -> p a b
r :-> p
n (r (Either a d) (Either b d) -> r a b
forall a d b. r (Either a d) (Either b d) -> r a b
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) = (r :-> p) -> r a b -> CotambaraSum p a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum r a b -> p a b
r :-> p
n (r (Either d a) (Either d b) -> r a b
forall d a b. r (Either d a) (Either d b) -> r a b
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 = (a -> b) -> CotambaraSum p a a -> CotambaraSum p a b
forall b c a. (b -> c) -> CotambaraSum p a b -> CotambaraSum p a c
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 = (p :-> q) -> p a b -> CotambaraSum q a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum p a b -> q a b
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 = CotambaraSum q a b -> q a b
CotambaraSum q :-> q
forall (p :: * -> * -> *). Profunctor p => CotambaraSum p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract (p a b -> CotambaraSum q a b
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> CopastroSum p a b)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> (a -> b) -> r a a -> r a b
forall b c a. (b -> c) -> r a b -> r a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
f ((forall x y. p x y -> r x y) -> r a a
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a a
h p x y -> r x y
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a d)
-> CopastroSum p a d
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a d)
 -> CopastroSum p a d)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a d)
-> CopastroSum p a d
forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> (a -> b) -> (c -> d) -> r b c -> r a d
forall a b c d. (a -> b) -> (c -> d) -> r b c -> r a d
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 x y. p x y -> r x y) -> r b c
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r b c
h p x y -> r x y
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a c)
-> CopastroSum p a c
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a c)
 -> CopastroSum p a c)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a c)
-> CopastroSum p a c
forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> (a -> b) -> r b c -> r a c
forall a b c. (a -> b) -> r b c -> r a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f ((forall x y. p x y -> r x y) -> r b c
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r b c
h p x y -> r x y
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a c)
-> CopastroSum p a c
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a c)
 -> CopastroSum p a c)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a c)
-> CopastroSum p a c
forall a b. (a -> b) -> a -> b
$ \ forall x y. p x y -> r x y
n -> (b -> c) -> r a b -> r a c
forall b c a. (b -> c) -> r a b -> r a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
g ((forall x y. p x y -> r x y) -> r a b
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a b
h p x y -> r x y
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 = (CopastroSum p :-> CopastroSum p)
-> CopastroSum p a b -> CotambaraSum (CopastroSum p) a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Cochoice r =>
(r :-> q) -> r a b -> CotambaraSum q a b
CotambaraSum CopastroSum p a b -> CopastroSum p a b
forall a. a -> a
CopastroSum p :-> CopastroSum p
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (p a b -> CopastroSum p a b
p :-> CopastroSum p
forall (p :: * -> * -> *). Profunctor p => p :-> CopastroSum p
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) = CotambaraSum p a b -> p a b
CotambaraSum p :-> p
forall (p :: * -> * -> *). Profunctor p => CotambaraSum p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract ((forall x y. CotambaraSum p x y -> CotambaraSum p x y)
-> CotambaraSum p a b
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. CotambaraSum p x y -> r x y) -> r a b
h CotambaraSum p x y -> CotambaraSum p x y
forall a. a -> a
forall x y. CotambaraSum p x y -> CotambaraSum p x y
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. q x y -> r x y) -> r a b)
-> CopastroSum q a b
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. q x y -> r x y) -> r a b)
 -> CopastroSum q a b)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. q x y -> r x y) -> r a b)
-> CopastroSum q a b
forall a b. (a -> b) -> a -> b
$ \forall x y. q x y -> r x y
n -> (forall x y. p x y -> r x y) -> r a b
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r a b
h (q x y -> r x y
forall x y. q x y -> r x y
n (q x y -> r x y) -> (p x y -> q x y) -> p x y -> r x y
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p x y -> q x y
p :-> q
f)

instance ProfunctorMonad CopastroSum where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> CopastroSum p
proreturn p a b
p = (forall (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> CopastroSum p a b)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> p a b -> r a b
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> CopastroSum p a b)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
c -> CopastroSum (CopastroSum p) a b
-> forall (r :: * -> * -> *).
   Cochoice r =>
   (forall x y. CopastroSum p x y -> r x y) -> r a b
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 -> CopastroSum p x y
-> forall (r :: * -> * -> *).
   Cochoice r =>
   (forall x y. p x y -> r x y) -> r x y
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 p x y -> r x y
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> CopastroSum p a b)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> r (Either a d) (Either b d) -> r a b
forall a d b. r (Either a d) (Either b d) -> r a b
forall (p :: * -> * -> *) a d b.
Cochoice p =>
p (Either a d) (Either b d) -> p a b
unleft ((forall x y. p x y -> r x y) -> r (Either a d) (Either b d)
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r (Either a d) (Either b d)
p p x y -> r x y
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 (r :: * -> * -> *).
 Cochoice r =>
 (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
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 (r :: * -> * -> *).
  Cochoice r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> CopastroSum p a b)
-> (forall (r :: * -> * -> *).
    Cochoice r =>
    (forall x y. p x y -> r x y) -> r a b)
-> CopastroSum p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> r (Either d a) (Either d b) -> r a b
forall d a b. r (Either d a) (Either d b) -> r a b
forall (p :: * -> * -> *) d a b.
Cochoice p =>
p (Either d a) (Either d b) -> p a b
unright ((forall x y. p x y -> r x y) -> r (Either d a) (Either d b)
forall (r :: * -> * -> *).
Cochoice r =>
(forall x y. p x y -> r x y) -> r (Either d a) (Either d b)
p p x y -> r x y
forall x y. p x y -> r x y
n)