{-# 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' = ((a, c) -> (c, a))
-> ((c, b) -> (b, c)) -> p (c, a) (c, b) -> p (a, c) (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, c) -> (c, a)
forall a b. (a, b) -> (b, a)
swap (c, b) -> (b, c)
forall a b. (a, b) -> (b, a)
swap (p (c, a) (c, b) -> p (a, c) (b, c))
-> (p a b -> p (c, a) (c, b)) -> p a b -> p (a, c) (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 (c, a) (c, b)
forall a b c. p a b -> p (c, a) (c, b)
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' = ((c, a) -> (a, c))
-> ((b, c) -> (c, b)) -> p (a, c) (b, c) -> p (c, a) (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, a) -> (a, c)
forall a b. (a, b) -> (b, a)
swap (b, c) -> (c, b)
forall a b. (a, b) -> (b, a)
swap (p (a, c) (b, c) -> p (c, a) (c, b))
-> (p a b -> p (a, c) (b, c)) -> p a b -> p (c, a) (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 (a, c) (b, c)
forall a b c. p a b -> p (a, c) (b, 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' = ((b -> c, b) -> c) -> p (a, b) (b -> c, b) -> p (a, b) c
forall b c a. (b -> c) -> p a b -> p a c
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) (p (a, b) (b -> c, b) -> p (a, b) c)
-> (p a (b -> c) -> p (a, b) (b -> c, b))
-> p a (b -> c)
-> p (a, 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 -> c) -> p (a, b) (b -> c, b)
forall a b c. p a b -> p (a, c) (b, 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 = (a -> (a, a)) -> ((b, a) -> c) -> p (a, a) (b, a) -> p a 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
a -> (a
a, a
a)) (\(b
b, a
a) -> a -> b -> c
f a
a b
b) (p a b -> p (a, a) (b, a)
forall a b c. p a b -> p (a, c) (b, c)
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) = ((a, c) -> m (b, c)) -> Kleisli m (a, c) (b, c)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (((a, c) -> m (b, c)) -> Kleisli m (a, c) (b, c))
-> ((a, c) -> m (b, c)) -> Kleisli m (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ \ ~(a
a, c
c) -> do
     b
b <- a -> m b
f a
a
     (b, c) -> m (b, c)
forall a. a -> m 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) = ((c, a) -> m (c, b)) -> Kleisli m (c, a) (c, b)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (((c, a) -> m (c, b)) -> Kleisli m (c, a) (c, b))
-> ((c, a) -> m (c, b)) -> Kleisli m (c, a) (c, b)
forall a b. (a -> b) -> a -> b
$ \ ~(c
c, a
a) -> do
     b
b <- a -> m b
f a
a
     (c, b) -> m (c, b)
forall a. a -> m 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) = ((a, c) -> m (b, c)) -> Star m (a, c) (b, c)
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (((a, c) -> m (b, c)) -> Star m (a, c) (b, c))
-> ((a, c) -> m (b, c)) -> Star m (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ \ ~(a
a, c
c) -> (\b
b' -> (b
b', c
c)) (b -> (b, c)) -> m b -> m (b, 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) = ((c, a) -> m (c, b)) -> Star m (c, a) (c, b)
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (((c, a) -> m (c, b)) -> Star m (c, a) (c, b))
-> ((c, a) -> m (c, b)) -> Star m (c, a) (c, b)
forall a b. (a -> b) -> a -> b
$ \ ~(c
c, a
a) -> (,) c
c (b -> (c, b)) -> m b -> m (c, b)
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) = p (a, c) (b, c) -> WrappedArrow p (a, c) (b, c)
forall {k} {k1} (p :: k -> k1 -> *) (a :: k) (b :: k1).
p a b -> WrappedArrow p a b
WrapArrow (p a b -> p (a, c) (b, c)
forall b c d. p b c -> p (b, d) (c, d)
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) = p (c, a) (c, b) -> WrappedArrow p (c, a) (c, b)
forall {k} {k1} (p :: k -> k1 -> *) (a :: k) (b :: k1).
p a b -> WrappedArrow p a b
WrapArrow (p a b -> p (c, a) (c, b)
forall b c d. p b c -> p (d, b) (d, c)
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) = ((a, c) -> r) -> Forget r (a, c) (b, c)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (a -> r
k (a -> r) -> ((a, c) -> a) -> (a, c) -> 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, c) -> a
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) = ((c, a) -> r) -> Forget r (c, a) (c, b)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (a -> r
k (a -> r) -> ((c, a) -> a) -> (c, 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
. (c, a) -> a
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) = f (a, c) -> Clown f (a, c) (b, c)
forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown (((a, c) -> a) -> f a -> f (a, c)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (a, c) -> a
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) = f (c, a) -> Clown f (c, a) (c, b)
forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown (((c, a) -> a) -> f a -> f (c, a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (c, a) -> a
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) = p (a, c) (b, c) -> q (a, c) (b, c) -> Product p q (a, c) (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 (a, c) (b, c)
forall a b c. p a b -> p (a, c) (b, c)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p a b
p) (q a b -> q (a, c) (b, c)
forall a b c. q a b -> q (a, c) (b, c)
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) = p (c, a) (c, b) -> q (c, a) (c, b) -> Product p q (c, a) (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 (c, a) (c, b)
forall a b c. p a b -> p (c, a) (c, b)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' p a b
p) (q a b -> q (c, a) (c, b)
forall a b c. q a b -> q (c, a) (c, b)
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) = p (a, c) (b, c) -> Sum p q (a, c) (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 (a, c) (b, c)
forall a b c. p a b -> p (a, c) (b, c)
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) = q (a, c) (b, c) -> Sum p q (a, c) (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 (a, c) (b, c)
forall a b c. q a b -> q (a, c) (b, c)
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) = p (c, a) (c, b) -> Sum p q (c, a) (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 (c, a) (c, b)
forall a b c. p a b -> p (c, a) (c, b)
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) = q (c, a) (c, b) -> Sum p q (c, a) (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 (c, a) (c, b)
forall a b c. q a b -> q (c, a) (c, b)
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) = f (p (a, c) (b, c)) -> Tannen f p (a, c) (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 (a, c) (b, c)) -> f (p a b) -> f (p (a, c) (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 (a, c) (b, c)
forall a b c. p a b -> p (a, c) (b, c)
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) = f (p (c, a) (c, b)) -> Tannen f p (c, a) (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 (c, a) (c, b)) -> f (p a b) -> f (p (c, a) (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 (c, a) (c, b)
forall a b c. p a b -> p (c, a) (c, b)
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 c. p (a, c) (d, c)) -> Tambara p a d
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. p (a, c) (d, c)) -> Tambara p a d)
-> (forall c. p (a, c) (d, c)) -> Tambara p a d
forall a b. (a -> b) -> a -> b
$ ((a, c) -> (b, c))
-> ((c, c) -> (d, c)) -> p (b, c) (c, c) -> p (a, c) (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) -> (a, c) -> (b, c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a -> b
f) ((c -> d) -> (c, c) -> (d, c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first c -> d
g) p (b, c) (c, c)
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 c. q (a, c) (b, c)) -> Tambara q a b
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (p (a, c) (b, c) -> q (a, c) (b, c)
p :-> q
f p (a, c) (b, c)
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) = (a -> (a, ())) -> ((b, ()) -> b) -> p (a, ()) (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
a -> (a
a,())) (b, ()) -> b
forall a b. (a, b) -> a
fst p (a, ()) (b, ())
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 c. Tambara p (a, c) (b, c)) -> Tambara (Tambara p) a b
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. p ((a, c), c) ((b, c), c)) -> Tambara p (a, c) (b, c)
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. p ((a, c), c) ((b, c), c)) -> Tambara p (a, c) (b, c))
-> (forall c. p ((a, c), c) ((b, c), c)) -> Tambara p (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ (((a, c), c) -> (a, (c, c)))
-> ((b, (c, c)) -> ((b, c), c))
-> p (a, (c, c)) (b, (c, c))
-> p ((a, c), c) ((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 ((a, c), c) -> (a, (c, c))
forall a b c. ((a, b), c) -> (a, (b, c))
hither (b, (c, c)) -> ((b, c), c)
forall a b c. (a, (b, c)) -> ((a, b), c)
yon p (a, (c, c)) (b, (c, c))
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 = Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)
forall (p :: * -> * -> *) a b.
Tambara p a b -> forall c. p (a, c) (b, c)
runTambara (Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c))
-> Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ Tambara p a b -> Tambara (Tambara p) a b
Tambara p :-> Tambara (Tambara p)
forall (p :: * -> * -> *).
Profunctor p =>
Tambara p :-> Tambara (Tambara p)
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 c. p (a, c) (a, c)) -> Tambara p a a
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara p (a, c) (a, c)
forall a. p a a
forall c. p (a, c) (a, c)
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 c. p (a, c) (c, c)) -> Tambara p a c
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (p (b, c) (c, c)
forall c. p (b, c) (c, c)
p p (b, c) (c, c) -> p (a, c) (b, c) -> p (a, c) (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 (a, c) (b, 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 c. p (b, c) (c, c)) -> Tambara p b c
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. p (b, c) (c, c)) -> Tambara p b c)
-> (forall c. p (b, c) (c, c)) -> Tambara p b c
forall a b. (a -> b) -> a -> b
$ ((b, c) -> (c, c)) -> p (b, c) (c, c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((b, c) -> (c, c)) -> p (b, c) (c, c))
-> ((b, c) -> (c, c)) -> p (b, c) (c, c)
forall a b. (a -> b) -> a -> b
$ (b -> c) -> (b, c) -> (c, c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
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 c. p ((b, d), c) ((c, d), c)) -> Tambara p (b, d) (c, d)
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((((c, c), d) -> ((c, d), c)) -> p ((c, c), d) ((c, d), c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((c, c), d) -> ((c, d), c)
forall a b c. ((a, b), c) -> ((a, c), b)
go p ((c, c), d) ((c, d), c)
-> p ((b, d), c) ((c, c), d) -> p ((b, d), c) ((c, d), 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 (b, c) (c, c) -> p ((b, c), d) ((c, c), d)
forall b c d. p b c -> p (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first p (b, c) (c, c)
forall c. p (b, c) (c, c)
f p ((b, c), d) ((c, c), d)
-> p ((b, d), c) ((b, c), d) -> p ((b, d), c) ((c, c), d)
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
. (((b, d), c) -> ((b, c), d)) -> p ((b, d), c) ((b, c), d)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((b, d), c) -> ((b, c), d)
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 c. p (Either b d, c) (Either c d, c))
-> Tambara p (Either b d) (Either c d)
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((Either (c, c) (d, c) -> (Either c d, c))
-> p (Either (c, c) (d, c)) (Either c d, c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Either (c, c) (d, c) -> (Either c d, c)
forall a c b. Either (a, c) (b, c) -> (Either a b, c)
yon p (Either (c, c) (d, c)) (Either c d, c)
-> p (Either b d, c) (Either (c, c) (d, c))
-> p (Either b d, c) (Either c d, 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 (b, c) (c, c) -> p (Either (b, c) (d, c)) (Either (c, c) (d, 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 (b, c) (c, c)
forall c. p (b, c) (c, c)
f p (Either (b, c) (d, c)) (Either (c, c) (d, c))
-> p (Either b d, c) (Either (b, c) (d, c))
-> p (Either b d, c) (Either (c, c) (d, 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
. ((Either b d, c) -> Either (b, c) (d, c))
-> p (Either b d, c) (Either (b, c) (d, c))
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (Either b d, c) -> Either (b, c) (d, c)
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) = (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)

instance ArrowApply p => ArrowApply (Tambara p) where
  app :: forall b c. Tambara p (Tambara p b c, b) c
app = (forall c. p ((Tambara p b c, b), c) (c, c))
-> Tambara p (Tambara p b c, b) c
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. p ((Tambara p b c, b), c) (c, c))
 -> Tambara p (Tambara p b c, b) c)
-> (forall c. p ((Tambara p b c, b), c) (c, c))
-> Tambara p (Tambara p b c, b) c
forall a b. (a -> b) -> a -> b
$ p (p (b, c) (c, c), (b, c)) (c, c)
forall b c. p (p b c, b) c
forall (a :: * -> * -> *) b c. ArrowApply a => a (a b c, b) c
app p (p (b, c) (c, c), (b, c)) (c, c)
-> p ((Tambara p b c, b), c) (p (b, c) (c, c), (b, c))
-> p ((Tambara p b c, b), c) (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
. (((Tambara p b c, b), c) -> (p (b, c) (c, c), (b, c)))
-> p ((Tambara p b c, b), c) (p (b, c) (c, c), (b, c))
forall b c. (b -> c) -> p b 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) -> (p (b, c) (c, c)
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 c. p (b, c) (c, c)) -> Tambara p b c
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (p ((b, c), d) ((c, c), d) -> p (b, c) (c, c)
forall b d c. p (b, d) (c, d) -> p b c
forall (a :: * -> * -> *) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop ((((c, d), c) -> ((c, c), d)) -> p ((c, d), c) ((c, c), d)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((c, d), c) -> ((c, c), d)
forall a b c. ((a, b), c) -> ((a, c), b)
go p ((c, d), c) ((c, c), d)
-> p ((b, c), d) ((c, d), c) -> p ((b, c), d) ((c, c), d)
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 ((b, d), c) ((c, d), c)
forall c. p ((b, d), c) ((c, d), c)
f p ((b, d), c) ((c, d), c)
-> p ((b, c), d) ((b, d), c) -> p ((b, c), d) ((c, d), 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
. (((b, c), d) -> ((b, d), c)) -> p ((b, c), d) ((b, d), c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((b, c), d) -> ((b, d), c)
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 c. p (b, c) (c, c)) -> Tambara p b c
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara p (b, c) (c, c)
forall c. p (b, c) (c, c)
forall b c. p b c
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 c. p (b, c) (c, c)) -> Tambara p b c
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (p (b, c) (c, c)
forall c. p (b, c) (c, c)
f p (b, c) (c, c) -> p (b, c) (c, c) -> p (b, c) (c, c)
forall b c. p b c -> p b c -> p b c
forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> p (b, c) (c, 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 = (a -> b) -> Tambara p a a -> Tambara p a b
forall b c a. (b -> c) -> Tambara p a b -> Tambara p a c
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 = (a -> a) -> Tambara p a a
forall b c. (b -> c) -> Tambara p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (a -> a -> a
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 = ((a -> b, a) -> b) -> Tambara p (a -> b, a) b
forall b c. (b -> c) -> Tambara p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((a -> b) -> a -> b) -> (a -> b, a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> b) -> a -> b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) Tambara p (a -> b, a) b -> Tambara p a (a -> b, a) -> Tambara p a b
forall b c a. Tambara p b c -> Tambara p a b -> Tambara 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
. (Tambara p a (a -> b)
f Tambara p a (a -> b) -> Tambara p a a -> Tambara p a (a -> b, a)
forall b c c'.
Tambara p b c -> Tambara p b c' -> Tambara p b (c, c')
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 = Tambara p a a
forall b c. Tambara p b c
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 Tambara p a a -> Tambara p a a -> Tambara p a a
forall b c. Tambara p b c -> Tambara p b c -> Tambara p b c
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 Tambara p a b -> Tambara p a b -> Tambara p a b
forall b c. Tambara p b c -> Tambara p b c -> Tambara p b c
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 = Tambara p a b
forall b c. Tambara p b c
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 c. q (a, c) (b, c)) -> Tambara q a b
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara ((forall c. q (a, c) (b, c)) -> Tambara q a b)
-> (forall c. q (a, c) (b, c)) -> Tambara q a b
forall a b. (a -> b) -> a -> b
$ p (a, c) (b, c) -> q (a, c) (b, c)
p :-> q
f (p (a, c) (b, c) -> q (a, c) (b, c))
-> p (a, c) (b, c) -> q (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ p a b -> p (a, c) (b, c)
forall a b c. p a b -> p (a, c) (b, c)
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 = (a -> (a, ())) -> ((b, ()) -> b) -> q (a, ()) (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
a -> (a
a,())) (b, ()) -> b
forall a b. (a, b) -> a
fst (q (a, ()) (b, ()) -> q a b) -> q (a, ()) (b, ()) -> q a b
forall a b. (a -> b) -> a -> b
$ Tambara q a b -> forall c. q (a, c) (b, c)
forall (p :: * -> * -> *) a b.
Tambara p a b -> forall c. p (a, c) (b, c)
runTambara (Tambara q a b -> forall c. q (a, c) (b, c))
-> Tambara q a b -> forall c. q (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ p a b -> Tambara q 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) = ((y, z) -> b) -> p x y -> (a -> (x, z)) -> Pastro p a b
forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (a -> b
f (a -> b) -> ((y, z) -> a) -> (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
. (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) = ((y, z) -> d) -> p x y -> (a -> (x, z)) -> Pastro p a d
forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (c -> d
g (c -> d) -> ((y, z) -> c) -> (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
. (y, z) -> c
l) p x y
m (b -> (x, z)
r (b -> (x, z)) -> (a -> b) -> a -> (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) -> 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) = ((y, z) -> c) -> p x y -> (a -> (x, z)) -> Pastro p a c
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 (b -> (x, z)) -> (a -> b) -> a -> (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) -> 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) = ((y, z) -> c) -> p x y -> (a -> (x, z)) -> Pastro p a c
forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (b -> c
g (b -> c) -> ((y, z) -> b) -> (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
. (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 = ((y, z) -> c) -> p x y -> (a -> (x, z)) -> Pastro p a c
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 q b c -> ((y, z) -> b) -> (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
#. (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 = ((y, z) -> c) -> p x y -> (a -> (x, z)) -> Pastro p a c
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 (b -> (x, z)) -> q a b -> a -> (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 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) = ((y, z) -> b) -> q x y -> (a -> (x, z)) -> Pastro q a b
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 x y -> q x y
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 = ((b, ()) -> b) -> p a b -> (a -> (a, ())) -> Pastro p a b
forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (b, ()) -> b
forall a b. (a, b) -> a
fst p a b
p ((a -> (a, ())) -> Pastro p a b) -> (a -> (a, ())) -> Pastro p a b
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) = ((y, (z, z)) -> b) -> p x y -> (a -> (x, (z, z))) -> Pastro p a b
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) = (a -> (x, z)) -> ((y, z) -> b) -> p (x, z) (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 -> (x, z)
f (y, z) -> b
g p (x, z) (y, z)
forall c. p (x, c) (y, c)
p
  unit :: forall (p :: * -> * -> *). Profunctor p => p :-> Tambara (Pastro p)
unit p a b
p = (forall c. Pastro p (a, c) (b, c)) -> Tambara (Pastro p) a b
forall (p :: * -> * -> *) a b.
(forall c. p (a, c) (b, c)) -> Tambara p a b
Tambara (((b, c) -> (b, c))
-> p a b -> ((a, c) -> (a, c)) -> Pastro p (a, c) (b, c)
forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (b, c) -> (b, c)
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id p a b
p (a, c) -> (a, c)
forall a. a -> a
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) = ((y, (z, c)) -> (b, c))
-> p x y -> ((a, c) -> (x, (z, c))) -> Pastro p (a, c) (b, c)
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) = ((y, (c, z)) -> (c, b))
-> p x y -> ((c, a) -> (x, (c, z))) -> Pastro p (c, a) (c, b)
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) = (a -> (x, z)) -> ((y, z) -> b) -> q (x, z) (y, z) -> 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 -> (x, z)
l (y, z) -> b
r (q x y -> q (x, z) (y, z)
forall a b c. q a b -> q (a, c) (b, c)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' (p x y -> q x y
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 a b -> q a b
Pastro p :-> q
f (((b, ()) -> b) -> p a b -> (a -> (a, ())) -> Pastro p a b
forall r z b (p :: * -> * -> *) x a.
((r, z) -> b) -> p x r -> (a -> (x, z)) -> Pastro p a b
Pastro (b, ()) -> b
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 = p (d, a) (d, b) -> p a b
forall d a b. p (d, a) (d, b) -> p a b
forall (p :: * -> * -> *) d a b.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond (p (d, a) (d, b) -> p a b)
-> (p (a, d) (b, d) -> p (d, a) (d, b)) -> p (a, d) (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
. ((d, a) -> (a, d))
-> ((b, d) -> (d, b)) -> p (a, d) (b, d) -> p (d, a) (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, a) -> (a, d)
forall a b. (a, b) -> (b, a)
swap (b, d) -> (d, b)
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 = p (a, d) (b, d) -> p a b
forall a d b. p (a, d) (b, d) -> p a b
forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst (p (a, d) (b, d) -> p a b)
-> (p (d, a) (d, b) -> p (a, d) (b, d)) -> p (d, a) (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
. ((a, d) -> (d, a))
-> ((d, b) -> (b, d)) -> p (d, a) (d, b) -> p (a, d) (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, d) -> (d, a)
forall a b. (a, b) -> (b, a)
swap (d, b) -> (b, d)
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) = (f a -> b) -> Costar f a b
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)) (a -> (a, d)) -> f a -> f (a, 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) = (f a -> b) -> Costar f a b
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 (a -> (d, a)) -> f a -> f (d, a)
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) = b -> Tagged a b
forall {k} (s :: k) b. b -> Tagged s b
Tagged ((b, d) -> b
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) = b -> Tagged a b
forall {k} (s :: k) b. b -> Tagged s b
Tagged ((d, b) -> b
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) = p a b -> WrappedArrow p a b
forall {k} {k1} (p :: k -> k1 -> *) (a :: k) (b :: k1).
p a b -> WrappedArrow p a b
WrapArrow (p (a, d) (b, d) -> p a b
forall b d c. p (b, d) (c, d) -> p b c
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) = (a -> m b) -> Kleisli m a b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (((b, d) -> b) -> m (b, d) -> m b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (b, d) -> b
forall a b. (a, b) -> a
fst (m (b, d) -> m b) -> (a -> m (b, d)) -> a -> m 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
. ((b, d) -> m (b, d)) -> m (b, d)
forall a. (a -> m a) -> m a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (((b, d) -> m (b, d)) -> m (b, d))
-> (a -> (b, d) -> m (b, d)) -> a -> m (b, 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
. 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, (b, d) -> d
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) = (f a -> b) -> Cokleisli f a b
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)) (a -> (a, d)) -> f a -> f (a, 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) = 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 (a, d) (b, d) -> p a b) -> f (p (a, d) (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 (a, d) (b, d) -> p a b
forall a d b. p (a, d) (b, d) -> p a b
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) = 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 (d, a) (d, b) -> p a b) -> f (p (d, a) (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 (d, a) (d, b) -> p a b
forall d a b. p (d, a) (d, b) -> p a b
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) = 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 (a, d) (b, d) -> p a b
forall a d b. p (a, d) (b, d) -> p a b
forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst p (a, d) (b, d)
p) (q (a, d) (b, d) -> q a b
forall a d b. q (a, d) (b, d) -> q a b
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) = 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 (d, a) (d, b) -> p a b
forall d a b. p (d, a) (d, b) -> p a b
forall (p :: * -> * -> *) d a b.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond p (d, a) (d, b)
p) (q (d, a) (d, b) -> q a b
forall d a b. q (d, a) (d, b) -> q a b
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) = 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 (a, d) (b, d) -> p a b
forall a d b. p (a, d) (b, d) -> p a b
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) = 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 (a, d) (b, d) -> q a b
forall a d b. q (a, d) (b, d) -> q a b
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) = 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 (d, a) (d, b) -> p a b
forall d a b. p (d, a) (d, b) -> p a b
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) = 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 (d, a) (d, b) -> q a b
forall d a b. q (d, a) (d, b) -> q a b
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) = (r :-> p) -> r a c -> Cotambara p a c
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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) -> Cotambara p a b -> Cotambara p a c
rmap b -> c
g (Cotambara r :-> p
n r a b
p) = (r :-> p) -> r a c -> Cotambara p a c
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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) -> Cotambara p b c -> Cotambara p a d
dimap a -> b
f c -> d
g (Cotambara r :-> p
n r b c
p) = (r :-> p) -> r a d -> Cotambara p a d
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara 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 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) = (r :-> q) -> r a b -> Cotambara q a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara (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 Cotambara where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Cotambara p :-> p
proextract (Cotambara 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 =>
Cotambara p :-> Cotambara (Cotambara p)
produplicate (Cotambara r :-> p
n r a b
p) = (Cotambara p :-> Cotambara p)
-> Cotambara p a b -> Cotambara (Cotambara p) a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara Cotambara p a b -> Cotambara p a b
forall a. a -> a
Cotambara p :-> Cotambara p
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id ((r :-> p) -> r a b -> Cotambara p a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara r a b -> p a b
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) = (r :-> p) -> r a b -> Cotambara p a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara r a b -> p a b
r :-> p
n (r (a, d) (b, d) -> r a b
forall a d b. r (a, d) (b, d) -> r a b
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 = (a -> b) -> Cotambara p a a -> Cotambara p a b
forall b c a. (b -> c) -> Cotambara p a b -> Cotambara p a c
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 = (p :-> q) -> p a b -> Cotambara q a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara p a b -> q a b
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 = Cotambara q a b -> q a b
Cotambara q :-> q
forall (p :: * -> * -> *). Profunctor p => Cotambara p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract (p a b -> Cotambara q a b
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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> Copastro p a b)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a b)
-> Copastro 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 :: * -> * -> *).
Costrong 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 (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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a d)
-> Copastro p a d
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a d)
 -> Copastro p a d)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a d)
-> Copastro 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 :: * -> * -> *).
Costrong 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) -> 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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a c)
-> Copastro p a c
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a c)
 -> Copastro p a c)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a c)
