{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Safe #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Profunctor.Composition
-- Copyright   :  (C) 2014-2015 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  GADTs, TFs, MPTCs, RankN
--
----------------------------------------------------------------------------
module Data.Profunctor.Composition
  (
  -- * Profunctor Composition
    Procompose(..)
  , procomposed
  -- * Unitors and Associator
  , idl
  , idr
  , assoc
  -- * Categories as monoid objects
  , eta
  , mu
  -- * Generalized Composition
  , stars, kleislis
  , costars, cokleislis
  -- * Right Kan Lift
  , Rift(..)
  , decomposeRift
  ) where

import Control.Arrow
import Control.Category
import Control.Comonad
import Control.Monad (liftM)
import Data.Functor.Compose
import Data.Profunctor
import Data.Profunctor.Adjunction
import Data.Profunctor.Monad
import Data.Profunctor.Rep
import Data.Profunctor.Sieve
import Data.Profunctor.Traversing
import Data.Profunctor.Unsafe
import Prelude hiding ((.),id)

type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)

-- * Profunctor Composition

-- | @'Procompose' p q@ is the 'Profunctor' composition of the
-- 'Profunctor's @p@ and @q@.
--
-- For a good explanation of 'Profunctor' composition in Haskell
-- see Dan Piponi's article:
--
-- <http://blog.sigfpe.com/2011/07/profunctors-in-haskell.html>
--
-- 'Procompose' has a polymorphic kind since @5.6@.

-- Procompose :: (k1 -> k2 -> Type) -> (k3 -> k1 -> Type) -> (k3 -> k2 -> Type)
data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

instance ProfunctorFunctor (Procompose p) where
  promap :: (p :-> q) -> Procompose p p :-> Procompose p q
promap p :-> q
f (Procompose p x b
p p a x
q) = p x b -> q a x -> Procompose p q a b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose p x b
p (p a x -> q a x
p :-> q
f p a x
q)

instance Category p => ProfunctorMonad (Procompose p) where
  proreturn :: p :-> Procompose p p
proreturn = p b b -> p a b -> Procompose p p a b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose p b b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  projoin :: Procompose p (Procompose p p) :-> Procompose p p
projoin (Procompose p x b
p (Procompose p x x
q p a x
r)) = p x b -> p a x -> Procompose p p a b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b
p p x b -> p x x -> p x b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p x x
q) p a x
r

