{-# 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.Strong
  (
  -- * Strength
    Strong(..)
  , uncurry'
  , strong
  , Tambara(..)
  , tambara, untambara
  , Pastro(..)
  , pastro, unpastro
  -- * Costrength
  , Costrong(..)
  , Cotambara(..)
  , cotambara, uncotambara
  , Copastro(..)
  ) where

import Control.Applicative hiding (WrappedArrow(..))
import Control.Arrow
import Control.Category
import Control.Comonad
import Control.Monad (liftM)
import Control.Monad.Fix
import Data.Bifunctor.Clown (Clown(..))
import Data.Bifunctor.Product (Product(..))
import Data.Bifunctor.Sum (Sum(..))
import Data.Bifunctor.Tannen (Tannen(..))
import Data.Functor.Contravariant (Contravariant(..))
import Data.Profunctor.Adjunction
import Data.Profunctor.Monad
import Data.Profunctor.Types
import Data.Profunctor.Unsafe
import Data.Semigroup hiding (Product, Sum)
import Data.Tagged
import Data.Tuple
import Prelude hiding (id,(.))

------------------------------------------------------------------------------
-- Strong
------------------------------------------------------------------------------

-- | Generalizing 'Star' of a strong 'Functor'
--
-- /Note:/ Every 'Functor' in Haskell is strong with respect to @(,)@.
--
-- This describes profunctor strength with respect to the product structure
-- of Hask.
--
-- <http://www.riec.tohoku.ac.jp/~asada/papers/arrStrMnd.pdf>
--
class Profunctor p => Strong p where
  -- | Laws:
  --
  -- @
  -- 'first'' ≡ 'dimap' 'swap' 'swap' '.' 'second''
  -- 'lmap' 'fst' ≡ 'rmap' 'fst' '.' 'first''
  -- 'lmap' ('second'' f) '.' 'first'' ≡ 'rmap' ('second'' f) '.' 'first''
  -- 'first'' '.' 'first'' ≡ 'dimap' assoc unassoc '.' 'first'' where
  --   assoc ((a,b),c) = (a,(b,c))
  --   unassoc (a,(b,c)) = ((a,b),c)
  -- @
  first' :: p a b  -> p (a, c) (b, c)
  first' = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. (a, b) -> (b, a)
swap forall a b. (a, b) -> (b, a)
swap 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.
Strong p =>
p a b -> p (c, a) (c, b)
second'

  -- | Laws:
  --
  -- @
  -- 'second'' ≡ 'dimap' 'swap' 'swap' '.' 'first''
  -- 'lmap' 'snd' ≡ 'rmap' 'snd' '.' 'second''
  -- 'lmap' ('first'' f) '.' 'second'' ≡ 'rmap' ('first'' f) '.' 'second''
  -- 'second'' '.' 'second'' ≡ 'dimap' unassoc assoc '.' 'second'' where
  --   assoc ((a,b),c) = (a,(b,c))
  --   unassoc (a,(b,c)) = ((a,b),c)
  -- @
  second' :: p a b -> p (c, a) (c, b)
  second' = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. (a, b) -> (b, a)
swap forall a b. (a, b) -> (b, a)
swap 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.
Strong p =>
p a b -> p (a, c) (b, c)
first'

  {-# MINIMAL first' | second' #-}

uncurry' :: Strong p => p a (b -> c) -> p (a, b) c
uncurry' :: forall (p :: * -> * -> *) a b c.
Strong p =>
p a (b -> c) -> p (a, b) c
uncurry' = forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap (\(b -> c
f,b
x) -> b -> c
f b
x) 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.
Strong p =>
p a b -> p (a, c) (b, c)
first'
{-# INLINE uncurry' #-}

strong :: Strong p => (a -> b -> c) -> p a b -> p a c
strong :: forall (p :: * -> * -> *) a b c.
Strong p =>
(a -> b -> c) -> p a b -> p a c
strong a -> b -> c
f p a b
x = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\a
a -> (a
a, a
a)) (\(b
b, a
a) -> a -> b -> c
f a
a b
b) (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p a b
x)

instance Strong (->) where
  first' :: forall a b c. (a -> b) -> (a, c) -> (b, c)
first' a -> b
ab ~(a
a, c
c) = (a -> b
ab a
a, c
c)
  {-# INLINE first' #-}
  second' :: forall a b c. (a -> b) -> (c, a) -> (c, b)
second' a -> b
ab ~(c
c, a
a) = (c
c, a -> b
ab a
a)
  {-# INLINE second' #-}

instance Monad m => Strong (Kleisli m) where
  first' :: forall a b c. Kleisli m a b -> Kleisli m (a, c) (b, c)
first' (Kleisli a -> m b
f) = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli forall a b. (a -> b) -> a -> b
$ \ ~(a
a, c
c) -> do
     b
b <- a -> m b
f a
a
     forall (m :: * -> *) a. Monad m => a -> m a
return (b
b, c
c)
  {-# INLINE first' #-}
  second' :: forall a b c. Kleisli m a b -> Kleisli m (c, a) (c, b)
second' (Kleisli a -> m b
f) = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli forall a b. (a -> b) -> a -> b
$ \ ~(c
c, a
a) -> do
     b
b <- a -> m b
f a
a
     forall (m :: * -> *) a. Monad m => a -> m a
return (c
c, b
b)
  {-# INLINE second' #-}

instance Functor m => Strong (Star m) where
  first' :: forall a b c. Star m a b -> Star m (a, c) (b, c)
first' (Star a -> m b
f) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ \ ~(a
a, c
c) -> (\b
b' -> (b
b', c
c)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
  {-# INLINE first' #-}
  second' :: forall a b c. Star m a b -> Star m (c, a) (c, b)
second' (Star a -> m b
f) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ \ ~(c
c, a
a) -> (,) c
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
a
  {-# INLINE second' #-}

-- | 'Arrow' is 'Strong' 'Category'
instance Arrow p => Strong (WrappedArrow p) where
  first' :: forall a b c. WrappedArrow p a b -> WrappedArrow p (a, c) (b, c)
first' (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.
Arrow a =>
a b c -> a (b, d) (c, d)
first p a b
k)
  {-# INLINE first' #-}
  second' :: forall a b c. WrappedArrow p a b -> WrappedArrow p (c, a) (c, b)
second' (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.
Arrow a =>
a b c -> a (d, b) (d, c)
second p a b
k)
  {-# INLINE second' #-}

instance Strong (Forget r) where
  first' :: forall a b c. Forget r a b -> Forget r (a, c) (b, c)
first' (Forget a -> r
k) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (a -> r
k 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, b) -> a
fst)
  {-# INLINE first' #-}
  second' :: forall a b c. Forget r a b -> Forget r (c, a) (c, b)
second' (Forget a -> r
k) = forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (a -> r
k 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, b) -> b
snd)
  {-# INLINE second' #-}

instance Contravariant f => Strong (Clown f) where
  first' :: forall a b c. Clown f a b -> Clown f (a, c) (b, c)
first' (Clown f a
fa) = forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown (forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall a b. (a, b) -> a
fst f a
fa)
  {-# INLINE first' #-}
  second' :: forall a b c. Clown f a b -> Clown f (c, a) (c, b)
second' (Clown f a
fa) = forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown (forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall a b. (a, b) -> b
snd f a
fa)
  {-# INLINE second' #-}

instance (Strong p, Strong q) => Strong (Product p q) where
  first' :: forall a b c. Product p q a b -> Product p q (a, c) (b, c)
first' (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.
Strong p =>
p a b -> p (a, c) (b, c)
first' p a b
p) (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' q a b
q)
  {-# INLINE first' #-}
  second' :: forall a b c. Product p q a b -> Product p q (c, a) (c, b)
second' (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.
Strong p =>
p a b -> p (c, a) (c, b)
second' p a b
p) (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' q a b
q)
  {-# INLINE second' #-}

instance (Strong p, Strong q) => Strong (Sum p q) where
  first' :: forall a b c. Sum p q a b -> Sum p q (a, c) (b, c)
first' (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.
Strong p =>
p a b -> p (a, c) (b, c)
first' p a b
p)
  first' (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.
Strong p =>
p a b -> p (a, c) (b, c)
first' q a b
q)
  {-# INLINE first' #-}
  second' :: forall a b c. Sum p q a b -> Sum p q (c, a) (c, b)
second' (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.
Strong p =>
p a b -> p (c, a) (c, b)
second' p a b
p)
  second' (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.
Strong p =>
p a b -> p (c, a) (c, b)
second' q a b
q)
  {-# INLINE second' #-}

instance (Functor f, Strong p) => Strong (Tannen f p) where
  first' :: forall a b c. Tannen f p a b -> Tannen f p (a, c) (b, c)
first' (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.
Strong p =>
p a b -> p (a, c) (b, c)
first' f (p a b)
fp)
  {-# INLINE first' #-}
  second' :: forall a b c. Tannen f p a b -> Tannen f p (c, a) (c, b)
second' (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.
Strong p =>
p a b -> p (c, a) (c, b)
second' f (p a b)
fp)
  {-# INLINE second' #-}

----------------------------------------------------------------------------
-- * Tambara
----------------------------------------------------------------------------

-- | 'Tambara' cofreely makes any 'Profunctor' 'Strong'.
newtype Tambara p a b = Tambara { forall (p :: * -> * -> *) a b.
Tambara p a b -> forall c. p (a, c) (b, c)
runTambara :: forall c. p (a, c) (b, c) }

instance Profunctor p => Profunctor (Tambara p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Tambara p b c -> Tambara p a d
dimap a -> b
f c -> d
g (Tambara forall c. p (b, c) (c, c)
p) = 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 d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a -> b
f) (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first c -> d
g) forall c. p (b, c) (c, c)
p
  {-# INLINE dimap #-}

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

instance ProfunctorComonad Tambara where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Tambara p :-> p
proextract (Tambara forall c. p (a, c) (b, c)
p) = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\a
a -> (a
a,())) forall a b. (a, b) -> a
fst forall c. p (a, c) (b, c)
p
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Tambara p :-> Tambara (Tambara p)
produplicate (Tambara forall c. p (a, c) (b, c)
p) = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (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. ((a, b), c) -> (a, (b, c))
hither forall a b c. (a, (b, c)) -> ((a, b), c)
yon forall c. p (a, c) (b, c)
p) where
    hither :: ((a, b), c) -> (a, (b, c))
    hither :: forall a b c. ((a, b), c) -> (a, (b, c))
hither ~(~(a
x,b
y),c
z) = (a
x,(b
y,c
z))

    yon    :: (a, (b, c)) -> ((a, b), c)
    yon :: forall a b c. (a, (b, c)) -> ((a, b), c)
yon    ~(a
x,~(b
y,c
z)) = ((a
x,b
y),c
z)

instance Profunctor p => Strong (Tambara p) where
  first' :: forall a b c. Tambara p a b -> Tambara p (a, c) (b, c)
first' Tambara p a b
p = forall (p :: * -> * -> *) a b.
Tambara p a b -> forall c. p (a, c) (b, c)
runTambara forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> t (t p)
produplicate Tambara p a b
p
  {-# INLINE first' #-}

instance Category p => Category (Tambara p) where
  id :: forall a. Tambara p a a
id = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  Tambara forall c. p (b, c) (c, c)
p . :: forall b c a. Tambara p b c -> Tambara p a b -> Tambara p a c
. Tambara forall c. p (a, c) (b, c)
q = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (forall c. p (b, c) (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 (a, c) (b, c)
q)

instance Arrow p => Arrow (Tambara p) where
  arr :: forall b c. (b -> c) -> Tambara p b c
arr 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 (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first b -> c
f
  first :: forall b c d. Tambara p b c -> Tambara p (b, d) (c, d)
first (Tambara forall c. p (b, c) (c, c)
f) = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b c. ((a, b), c) -> ((a, c), 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 c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall c. p (b, c) (c, c)
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 c. Arrow a => (b -> c) -> a b c
arr forall a b c. ((a, b), c) -> ((a, c), b)
go) where
    go :: ((a, b), c) -> ((a, c), b)
    go :: forall a b c. ((a, b), c) -> ((a, c), b)
go ~(~(a
x,b
y),c
z) = ((a
x,c
z),b
y)

instance ArrowChoice p => ArrowChoice (Tambara p) where
  left :: forall b c d. Tambara p b c -> Tambara p (Either b d) (Either c d)
left (Tambara forall c. p (b, c) (c, c)
f) = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a c b. Either (a, c) (b, c) -> (Either a b, c)
yon 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 c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left forall c. p (b, c) (c, c)
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 c. Arrow a => (b -> c) -> a b c
arr forall a b c. (Either a b, c) -> Either (a, c) (b, c)
hither) 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)

instance ArrowApply p => ArrowApply (Tambara p) where
  app :: forall b c. Tambara p (Tambara p b c, b) c
app = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c. ArrowApply a => a (a b c, b) c
app 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 c. Arrow a => (b -> c) -> a b c
arr (\((Tambara forall c. p (b, c) (c, c)
f, b
x), c
s) -> (forall c. p (b, c) (c, c)
f, (b
x, c
s)))

instance ArrowLoop p => ArrowLoop (Tambara p) where
  loop :: forall b d c. Tambara p (b, d) (c, d) -> Tambara p b c
loop (Tambara forall c. p ((b, d), c) ((c, d), c)
f) = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (forall (a :: * -> * -> *) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b c. ((a, b), c) -> ((a, c), 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 c. p ((b, d), c) ((c, d), c)
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 c. Arrow a => (b -> c) -> a b c
arr forall a b c. ((a, b), c) -> ((a, c), b)
go)) where
    go :: ((a, b), c) -> ((a, c), b)
    go :: forall a b c. ((a, b), c) -> ((a, c), b)
go ~(~(a
x,b
y),c
z) = ((a
x,c
z),b
y)

instance ArrowZero p => ArrowZero (Tambara p) where
  zeroArrow :: forall b c. Tambara p b c
zeroArrow = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow

instance ArrowPlus p => ArrowPlus (Tambara p) where
  Tambara forall c. p (b, c) (c, c)
f <+> :: forall b c. Tambara p b c -> Tambara p b c -> Tambara p b c
<+> Tambara forall c. p (b, c) (c, c)
g = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (forall c. p (b, c) (c, c)
f forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> forall c. p (b, c) (c, c)
g)

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

instance (Profunctor p, Arrow p) => Applicative (Tambara p a) where
  pure :: forall a. a -> Tambara p a a
pure a
x = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b. a -> b -> a
const a
x)
  Tambara p a (a -> b)
f <*> :: forall a b. Tambara p a (a -> b) -> Tambara p a a -> Tambara p a b
<*> Tambara p a a
g = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry 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
. (Tambara p a (a -> b)
f forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Tambara p a a
g)

instance (Profunctor p, ArrowPlus p) => Alternative (Tambara p a) where
  empty :: forall a. Tambara p a a
empty = forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow
  Tambara p a a
f <|> :: forall a. Tambara p a a -> Tambara p a a -> Tambara p a a
<|> Tambara p a a
g = Tambara p a a
f forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> Tambara p a a
g

instance ArrowPlus p => Semigroup (Tambara p a b) where
  Tambara p a b
f <> :: Tambara p a b -> Tambara p a b -> Tambara p a b
<> Tambara p a b
g = Tambara p a b
f forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> Tambara p a b
g

instance ArrowPlus p => Monoid (Tambara p a b) where
  mempty :: Tambara p a b
mempty = forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow
#if !(MIN_VERSION_base(4,11,0))
  mappend = (<>)
#endif

-- |
-- @
-- 'tambara' ('untambara' f) ≡ f
-- 'untambara' ('tambara' f) ≡ f
-- @
tambara :: Strong p => (p :-> q) -> p :-> Tambara q
tambara :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Strong p =>
(p :-> q) -> p :-> Tambara q
tambara p :-> q
f p a b
p = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara forall a b. (a -> b) -> a -> b
$ p :-> q
f forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p a b
p

-- |
-- @
-- 'tambara' ('untambara' f) ≡ f
-- 'untambara' ('tambara' f) ≡ f
-- @
untambara :: Profunctor q => (p :-> Tambara q) -> p :-> q
untambara :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Profunctor q =>
(p :-> Tambara q) -> p :-> q
untambara p :-> Tambara 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 (\a
a -> (a
a,())) forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b.
Tambara p a b -> forall c. p (a, c) (b, c)
runTambara forall a b. (a -> b) -> a -> b
$ p :-> Tambara q
f p a b
p

----------------------------------------------------------------------------
-- * Pastro
----------------------------------------------------------------------------

-- | Pastro -| Tambara
--
-- @
-- Pastro p ~ exists z. Costar ((,)z) `Procompose` p `Procompose` Star ((,)z)
-- @
--
-- 'Pastro' freely makes any 'Profunctor' 'Strong'.
data Pastro p a b where
  Pastro :: ((y, z) -> b) -> p x y -> (a -> (x, z)) -> Pastro p a b

instance Functor (Pastro p a) where
  fmap :: forall a b. (a -> b) -> Pastro p a a -> Pastro p a b
fmap a -> b
f (Pastro (y, z) -> a
l p x y
m a -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (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
. (y, z) -> a
l) p x y
m a -> (x, z)
r

instance Profunctor (Pastro p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Pastro p b c -> Pastro p a d
dimap a -> b
f c -> d
g (Pastro (y, z) -> c
l p x y
m b -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (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
. (y, z) -> c
l) p x y
m (b -> (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) -> Pastro p b c -> Pastro p a c
lmap a -> b
f (Pastro (y, z) -> c
l p x y
m b -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (y, z) -> c
l p x y
m (b -> (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) -> Pastro p a b -> Pastro p a c
rmap b -> c
g (Pastro (y, z) -> b
l p x y
m a -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (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
. (y, z) -> b
l) p x y
m a -> (x, z)
r
  q b c
w #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Pastro p a b -> Pastro p a c
#. Pastro (y, z) -> b
l p x y
m a -> (x, z)
r = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (q b c
w forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. (y, z) -> b
l) p x y
m a -> (x, z)
r
  Pastro (y, z) -> c
l p x y
m b -> (x, z)
r .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Pastro p b c -> q a b -> Pastro p a c
.# q a b
w = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (y, z) -> c
l p x y
m (b -> (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 ProfunctorFunctor Pastro where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Pastro p :-> Pastro q
promap p :-> q
f (Pastro (y, z) -> b
l p x y
m a -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (y, z) -> b
l (p :-> q
f p x y
m) a -> (x, z)
r

instance ProfunctorMonad Pastro where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Pastro p
proreturn p a b
p = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro forall a b. (a, b) -> a
fst p a b
p forall a b. (a -> b) -> a -> b
$ \a
a -> (a
a,())
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
Pastro (Pastro p) :-> Pastro p
projoin (Pastro (y, z) -> b
l (Pastro (y, z) -> y
m p x y
n x -> (x, z)
o) a -> (x, z)
p) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (y, (z, z)) -> b
lm p x y
n a -> (x, (z, z))
op where
    op :: a -> (x, (z, z))
op a
a = case a -> (x, z)
p a
a of
      (x
b, z
f) -> case x -> (x, z)
o x
b of
         (x
c, z
g) -> (x
c, (z
f, z
g))
    lm :: (y, (z, z)) -> b
lm (y
d, (z
f, z
g)) = (y, z) -> b
l ((y, z) -> y
m (y
d, z
g), z
f)

instance ProfunctorAdjunction Pastro Tambara where
  counit :: forall (p :: * -> * -> *). Profunctor p => Pastro (Tambara p) :-> p
counit (Pastro (y, z) -> b
g (Tambara forall c. p (x, c) (y, c)
p) a -> (x, z)
f) = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> (x, z)
f (y, z) -> b
g forall c. p (x, c) (y, c)
p
  unit :: forall (p :: * -> * -> *). Profunctor p => p :-> Tambara (Pastro p)
unit p a b
p = forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro 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 Strong (Pastro p) where
  first' :: forall a b c. Pastro p a b -> Pastro p (a, c) (b, c)
first' (Pastro (y, z) -> b
l p x y
m a -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (y, (z, c)) -> (b, c)
l' p x y
m (a, c) -> (x, (z, c))
r' where
    r' :: (a, c) -> (x, (z, c))
r' (a
a,c
c) = case a -> (x, z)
r a
a of
      (x
x,z
z) -> (x
x,(z
z,c
c))
    l' :: (y, (z, c)) -> (b, c)
l' (y
y,(z
z,c
c)) = ((y, z) -> b
l (y
y,z
z), c
c)
  second' :: forall a b c. Pastro p a b -> Pastro p (c, a) (c, b)
second' (Pastro (y, z) -> b
l p x y
m a -> (x, z)
r) = forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (y, (c, z)) -> (c, b)
l' p x y
m (c, a) -> (x, (c, z))
r' where
    r' :: (c, a) -> (x, (c, z))
r' (c
c,a
a) = case a -> (x, z)
r a
a of
      (x
x,z
z) -> (x
x,(c
c,z
z))
    l' :: (y, (c, z)) -> (c, b)
l' (y
y,(c
c,z
z)) = (c
c,(y, z) -> b
l (y
y,z
z))

-- |
-- @
-- 'pastro' ('unpastro' f) ≡ f
-- 'unpastro' ('pastro' f) ≡ f
-- @
pastro :: Strong q => (p :-> q) -> Pastro p :-> q
pastro :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Strong q =>
(p :-> q) -> Pastro p :-> q
pastro p :-> q
f (Pastro (y, z) -> b
r p x y
g a -> (x, z)
l) = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> (x, z)
l (y, z) -> b
r (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' (p :-> q
f p x y
g))

-- |
-- @
-- 'pastro' ('unpastro' f) ≡ f
-- 'unpastro' ('pastro' f) ≡ f
-- @
unpastro :: (Pastro p :-> q) -> p :-> q
unpastro :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(Pastro p :-> q) -> p :-> q
unpastro Pastro p :-> q
f p a b
p = Pastro p :-> q
f (forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro forall a b. (a, b) -> a
fst p a b
p (\a
a -> (a
a, ())))

--------------------------------------------------------------------------------
-- * Costrength for (,)
--------------------------------------------------------------------------------

-- | Analogous to 'ArrowLoop', 'loop' = 'unfirst'
class Profunctor p => Costrong p where
  -- | Laws:
  --
  -- @
  -- 'unfirst' ≡ 'unsecond' '.' 'dimap' 'swap' 'swap'
  -- 'lmap' (,()) ≡ 'unfirst' '.' 'rmap' (,())
  -- 'unfirst' '.' 'lmap' ('second' f) ≡ 'unfirst' '.' 'rmap' ('second' f)
  -- 'unfirst' '.' 'unfirst' = 'unfirst' '.' 'dimap' assoc unassoc where
  --   assoc ((a,b),c) = (a,(b,c))
  --   unassoc (a,(b,c)) = ((a,b),c)
  -- @
  unfirst  :: p (a, d) (b, d) -> p a b
  unfirst = forall (p :: * -> * -> *) d a b.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond 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 b. (a, b) -> (b, a)
swap forall a b. (a, b) -> (b, a)
swap

  -- | Laws:
  --
  -- @
  -- 'unsecond' ≡ 'unfirst' '.' 'dimap' 'swap' 'swap'
  -- 'lmap' ((),) ≡ 'unsecond' '.' 'rmap' ((),)
  -- 'unsecond' '.' 'lmap' ('first' f) ≡ 'unsecond' '.' 'rmap' ('first' f)
  -- 'unsecond' '.' 'unsecond' = 'unsecond' '.' 'dimap' unassoc assoc where
  --   assoc ((a,b),c) = (a,(b,c))
  --   unassoc (a,(b,c)) = ((a,b),c)
  -- @
  unsecond :: p (d, a) (d, b) -> p a b
  unsecond = forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst 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 b. (a, b) -> (b, a)
swap forall a b. (a, b) -> (b, a)
swap

  {-# MINIMAL unfirst | unsecond #-}

instance Costrong (->) where
  unfirst :: forall a d b. ((a, d) -> (b, d)) -> a -> b
unfirst (a, d) -> (b, d)
f a
a = b
b where (b
b, d
d) = (a, d) -> (b, d)
f (a
a, d
d)
  unsecond :: forall d a b. ((d, a) -> (d, b)) -> a -> b
unsecond (d, a) -> (d, b)
f a
a = b
b where (d
d, b
b) = (d, a) -> (d, b)
f (d
d, a
a)

instance Functor f => Costrong (Costar f) where
  unfirst :: forall a d b. Costar f (a, d) (b, d) -> Costar f a b
unfirst (Costar f (a, d) -> (b, d)
f) = forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar f a -> b
f'
    where f' :: f a -> b
f' f a
fa = b
b where (b
b, d
d) = f (a, d) -> (b, d)
f ((\a
a -> (a
a, d
d)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
fa)
  unsecond :: forall d a b. Costar f (d, a) (d, b) -> Costar f a b
unsecond (Costar f (d, a) -> (d, b)
f) = forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar f a -> b
f'
    where f' :: f a -> b
f' f a
fa = b
b where (d
d, b
b) = f (d, a) -> (d, b)
f ((,) d
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
fa)

instance Costrong Tagged where
  unfirst :: forall a d b. Tagged (a, d) (b, d) -> Tagged a b
unfirst (Tagged (b, d)
bd) = forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a b. (a, b) -> a
fst (b, d)
bd)
  unsecond :: forall d a b. Tagged (d, a) (d, b) -> Tagged a b
unsecond (Tagged (d, b)
db) = forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a b. (a, b) -> b
snd (d, b)
db)

instance ArrowLoop p => Costrong (WrappedArrow p) where
  unfirst :: forall a d b. WrappedArrow p (a, d) (b, d) -> WrappedArrow p a b
unfirst (WrapArrow p (a, d) (b, d)
k) = forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
p a b -> WrappedArrow p a b
WrapArrow (forall (a :: * -> * -> *) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop p (a, d) (b, d)
k)

instance MonadFix m => Costrong (Kleisli m) where
  unfirst :: forall a d b. Kleisli m (a, d) (b, d) -> Kleisli m a b
unfirst (Kleisli (a, d) -> m (b, d)
f) = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a b. (a, b) -> a
fst forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> (b, d) -> m (b, d)
f')
    where f' :: a -> (b, d) -> m (b, d)
f' a
x (b, d)
y = (a, d) -> m (b, d)
f (a
x, forall a b. (a, b) -> b
snd (b, d)
y)

instance Functor f => Costrong (Cokleisli f) where
  unfirst :: forall a d b. Cokleisli f (a, d) (b, d) -> Cokleisli f a b
unfirst (Cokleisli f (a, d) -> (b, d)
f) = forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli f a -> b
f'
    where f' :: f a -> b
f' f a
fa = b
b where (b
b, d
d) = f (a, d) -> (b, d)
f ((\a
a -> (a
a, d
d)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
fa)

instance (Functor f, Costrong p) => Costrong (Tannen f p) where
  unfirst :: forall a d b. Tannen f p (a, d) (b, d) -> Tannen f p a b
unfirst (Tannen f (p (a, d) (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.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst f (p (a, d) (b, d))
fp)
  unsecond :: forall d a b. Tannen f p (d, a) (d, b) -> Tannen f p a b
unsecond (Tannen f (p (d, a) (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.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond f (p (d, a) (d, b))
fp)

instance (Costrong p, Costrong q) => Costrong (Product p q) where
  unfirst :: forall a d b. Product p q (a, d) (b, d) -> Product p q a b
unfirst (Pair p (a, d) (b, d)
p q (a, d) (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.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst p (a, d) (b, d)
p) (forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst q (a, d) (b, d)
q)
  unsecond :: forall d a b. Product p q (d, a) (d, b) -> Product p q a b
unsecond (Pair p (d, a) (d, b)
p q (d, a) (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.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond p (d, a) (d, b)
p) (forall (p :: * -> * -> *) d a b.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond q (d, a) (d, b)
q)

instance (Costrong p, Costrong q) => Costrong (Sum p q) where
  unfirst :: forall a d b. Sum p q (a, d) (b, d) -> Sum p q a b
unfirst (L2 p (a, d) (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.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst p (a, d) (b, d)
p)
  unfirst (R2 q (a, d) (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.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst q (a, d) (b, d)
q)
  unsecond :: forall d a b. Sum p q (d, a) (d, b) -> Sum p q a b
unsecond (L2 p (d, a) (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.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond p (d, a) (d, b)
p)
  unsecond (R2 q (d, a) (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.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond q (d, a) (d, b)
q)

----------------------------------------------------------------------------
-- * Cotambara
----------------------------------------------------------------------------

-- | Cotambara cofreely constructs costrength
data Cotambara q a b where
    Cotambara :: Costrong r => (r :-> q) -> r a b -> Cotambara q a b

instance Profunctor (Cotambara p) where
  lmap :: forall a b c. (a -> b) -> Cotambara p b c -> Cotambara p a c
lmap a -> b
f (Cotambara r :-> p
n r b c
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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) -> Cotambara p a b -> Cotambara p a c
rmap b -> c
g (Cotambara r :-> p
n r a b
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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) -> Cotambara p b c -> Cotambara p a d
dimap a -> b
f c -> d
g (Cotambara r :-> p
n r b c
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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 Cotambara where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Cotambara p :-> Cotambara q
promap p :-> q
f (Cotambara r :-> p
n r a b
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara (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 Cotambara where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Cotambara p :-> p
proextract (Cotambara r :-> p
n r a b
p)  = r :-> p
n r a b
p
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Cotambara p :-> Cotambara (Cotambara p)
produplicate (Cotambara r :-> p
n r a b
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara r :-> p
n r a b
p)

instance Costrong (Cotambara p) where
  unfirst :: forall a d b. Cotambara p (a, d) (b, d) -> Cotambara p a b
unfirst (Cotambara r :-> p
n r (a, d) (b, d)
p) = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara r :-> p
n (forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst r (a, d) (b, d)
p)

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

-- |
-- @
-- 'cotambara' '.' 'uncotambara' ≡ 'id'
-- 'uncotambara' '.' 'cotambara' ≡ 'id'
-- @
cotambara :: Costrong p => (p :-> q) -> p :-> Cotambara q
cotambara :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Costrong p =>
(p :-> q) -> p :-> Cotambara q
cotambara p :-> q
f = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara p :-> q
f

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

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

-- | Copastro -| Cotambara
--
-- Copastro freely constructs costrength
newtype Copastro p a b = Copastro { forall (p :: * -> * -> *) a b.
Copastro p a b
-> forall (r :: * -> * -> *).
   Costrong r =>
   (forall x y. p x y -> r x y) -> r a b
runCopastro :: forall r. Costrong r => (forall x y. p x y -> r x y) -> r a b }

instance Functor (Copastro p a) where
  fmap :: forall a b. (a -> b) -> Copastro p a a -> Copastro p a b
fmap a -> b
f (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r a a
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro 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 :: * -> * -> *).
Costrong 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 (Copastro p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Copastro p b c -> Copastro p a d
dimap a -> b
f c -> d
g (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r b c
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro 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 :: * -> * -> *).
Costrong 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) -> Copastro p b c -> Copastro p a c
lmap a -> b
f (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r b c
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro 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 :: * -> * -> *).
Costrong 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) -> Copastro p a b -> Copastro p a c
rmap b -> c
g (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r a b
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro 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 :: * -> * -> *).
Costrong 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 Copastro Cotambara where
 unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> Cotambara (Copastro p)
unit p a b
p = forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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 =>
Copastro (Cotambara p) :-> p
counit (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. Cotambara p x y -> r x y) -> r a b
h) = forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract (forall (r :: * -> * -> *).
Costrong r =>
(forall x y. Cotambara 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 Copastro where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Copastro p :-> Copastro q
promap p :-> q
f (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r a b
h) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro forall a b. (a -> b) -> a -> b
$ \forall x y. q x y -> r x y
n -> forall (r :: * -> * -> *).
Costrong 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 Copastro where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Copastro p
proreturn p a b
p = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro 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 =>
Copastro (Copastro p) :-> Copastro p
projoin Copastro (Copastro p) a b
p = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
c -> forall (p :: * -> * -> *) a b.
Copastro p a b
-> forall (r :: * -> * -> *).
   Costrong r =>
   (forall x y. p x y -> r x y) -> r a b
runCopastro Copastro (Copastro p) a b
p (\Copastro p x y
x -> forall (p :: * -> * -> *) a b.
Copastro p a b
-> forall (r :: * -> * -> *).
   Costrong r =>
   (forall x y. p x y -> r x y) -> r a b
runCopastro Copastro p x y
x forall x y. p x y -> r x y
c)

instance Costrong (Copastro p) where
  unfirst :: forall a d b. Copastro p (a, d) (b, d) -> Copastro p a b
unfirst (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r (a, d) (b, d)
p) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst (forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r (a, d) (b, d)
p forall x y. p x y -> r x y
n)
  unsecond :: forall d a b. Copastro p (d, a) (d, b) -> Copastro p a b
unsecond (Copastro forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r (d, a) (d, b)
p) = forall (p :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
Copastro forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> forall (p :: * -> * -> *) d a b.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond (forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r (d, a) (d, b)
p forall x y. p x y -> r x y
n)