-> Copastro 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 :: * -> * -> *).
Costrong 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) -> 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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a c)
-> Copastro p a c
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a c)
 -> Copastro p a c)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a c)
-> Copastro 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 :: * -> * -> *).
Costrong 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 Copastro Cotambara where
 unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> Cotambara (Copastro p)
unit p a b
p = (Copastro p :-> Copastro p)
-> Copastro p a b -> Cotambara (Copastro p) a b
forall (r :: * -> * -> *) (q :: * -> * -> *) a b.
Costrong r =>
(r :-> q) -> r a b -> Cotambara q a b
Cotambara Copastro p a b -> Copastro p a b
forall a. a -> a
Copastro p :-> Copastro p
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (p a b -> Copastro p a b
p :-> Copastro p
forall (p :: * -> * -> *). Profunctor p => p :-> Copastro p
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) = Cotambara p a b -> p a b
Cotambara p :-> p
forall (p :: * -> * -> *). Profunctor p => Cotambara p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract ((forall x y. Cotambara p x y -> Cotambara p x y) -> Cotambara p a b
forall (r :: * -> * -> *).
Costrong r =>
(forall x y. Cotambara p x y -> r x y) -> r a b
h Cotambara p x y -> Cotambara p x y
forall a. a -> a
forall x y. Cotambara p x y -> Cotambara p x y
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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. q x y -> r x y) -> r a b)
-> Copastro q a b
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. q x y -> r x y) -> r a b)
 -> Copastro q a b)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. q x y -> r x y) -> r a b)