procomposed :: Category p => Procompose p p a b -> p a b
procomposed :: Procompose p p a b -> p a b
procomposed (Procompose p x b
pxc p a x
pdx) = p x b
pxc p x b -> p a x -> p a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p a x
pdx
{-# INLINE procomposed #-}

instance (Profunctor p, Profunctor q) => Profunctor (Procompose p q) where
  dimap :: (a -> b) -> (c -> d) -> Procompose p q b c -> Procompose p q a d
dimap a -> b
l c -> d
r (Procompose p x c
f q b x
g) = p x d -> q a x -> Procompose p q a d
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((c -> d) -> p x c -> p x d
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
r p x c
f) ((a -> b) -> q b x -> q a x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
l q b x
g)
  {-# INLINE dimap #-}
  lmap :: (a -> b) -> Procompose p q b c -> Procompose p q a c
lmap a -> b
k (Procompose p x c
f q b x
g) = p x c -> q a x -> Procompose p q a c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose p x c
f ((a -> b) -> q b x -> q a x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
k q b x
g)
  {-# INLINE rmap #-}
  rmap :: (b -> c) -> Procompose p q a b -> Procompose p q a c
rmap b -> c
k (Procompose p x b
f q a x
g) = p x c -> q a x -> Procompose p q a c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((b -> c) -> p x b -> p x c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
k p x b
f) q a x
g
  {-# INLINE lmap #-}
  q b c
k #. :: q b c -> Procompose p q a b -> Procompose p q a c
#. Procompose p x b
f q a x
g     = p x c -> q a x -> Procompose p q a c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (q b c
k q b c -> p x b -> p x c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. p x b
f) q a x
g
  {-# INLINE (#.) #-}
  Procompose p x c
f q b x
g .# :: Procompose p q b c -> q a b -> Procompose p q a c
.# q a b
k     = p x c -> q a x -> Procompose p q a c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose p x c
f (q b x
g q b x -> q a b -> q a x
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# q a b
k)
  {-# INLINE (.#) #-}

instance Profunctor p => Functor (Procompose p q a) where
  fmap :: (a -> b) -> Procompose p q a a -> Procompose p q a b
fmap a -> b
k (Procompose p x a
f q a x
g) = p x b -> q a x -> Procompose p q a b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((a -> b) -> p x a -> p x b
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
k p x a
f) q a x
g
  {-# INLINE fmap #-}

instance (Sieve p f, Sieve q g) => Sieve (Procompose p q) (Compose g f) where
  sieve :: Procompose p q a b -> a -> Compose g f b
sieve (Procompose p x b
g q a x
f) a
d = g (f b) -> Compose g f b
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (g (f b) -> Compose g f b) -> g (f b) -> Compose g f b
forall a b. (a -> b) -> a -> b
$ p x b -> x -> f b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p x b
g (x -> f b) -> g x -> g (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> q a x -> a -> g x
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve q a x
f a
d
  {-# INLINE sieve #-}

-- | The composition of two 'Representable' 'Profunctor's is 'Representable' by
-- the composition of their representations.
instance (Representable p, Representable q) => Representable (Procompose p q) where
  type Rep (Procompose p q) = Compose (Rep q) (Rep p)
  tabulate :: (d -> Rep (Procompose p q) c) -> Procompose p q d c
tabulate d -> Rep (Procompose p q) c
f = p (Rep p c) c -> q d (Rep p c) -> Procompose p q d c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((Rep p c -> Rep p c) -> p (Rep p c) c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate Rep p c -> Rep p c
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) ((d -> Rep q (Rep p c)) -> q d (Rep p c)
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate (Compose (Rep q) (Rep p) c -> Rep q (Rep p c)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Rep q) (Rep p) c -> Rep q (Rep p c))
-> (d -> Compose (Rep q) (Rep p) c) -> d -> Rep q (Rep p c)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Compose (Rep q) (Rep p) c
d -> Rep (Procompose p q) c
f))
  {-# INLINE tabulate #-}

instance (Cosieve p f, Cosieve q g) => Cosieve (Procompose p q) (Compose f g) where
  cosieve :: Procompose p q a b -> Compose f g a -> b
cosieve (Procompose p x b
g q a x
f) (Compose f (g a)
d) = p x b -> f x -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve p x b
g (f x -> b) -> f x -> b
forall a b. (a -> b) -> a -> b
$ q a x -> g a -> x
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve q a x
f (g a -> x) -> f (g a) -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (g a)
d
  {-# INLINE cosieve #-}

instance (Corepresentable p, Corepresentable q) => Corepresentable (Procompose p q) where
  type Corep (Procompose p q) = Compose (Corep p) (Corep q)
  cotabulate :: (Corep (Procompose p q) d -> c) -> Procompose p q d c
cotabulate Corep (Procompose p q) d -> c
f = p (Corep q d) c -> q d (Corep q d) -> Procompose p q d c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((Corep p (Corep q d) -> c) -> p (Corep q d) c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate (Compose (Corep p) (Corep q) d -> c
Corep (Procompose p q) d -> c
f (Compose (Corep p) (Corep q) d -> c)
-> (Corep p (Corep q d) -> Compose (Corep p) (Corep q) d)
-> Corep p (Corep q d)
-> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Corep p (Corep q d) -> Compose (Corep p) (Corep q) d
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)) ((Corep q d -> Corep q d) -> q d (Corep q d)
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate Corep q d -> Corep q d
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  {-# INLINE cotabulate #-}

instance (Strong p, Strong q) => Strong (Procompose p q) where
  first' :: Procompose p q a b -> Procompose p q (a, c) (b, c)
first' (Procompose p x b
x q a x
y) = p (x, c) (b, c) -> q (a, c) (x, c) -> Procompose p q (a, c) (b, c)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (x, c) (b, c)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p x b
x) (q a x -> q (a, c) (x, c)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' q a x
y)
  {-# INLINE first' #-}
  second' :: Procompose p q a b -> Procompose p q (c, a) (c, b)
second' (Procompose p x b
x q a x
y) = p (c, x) (c, b) -> q (c, a) (c, x) -> Procompose p q (c, a) (c, b)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (c, x) (c, b)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' p x b
x) (q a x -> q (c, a) (c, x)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' q a x
y)
  {-# INLINE second' #-}

instance (Choice p, Choice q) => Choice (Procompose p q) where
  left' :: Procompose p q a b -> Procompose p q (Either a c) (Either b c)
left' (Procompose p x b
x q a x
y) = p (Either x c) (Either b c)
-> q (Either a c) (Either x c)
-> Procompose p q (Either a c) (Either b c)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (Either x c) (Either b c)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p x b
x) (q a x -> q (Either a c) (Either x c)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' q a x
y)
  {-# INLINE left' #-}
  right' :: Procompose p q a b -> Procompose p q (Either c a) (Either c b)
right' (Procompose p x b
x q a x
y) = p (Either c x) (Either c b)
-> q (Either c a) (Either c x)
-> Procompose p q (Either c a) (Either c b)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (Either c x) (Either c b)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' p x b
x) (q a x -> q (Either c a) (Either c x)
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' q a x
y)
  {-# INLINE right' #-}

instance (Closed p, Closed q) => Closed (Procompose p q) where
  closed :: Procompose p q a b -> Procompose p q (x -> a) (x -> b)
closed (Procompose p x b
x q a x
y) = p (x -> x) (x -> b)
-> q (x -> a) (x -> x) -> Procompose p q (x -> a) (x -> b)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (x -> x) (x -> b)
forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed p x b
x) (q a x -> q (x -> a) (x -> x)
forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed q a x
y)
  {-# INLINE closed #-}

instance (Traversing p, Traversing q) => Traversing (Procompose p q) where
  traverse' :: Procompose p q a b -> Procompose p q (f a) (f b)
traverse' (Procompose p x b
p q a x
q) = p (f x) (f b) -> q (f a) (f x) -> Procompose p q (f a) (f b)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (f x) (f b)
forall (p :: * -> * -> *) (f :: * -> *) a b.
(Traversing p, Traversable f) =>
p a b -> p (f a) (f b)
traverse' p x b
p) (q a x -> q (f a) (f x)
forall (p :: * -> * -> *) (f :: * -> *) a b.
(Traversing p, Traversable f) =>
p a b -> p (f a) (f b)
traverse' q a x
q)
  {-# INLINE traverse' #-}

instance (Mapping p, Mapping q) => Mapping (Procompose p q) where
  map' :: Procompose p q a b -> Procompose p q (f a) (f b)
map' (Procompose p x b
p q a x
q) = p (f x) (f b) -> q (f a) (f x) -> Procompose p q (f a) (f b)
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (f x) (f b)
forall (p :: * -> * -> *) (f :: * -> *) a b.
(Mapping p, Functor f) =>
p a b -> p (f a) (f b)
map' p x b
p) (q a x -> q (f a) (f x)
forall (p :: * -> * -> *) (f :: * -> *) a b.
(Mapping p, Functor f) =>
p a b -> p (f a) (f b)
map' q a x
q)
  {-# INLINE map' #-}

instance (Corepresentable p, Corepresentable q) => Costrong (Procompose p q) where
  unfirst :: Procompose p q (a, d) (b, d) -> Procompose p q a b
unfirst = Procompose p q (a, d) (b, d) -> Procompose p q a b
forall (p :: * -> * -> *) a d b.
Corepresentable p =>
p (a, d) (b, d) -> p a b
unfirstCorep
  {-# INLINE unfirst #-}
  unsecond :: Procompose p q (d, a) (d, b) -> Procompose p q a b
unsecond = Procompose p q (d, a) (d, b) -> Procompose p q a b
forall (p :: * -> * -> *) d a b.
Corepresentable p =>
p (d, a) (d, b) -> p a b
unsecondCorep
  {-# INLINE unsecond #-}

-- * Lax identity

-- | @(->)@ functions as a lax identity for 'Profunctor' composition.
--
-- This provides an 'Iso' for the @lens@ package that witnesses the
-- isomorphism between @'Procompose' (->) q d c@ and @q d c@, which
-- is the left identity law.
--
-- @
-- 'idl' :: 'Profunctor' q => Iso' ('Procompose' (->) q d c) (q d c)
-- @
idl :: Profunctor q => Iso (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
idl :: Iso
  (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
idl = (Procompose (->) q d c -> q d c)
-> (f (r d' c') -> f (Procompose (->) r d' c'))
-> p (q d c) (f (r d' c'))
-> p (Procompose (->) q d c) (f (Procompose (->) r d' c'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\(Procompose x -> c
g q d x
f) -> (x -> c) -> q d x -> q d c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap x -> c
g q d x
f) ((r d' c' -> Procompose (->) r d' c')
-> f (r d' c') -> f (Procompose (->) r d' c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((c' -> c') -> r d' c' -> Procompose (->) r d' c'
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose c' -> c'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id))

-- | @(->)@ functions as a lax identity for 'Profunctor' composition.
--
-- This provides an 'Iso' for the @lens@ package that witnesses the
-- isomorphism between @'Procompose' q (->) d c@ and @q d c@, which
-- is the right identity law.
--
-- @
-- 'idr' :: 'Profunctor' q => Iso' ('Procompose' q (->) d c) (q d c)
-- @
idr :: Profunctor q => Iso (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c')
idr :: Iso
  (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c')
idr = (Procompose q (->) d c -> q d c)
-> (f (r d' c') -> f (Procompose r (->) d' c'))
-> p (q d c) (f (r d' c'))
-> p (Procompose q (->) d c) (f (Procompose r (->) d' c'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\(Procompose q x c
g d -> x
f) -> (d -> x) -> q x c -> q d c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap d -> x
f q x c
g) ((r d' c' -> Procompose r (->) d' c')
-> f (r d' c') -> f (Procompose r (->) d' c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (r d' c' -> (d' -> d') -> Procompose r (->) d' c'
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
`Procompose` d' -> d'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id))


-- | The associator for 'Profunctor' composition.
--
-- This provides an 'Iso' for the @lens@ package that witnesses the
-- isomorphism between @'Procompose' p ('Procompose' q r) a b@ and
-- @'Procompose' ('Procompose' p q) r a b@, which arises because
-- @Prof@ is only a bicategory, rather than a strict 2-category.
assoc :: Iso (Procompose p (Procompose q r) a b) (Procompose x (Procompose y z) a b)
             (Procompose (Procompose p q) r a b) (Procompose (Procompose x y) z a b)
assoc :: p (Procompose (Procompose p q) r a b)
  (f (Procompose (Procompose x y) z a b))
-> p (Procompose p (Procompose q r) a b)
     (f (Procompose x (Procompose y z) a b))
assoc = (Procompose p (Procompose q r) a b
 -> Procompose (Procompose p q) r a b)
-> (f (Procompose (Procompose x y) z a b)
    -> f (Procompose x (Procompose y z) a b))
-> p (Procompose (Procompose p q) r a b)
     (f (Procompose (Procompose x y) z a b))
-> p (Procompose p (Procompose q r) a b)
     (f (Procompose x (Procompose y z) a b))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\(Procompose p x b
f (Procompose g h)) -> Procompose p q x b -> r a x -> Procompose (Procompose p q) r a b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> q x x -> Procompose p q x b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose p x b
f q x x
g) r a x
h)
              ((Procompose (Procompose x y) z a b
 -> Procompose x (Procompose y z) a b)
-> f (Procompose (Procompose x y) z a b)
-> f (Procompose x (Procompose y z) a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Procompose (Procompose f g) z a x
h) -> x x b -> Procompose y z a x -> Procompose x (Procompose y z) a b
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose x x b
f (y x x -> z a x -> Procompose y z a x
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose y x x
g z a x
h)))

-- | 'Profunctor' composition generalizes 'Functor' composition in two ways.
--
-- This is the first, which shows that @exists b. (a -> f b, b -> g c)@ is
-- isomorphic to @a -> f (g c)@.
--
-- @'stars' :: 'Functor' f => Iso' ('Procompose' ('Star' f) ('Star' g) d c) ('Star' ('Compose' f g) d c)@
stars :: Functor g
        => Iso (Procompose (Star f ) (Star g ) d  c )
               (Procompose (Star f') (Star g') d' c')
               (Star (Compose g  f ) d  c )
               (Star (Compose g' f') d' c')
stars :: Iso
  (Procompose (Star f) (Star g) d c)
  (Procompose (Star f') (Star g') d' c')
  (Star (Compose g f) d c)
  (Star (Compose g' f') d' c')
stars = (Procompose (Star f) (Star g) d c -> Star (Compose g f) d c)
-> (f (Star (Compose g' f') d' c')
    -> f (Procompose (Star f') (Star g') d' c'))
-> p (Star (Compose g f) d c) (f (Star (Compose g' f') d' c'))
-> p (Procompose (Star f) (Star g) d c)
     (f (Procompose (Star f') (Star g') d' c'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Procompose (Star f) (Star g) d c -> Star (Compose g f) d c
forall k (f :: * -> *) (g :: k -> *) d (c :: k).
Functor f =>
Procompose (Star g) (Star f) d c -> Star (Compose f g) d c
hither ((Star (Compose g' f') d' c'
 -> Procompose (Star f') (Star g') d' c')
-> f (Star (Compose g' f') d' c')
-> f (Procompose (Star f') (Star g') d' c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Star (Compose g' f') d' c' -> Procompose (Star f') (Star g') d' c'
forall k (f :: * -> *) (f :: k -> *) d (c :: k).
Star (Compose f f) d c -> Procompose (Star f) (Star f) d c
yon) where
  hither :: Procompose (Star g) (Star f) d c -> Star (Compose f g) d c
hither (Procompose (Star xgc) (Star dfx)) = (d -> Compose f g c) -> Star (Compose f g) d c
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (f (g c) -> Compose f g c
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g c) -> Compose f g c) -> (d -> f (g c)) -> d -> Compose f g c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (x -> g c) -> f x -> f (g c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> g c
xgc (f x -> f (g c)) -> (d -> f x) -> d -> f (g c)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> f x
dfx)
  yon :: Star (Compose f f) d c -> Procompose (Star f) (Star f) d c
yon (Star d -> Compose f f c
dfgc) = Star f (f c) c
-> Star f d (f c) -> Procompose (Star f) (Star f) d c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((f c -> f c) -> Star f (f c) c
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star f c -> f c
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) ((d -> f (f c)) -> Star f d (f c)
forall k (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (Compose f f c -> f (f c)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f f c -> f (f c)) -> (d -> Compose f f c) -> d -> f (f c)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Compose f f c
dfgc))

-- | 'Profunctor' composition generalizes 'Functor' composition in two ways.
--
-- This is the second, which shows that @exists b. (f a -> b, g b -> c)@ is
-- isomorphic to @g (f a) -> c@.
--
-- @'costars' :: 'Functor' f => Iso' ('Procompose' ('Costar' f) ('Costar' g) d c) ('Costar' ('Compose' g f) d c)@
costars :: Functor f
          => Iso (Procompose (Costar f ) (Costar g ) d  c )
                 (Procompose (Costar f') (Costar g') d' c')
                 (Costar (Compose f  g ) d  c )
                 (Costar (Compose f' g') d' c')
costars :: Iso
  (Procompose (Costar f) (Costar g) d c)
  (Procompose (Costar f') (Costar g') d' c')
  (Costar (Compose f g) d c)
  (Costar (Compose f' g') d' c')
costars = (Procompose (Costar f) (Costar g) d c -> Costar (Compose f g) d c)
-> (f (Costar (Compose f' g') d' c')
    -> f (Procompose (Costar f') (Costar g') d' c'))
-> p (Costar (Compose f g) d c) (f (Costar (Compose f' g') d' c'))
-> p (Procompose (Costar f) (Costar g) d c)
     (f (Procompose (Costar f') (Costar g') d' c'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Procompose (Costar f) (Costar g) d c -> Costar (Compose f g) d c
forall k (f :: * -> *) (f :: k -> *) (d :: k) c.
Functor f =>
Procompose (Costar f) (Costar f) d c -> Costar (Compose f f) d c
hither ((Costar (Compose f' g') d' c'
 -> Procompose (Costar f') (Costar g') d' c')
-> f (Costar (Compose f' g') d' c')
-> f (Procompose (Costar f') (Costar g') d' c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Costar (Compose f' g') d' c'
-> Procompose (Costar f') (Costar g') d' c'
forall k (f :: * -> *) (f :: k -> *) (d :: k) c.
Costar (Compose f f) d c -> Procompose (Costar f) (Costar f) d c
yon) where
  hither :: Procompose (Costar f) (Costar f) d c -> Costar (Compose f f) d c
hither (Procompose (Costar gxc) (Costar fdx)) = (Compose f f d -> c) -> Costar (Compose f f) d c
forall k (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar (f x -> c
gxc (f x -> c) -> (Compose f f d -> f x) -> Compose f f d -> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f d -> x) -> f (f d) -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f d -> x
fdx (f (f d) -> f x)
-> (Compose f f d -> f (f d)) -> Compose f f d -> f x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose f f d -> f (f d)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
  yon :: Costar (Compose f f) d c -> Procompose (Costar f) (Costar f) d c
yon (Costar Compose f f d -> c
dgfc) = Costar f (f d) c
-> Costar f d (f d) -> Procompose (Costar f) (Costar f) d c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((f (f d) -> c) -> Costar f (f d) c
forall k (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar (Compose f f d -> c
dgfc (Compose f f d -> c) -> (f (f d) -> Compose f f d) -> f (f d) -> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f (f d) -> Compose f f d
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)) ((f d -> f d) -> Costar f d (f d)
forall k (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar f d -> f d
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

-- | This is a variant on 'stars' that uses 'Kleisli' instead of 'Star'.
--
-- @'kleislis' :: 'Monad' f => Iso' ('Procompose' ('Kleisli' f) ('Kleisli' g) d c) ('Kleisli' ('Compose' f g) d c)@
kleislis :: Monad g
        => Iso (Procompose (Kleisli f ) (Kleisli g ) d  c )
               (Procompose (Kleisli f') (Kleisli g') d' c')
               (Kleisli (Compose g  f ) d  c )
               (Kleisli (Compose g' f') d' c')
kleislis :: Iso
  (Procompose (Kleisli f) (Kleisli g) d c)
  (Procompose (Kleisli f') (Kleisli g') d' c')
  (Kleisli (Compose g f) d c)
  (Kleisli (Compose g' f') d' c')
kleislis = (Procompose (Kleisli f) (Kleisli g) d c
 -> Kleisli (Compose g f) d c)
-> (f (Kleisli (Compose g' f') d' c')
    -> f (Procompose (Kleisli f') (Kleisli g') d' c'))
-> p (Kleisli (Compose g f) d c)
     (f (Kleisli (Compose g' f') d' c'))
-> p (Procompose (Kleisli f) (Kleisli g) d c)
     (f (Procompose (Kleisli f') (Kleisli g') d' c'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Procompose (Kleisli f) (Kleisli g) d c -> Kleisli (Compose g f) d c
forall (f :: * -> *) (g :: * -> *) d c.
Monad f =>
Procompose (Kleisli g) (Kleisli f) d c -> Kleisli (Compose f g) d c
hither ((Kleisli (Compose g' f') d' c'
 -> Procompose (Kleisli f') (Kleisli g') d' c')
-> f (Kleisli (Compose g' f') d' c')
-> f (Procompose (Kleisli f') (Kleisli g') d' c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Kleisli (Compose g' f') d' c'
-> Procompose (Kleisli f') (Kleisli g') d' c'
forall (m :: * -> *) (m :: * -> *) d c.
Kleisli (Compose m m) d c -> Procompose (Kleisli m) (Kleisli m) d c
yon) where
  hither :: Procompose (Kleisli g) (Kleisli f) d c -> Kleisli (Compose f g) d c
hither (Procompose (Kleisli xgc) (Kleisli dfx)) = (d -> Compose f g c) -> Kleisli (Compose f g) d c
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (f (g c) -> Compose f g c
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g c) -> Compose f g c) -> (d -> f (g c)) -> d -> Compose f g c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (x -> g c) -> f x -> f (g c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM x -> g c
xgc (f x -> f (g c)) -> (d -> f x) -> d -> f (g c)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> f x
dfx)
  yon :: Kleisli (Compose m m) d c -> Procompose (Kleisli m) (Kleisli m) d c
yon (Kleisli d -> Compose m m c
dfgc) = Kleisli m (m c) c
-> Kleisli m d (m c) -> Procompose (Kleisli m) (Kleisli m) d c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((m c -> m c) -> Kleisli m (m c) c
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli m c -> m c
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) ((d -> m (m c)) -> Kleisli m d (m c)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (Compose m m c -> m (m c)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose m m c -> m (m c)) -> (d -> Compose m m c) -> d -> m (m c)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. d -> Compose m m c
dfgc))

-- | This is a variant on 'costars' that uses 'Cokleisli' instead
-- of 'Costar'.
--
-- @'cokleislis' :: 'Functor' f => Iso' ('Procompose' ('Cokleisli' f) ('Cokleisli' g) d c) ('Cokleisli' ('Compose' g f) d c)@
cokleislis :: Functor f
          => Iso (Procompose (Cokleisli f ) (Cokleisli g ) d  c )
                 (Procompose (Cokleisli f') (Cokleisli g') d' c')
                 (Cokleisli (Compose f  g ) d  c )
                 (Cokleisli (Compose f' g') d' c')
cokleislis :: Iso
  (Procompose (Cokleisli f) (Cokleisli g) d c)
  (Procompose (Cokleisli f') (Cokleisli g') d' c')
  (Cokleisli (Compose f g) d c)
  (Cokleisli (Compose f' g') d' c')
cokleislis = (Procompose (Cokleisli f) (Cokleisli g) d c
 -> Cokleisli (Compose f g) d c)
-> (f (Cokleisli (Compose f' g') d' c')
    -> f (Procompose (Cokleisli f') (Cokleisli g') d' c'))
-> p (Cokleisli (Compose f g) d c)
     (f (Cokleisli (Compose f' g') d' c'))
-> p (Procompose (Cokleisli f) (Cokleisli g) d c)
     (f (Procompose (Cokleisli f') (Cokleisli g') d' c'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Procompose (Cokleisli f) (Cokleisli g) d c
-> Cokleisli (Compose f g) d c
forall k (w :: * -> *) (w :: k -> *) (d :: k) c.
Functor w =>
Procompose (Cokleisli w) (Cokleisli w) d c
-> Cokleisli (Compose w w) d c
hither ((Cokleisli (Compose f' g') d' c'
 -> Procompose (Cokleisli f') (Cokleisli g') d' c')
-> f (Cokleisli (Compose f' g') d' c')
-> f (Procompose (Cokleisli f') (Cokleisli g') d' c')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cokleisli (Compose f' g') d' c'
-> Procompose (Cokleisli f') (Cokleisli g') d' c'
forall k (w :: * -> *) (w :: k -> *) (d :: k) c.
Cokleisli (Compose w w) d c
-> Procompose (Cokleisli w) (Cokleisli w) d c
yon) where
  hither :: Procompose (Cokleisli w) (Cokleisli w) d c
-> Cokleisli (Compose w w) d c
hither (Procompose (Cokleisli gxc) (Cokleisli fdx)) = (Compose w w d -> c) -> Cokleisli (Compose w w) d c
forall k (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli (w x -> c
gxc (w x -> c) -> (Compose w w d -> w x) -> Compose w w d -> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (w d -> x) -> w (w d) -> w x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w d -> x
fdx (w (w d) -> w x)
-> (Compose w w d -> w (w d)) -> Compose w w d -> w x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Compose w w d -> w (w d)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
  yon :: Cokleisli (Compose w w) d c
-> Procompose (Cokleisli w) (Cokleisli w) d c
yon (Cokleisli Compose w w d -> c
dgfc) = Cokleisli w (w d) c
-> Cokleisli w d (w d)
-> Procompose (Cokleisli w) (Cokleisli w) d c
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose ((w (w d) -> c) -> Cokleisli w (w d) c
forall k (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli (Compose w w d -> c
dgfc (Compose w w d -> c) -> (w (w d) -> Compose w w d) -> w (w d) -> c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. w (w d) -> Compose w w d
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)) ((w d -> w d) -> Cokleisli w d (w d)
forall k (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli w d -> w d
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

----------------------------------------------------------------------------
-- * Rift
----------------------------------------------------------------------------

-- | This represents the right Kan lift of a 'Profunctor' @q@ along a
-- 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where
-- the only object is the category Hask, 1-morphisms are profunctors composed
-- and compose with Profunctor composition, and 2-morphisms are just natural
-- transformations.
--
-- 'Rift' has a polymorphic kind since @5.6@.

-- Rift :: (k3 -> k2 -> Type) -> (k1 -> k2 -> Type) -> (k1 -> k3 -> Type)
newtype Rift p q a b = Rift { Rift p q a b -> forall (x :: k). p b x -> q a x
runRift :: forall x. p b x -> q a x }

instance ProfunctorFunctor (Rift p) where
  promap :: (p :-> q) -> Rift p p :-> Rift p q
promap p :-> q
f (Rift forall x. p b x -> p a x
g) = (forall x. p b x -> q a x) -> Rift p q a b
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift (p a x -> q a x
p :-> q
f (p a x -> q a x) -> (p b x -> p a x) -> p b x -> q a x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p b x -> p a x
forall x. p b x -> p a x
g)

instance Category p => ProfunctorComonad (Rift p) where
  proextract :: Rift p p :-> p
proextract (Rift forall x. p b x -> p a x
f) = p b b -> p a b
forall x. p b x -> p a x
f p b b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  produplicate :: Rift p p :-> Rift p (Rift p p)
produplicate (Rift forall x. p b x -> p a x
f) = (forall x. p b x -> Rift p p a x) -> Rift p (Rift p p) a b
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift ((forall x. p b x -> Rift p p a x) -> Rift p (Rift p p) a b)
-> (forall x. p b x -> Rift p p a x) -> Rift p (Rift p p) a b
forall a b. (a -> b) -> a -> b
$ \p b x
p -> (forall x. p x x -> p a x) -> Rift p p a x
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift ((forall x. p x x -> p a x) -> Rift p p a x)
-> (forall x. p x x -> p a x) -> Rift p p a x
forall a b. (a -> b) -> a -> b
$ \p x x
q -> p b x -> p a x
forall x. p b x -> p a x
f (p x x
q p x x -> p b x -> p b x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p b x
p)

instance (Profunctor p, Profunctor q) => Profunctor (Rift p q) where
  dimap :: (a -> b) -> (c -> d) -> Rift p q b c -> Rift p q a d
dimap a -> b
ca c -> d
bd Rift p q b c
f = (forall x. p d x -> q a x) -> Rift p q a d
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift ((a -> b) -> q b x -> q a x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
ca (q b x -> q a x) -> (p d x -> q b x) -> p d x -> q a x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Rift p q b c -> forall x. p c x -> q b x
forall k k (p :: k -> k -> *) k (q :: k -> k -> *) (a :: k)
       (b :: k).
Rift p q a b -> forall (x :: k). p b x -> q a x
runRift Rift p q b c
f (p c x -> q b x) -> (p d x -> p c x) -> p d x -> q b x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (c -> d) -> p d x -> p c x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap c -> d
bd)
  {-# INLINE dimap #-}
  lmap :: (a -> b) -> Rift p q b c -> Rift p q a c
lmap a -> b
ca Rift p q b c
f = (forall x. p c x -> q a x) -> Rift p q a c
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift ((a -> b) -> q b x -> q a x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
ca (q b x -> q a x) -> (p c x -> q b x) -> p c x -> q a x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Rift p q b c -> forall x. p c x -> q b x
forall k k (p :: k -> k -> *) k (q :: k -> k -> *) (a :: k)
       (b :: k).
Rift p q a b -> forall (x :: k). p b x -> q a x
runRift Rift p q b c
f)
  {-# INLINE lmap #-}
  rmap :: (b -> c) -> Rift p q a b -> Rift p q a c
rmap b -> c
bd Rift p q a b
f = (forall x. p c x -> q a x) -> Rift p q a c
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift (Rift p q a b -> forall x. p b x -> q a x
forall k k (p :: k -> k -> *) k (q :: k -> k -> *) (a :: k)
       (b :: k).
Rift p q a b -> forall (x :: k). p b x -> q a x
runRift Rift p q a b
f (p b x -> q a x) -> (p c x -> p b x) -> p c x -> q a x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (b -> c) -> p c x -> p b x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap b -> c
bd)
  {-# INLINE rmap #-}
  q b c
bd #. :: q b c -> Rift p q a b -> Rift p q a c
#. Rift p q a b
f = (forall x. p c x -> q a x) -> Rift p q a c
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift (\p c x
p -> Rift p q a b -> p b x -> q a x
forall k k (p :: k -> k -> *) k (q :: k -> k -> *) (a :: k)
       (b :: k).
Rift p q a b -> forall (x :: k). p b x -> q a x
runRift Rift p q a b
f (p c x
p p c x -> q b c -> p b x
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# q b c
bd))
  {-# INLINE (#.) #-}
  Rift p q b c
f .# :: Rift p q b c -> q a b -> Rift p q a c
.# q a b
ca = (forall x. p c x -> q a x) -> Rift p q a c
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift (\p c x
p -> Rift p q b c -> p c x -> q b x
forall k k (p :: k -> k -> *) k (q :: k -> k -> *) (a :: k)
       (b :: k).
Rift p q a b -> forall (x :: k). p b x -> q a x
runRift Rift p q b c
f p c x
p q b x -> q a b -> q a x
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# q a b
ca)
  {-# INLINE (.#) #-}

instance Profunctor p => Functor (Rift p q a) where
  fmap :: (a -> b) -> Rift p q a a -> Rift p q a b
fmap a -> b
bd Rift p q a a
f = (forall x. p b x -> q a x) -> Rift p q a b
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift (Rift p q a a -> forall x. p a x -> q a x
forall k k (p :: k -> k -> *) k (q :: k -> k -> *) (a :: k)
       (b :: k).
Rift p q a b -> forall (x :: k). p b x -> q a x
runRift Rift p q a a
f (p a x -> q a x) -> (p b x -> p a x) -> p b x -> q a x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> b) -> p b x -> p a x
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
bd)
  {-# INLINE fmap #-}

-- | @'Rift' p p@ forms a 'Monad' in the 'Profunctor' 2-category, which is isomorphic to a Haskell 'Category' instance.
instance p ~ q => Category (Rift p q) where
  id :: Rift p q a a
id = (forall (x :: k). p a x -> q a x) -> Rift p q a a
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift forall (x :: k). p a x -> q a x
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  {-# INLINE id #-}
  Rift forall (x :: k). p c x -> q b x
f . :: Rift p q b c -> Rift p q a b -> Rift p q a c
. Rift forall (x :: k). p b x -> q a x
g = (forall (x :: k). p c x -> q a x) -> Rift p q a c
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift (q b x -> q a x
forall (x :: k). p b x -> q a x
g (q b x -> q a x) -> (q c x -> q b x) -> q c x -> q a x
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. q c x -> q b x
forall (x :: k). p c x -> q b x
f)
  {-# INLINE (.) #-}

-- | The 2-morphism that defines a left Kan lift.
--
-- Note: When @p@ is right adjoint to @'Rift' p (->)@ then 'decomposeRift' is the 'counit' of the adjunction.
decomposeRift :: Procompose p (Rift p q) :-> q
decomposeRift :: Procompose p (Rift p q) a b -> q a b
decomposeRift (Procompose p x b
p (Rift forall (x :: k). p x x -> q a x
pq)) = p x b -> q a b
forall (x :: k). p x x -> q a x
pq p x b
p
{-# INLINE decomposeRift #-}

instance ProfunctorAdjunction (Procompose p) (Rift p) where
  counit :: Procompose p (Rift p p) :-> p
counit (Procompose p x b
p (Rift forall x. p x x -> p a x
pq)) = p x b -> p a b
forall x. p x x -> p a x
pq p x b
p
  unit :: p :-> Rift p (Procompose p p)
unit p a b
q = (forall x. p b x -> Procompose p p a x)
-> Rift p (Procompose p p) a b
forall k k k (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p b x -> q a x) -> Rift p q a b
Rift ((forall x. p b x -> Procompose p p a x)
 -> Rift p (Procompose p p) a b)
-> (forall x. p b x -> Procompose p p a x)
-> Rift p (Procompose p p) a b
forall a b. (a -> b) -> a -> b
$ \p b x
p -> p b x -> p a b -> Procompose p p a x
forall k k k (p :: k -> k -> *) (x :: k) (c :: k)
       (q :: k -> k -> *) (d :: k).
p x c -> q d x -> Procompose p q d c
Procompose p b x
p p a b
q

--instance (ProfunctorAdjunction f g, ProfunctorAdjunction f' g') => ProfunctorAdjunction (ProfunctorCompose f' f) (ProfunctorCompose g g') where

----------------------------------------------------------------------------
-- * Monoids
----------------------------------------------------------------------------


-- | a 'Category' that is also a 'Profunctor' is a 'Monoid' in @Prof@

eta :: (Profunctor p, Category p) => (->) :-> p
eta :: (->) :-> p
eta a -> b
f = (a -> b) -> p a a -> p a b
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
f p a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

mu :: Category p => Procompose p p :-> p
mu :: Procompose p p :-> p
mu (Procompose p x b
f p a x
g) = p x b
f p x b -> p a x -> p a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p a x
g