-> Copastro 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 :: * -> * -> *).
Costrong 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 Copastro where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Copastro p
proreturn p a b
p = (forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> Copastro p a b)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a b)
-> Copastro 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 =>
Copastro (Copastro p) :-> Copastro p
projoin Copastro (Copastro p) a b
p = (forall (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> Copastro p a b)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
c -> Copastro (Copastro p) a b
-> forall (r :: * -> * -> *).
   Costrong r =>
   (forall x y. Copastro p x y -> r x y) -> r a b
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 -> Copastro p x y
-> forall (r :: * -> * -> *).
   Costrong r =>
   (forall x y. p x y -> r x y) -> r x y
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 p x y -> r x y
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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> Copastro p a b)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> r (a, d) (b, d) -> r a b
forall a d b. r (a, d) (b, d) -> r a b
forall (p :: * -> * -> *) a d b.
Costrong p =>
p (a, d) (b, d) -> p a b
unfirst ((forall x y. p x y -> r x y) -> r (a, d) (b, d)
forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r (a, d) (b, d)
p p x y -> r x y
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 (r :: * -> * -> *).
 Costrong r =>
 (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
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 (r :: * -> * -> *).
  Costrong r =>
  (forall x y. p x y -> r x y) -> r a b)
 -> Copastro p a b)
-> (forall (r :: * -> * -> *).
    Costrong r =>
    (forall x y. p x y -> r x y) -> r a b)
-> Copastro p a b
forall a b. (a -> b) -> a -> b
$ \forall x y. p x y -> r x y
n -> r (d, a) (d, b) -> r a b
forall d a b. r (d, a) (d, b) -> r a b
forall (p :: * -> * -> *) d a b.
Costrong p =>
p (d, a) (d, b) -> p a b
unsecond ((forall x y. p x y -> r x y) -> r (d, a) (d, b)
forall (r :: * -> * -> *).
Costrong r =>
(forall x y. p x y -> r x y) -> r (d, a) (d, b)
p p x y -> r x y
forall x y. p x y -> r x y
n)