{-# 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 :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Procompose p p :-> Procompose p q
promap p :-> q
f (Procompose p x b
p p a x
q) = 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 :-> q
f p a x
q)

instance Category p => ProfunctorMonad (Procompose p) where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Procompose p p
proreturn = 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 forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
Procompose p (Procompose p p) :-> Procompose p p
projoin (Procompose p x b
p (Procompose p x x
q p a x
r)) = 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 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 :: forall {k} (p :: k -> k -> *) (a :: k) (b :: k).
Category p =>
Procompose p p a b -> p a b
procomposed (Procompose p x b
pxc p a x
pdx) = p x b
pxc 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 :: forall a b c d.
(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) = 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 (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
r p x c
f) (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 :: forall a b c. (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) = 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 (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 :: forall b c a. (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) = 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 (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 #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Procompose p q a b -> Procompose p q a c
#. Procompose p x b
f q a x
g     = 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 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 .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Procompose p q b c -> q a b -> Procompose p q a c
.# q a b
k     = 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 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 :: forall a b. (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) = 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 (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 :: forall a b. Procompose p q a b -> a -> Compose g f b
sieve (Procompose p x b
g q a x
f) a
d = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p x b
g forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 :: forall d c. (d -> Rep (Procompose p q) c) -> Procompose p q d c
tabulate d -> Rep (Procompose p q) c
f = 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 (forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate (forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a 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 :: forall a b. 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) = forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve p x b
g forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve q a x
f 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 :: forall d c. (Corep (Procompose p q) d -> c) -> Procompose p q d c
cotabulate Corep (Procompose p q) d -> c
f = 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 (forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate (Corep (Procompose p q) d -> c
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)) (forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate 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' :: forall a b c. Procompose p q a b -> Procompose p q (a, c) (b, c)
first' (Procompose p x b
x q a x
y) = 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 (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p x b
x) (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' q a x
y)
  {-# INLINE first' #-}
  second' :: forall a b c. Procompose p q a b -> Procompose p q (c, a) (c, b)
second' (Procompose p x b
x q a x
y) = 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 (forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (c, a) (c, b)
second' p x b
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' :: forall a b c.
Procompose p q a b -> Procompose p q (Either a c) (Either b c)
left' (Procompose p x b
x q a x
y) = 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 (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left' p x b
x) (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' :: forall a b c.
Procompose p q a b -> Procompose p q (Either c a) (Either c b)
right' (Procompose p x b
x q a x
y) = 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 (forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right' p x b
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 :: forall a b x.
Procompose p q a b -> Procompose p q (x -> a) (x -> b)
closed (Procompose p x b
x q a x
y) = 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 (forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed p x b
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' :: forall (f :: * -> *) a b.
Traversable f =>
Procompose p q a b -> Procompose p q (f a) (f b)
traverse' (Procompose p x b
p q a x
q) = 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 (forall (p :: * -> * -> *) (f :: * -> *) a b.
(Traversing p, Traversable f) =>
p a b -> p (f a) (f b)
traverse' p x b
p) (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' :: forall (f :: * -> *) a b.
Functor f =>
Procompose p q a b -> Procompose p q (f a) (f b)
map' (Procompose p x b
p q a x
q) = 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 (forall (p :: * -> * -> *) (f :: * -> *) a b.
(Mapping p, Functor f) =>
p a b -> p (f a) (f b)
map' p x b
p) (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 :: forall a d b. Procompose p q (a, d) (b, d) -> Procompose p q a b
unfirst = forall (p :: * -> * -> *) a d b.
Corepresentable p =>
p (a, d) (b, d) -> p a b
unfirstCorep
  {-# INLINE unfirst #-}
  unsecond :: forall d a b. Procompose p q (d, a) (d, b) -> Procompose p q a b
unsecond = 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 :: forall {k} (q :: * -> * -> *) d c (r :: k -> * -> *) (d' :: k) c'.
Profunctor q =>
Iso
  (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
idl = 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) -> forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap x -> c
g q d x
f) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 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 :: forall {k} (q :: * -> * -> *) d c (r :: * -> k -> *) d' (c' :: k).
Profunctor q =>
Iso
  (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c')
idr = 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) -> forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap d -> x
f q x c
g) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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` 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 :: forall {k} {k} {k} {k} {k} {k} (p :: k -> k -> *)
       (q :: k -> k -> *) (r :: k -> k -> *) (a :: k) (b :: k)
       (x :: k -> k -> *) (y :: k -> k -> *) (z :: k -> k -> *).
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 = 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 q x x
g r a x
h)) -> 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 (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)
              (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Procompose (Procompose x x b
f y x x
g) z a x
h) -> 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 (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 :: forall {k} {k} (g :: * -> *) (f :: k -> *) d (c :: k)
       (f' :: k -> *) (g' :: * -> *) d' (c' :: k).
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 = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall {k} {f :: * -> *} {g :: k -> *} {d} {c :: k}.
Functor f =>
Procompose (Star g) (Star f) d c -> Star (Compose f g) d c
hither (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 x -> g c
xgc) (Star d -> f x
dfx)) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> g c
xgc 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) = 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 (forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose 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 :: forall {k} {k} (f :: * -> *) (g :: k -> *) (d :: k) c
       (f' :: * -> *) (g' :: k -> *) (d' :: k) c'.
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 = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall {k} {f :: * -> *} {f :: k -> *} {d :: k} {c}.
Functor f =>
Procompose (Costar f) (Costar f) d c -> Costar (Compose f f) d c
hither (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k1} {f :: * -> *} {f :: k1 -> *} {d :: k1} {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 f x -> c
gxc) (Costar f d -> x
fdx)) = forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar (f x -> c
gxc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f d -> x
fdx forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k1} {k2} (f :: k1 -> *) (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) = 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 (forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar (Compose f f d -> c
dgfc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)) (forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar 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 :: forall (g :: * -> *) (f :: * -> *) d c (f' :: * -> *)
       (g' :: * -> *) d' c'.
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 = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall {f :: * -> *} {g :: * -> *} {a} {b}.
Monad f =>
Procompose (Kleisli g) (Kleisli f) a b -> Kleisli (Compose f g) a b
hither (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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) a b -> Kleisli (Compose f g) a b
hither (Procompose (Kleisli x -> g b
xgc) (Kleisli a -> f x
dfx)) = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM x -> g b
xgc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> 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) = 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 (forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) (forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose 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 :: forall {k} {k} (f :: * -> *) (g :: k -> *) (d :: k) c
       (f' :: * -> *) (g' :: k -> *) (d' :: k) c'.
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 = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall {k} {w :: * -> *} {w :: k -> *} {a :: k} {b}.
Functor w =>
Procompose (Cokleisli w) (Cokleisli w) a b
-> Cokleisli (Compose w w) a b
hither (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k1} {w :: * -> *} {w :: k1 -> *} {d :: k1} {c}.
Cokleisli (Compose w w) d c
-> Procompose (Cokleisli w) (Cokleisli w) d c
yon) where
  hither :: Procompose (Cokleisli w) (Cokleisli w) a b
-> Cokleisli (Compose w w) a b
hither (Procompose (Cokleisli w x -> b
gxc) (Cokleisli w a -> x
fdx)) = forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli (w x -> b
gxc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w a -> x
fdx forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k1} {k2} (f :: k1 -> *) (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) = 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 (forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli (Compose w w d -> c
dgfc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose)) (forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli 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 { forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
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 :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Rift p p :-> Rift p q
promap p :-> q
f (Rift forall x. p b x -> p a x
g) = 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 :-> q
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x. p b x -> p a x
g)

instance Category p => ProfunctorComonad (Rift p) where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Rift p p :-> p
proextract (Rift forall x. p b x -> p a x
f) = forall x. p b x -> p a x
f forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Rift p p :-> Rift p (Rift p p)
produplicate (Rift forall x. p b x -> p a x
f) = 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 a b. (a -> b) -> a -> b
$ \p b x
p -> 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 a b. (a -> b) -> a -> b
$ \p x x
q -> forall x. p b x -> p a x
f (p x x
q 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 :: forall a b c d.
(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 {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 (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
ca forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} {k} {k} (p :: 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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap c -> d
bd)
  {-# INLINE dimap #-}
  lmap :: forall a b c. (a -> b) -> Rift p q b c -> Rift p q a c
lmap a -> b
ca Rift p q b c
f = 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 (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
ca forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} {k} {k} (p :: 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 :: forall b c a. (b -> c) -> Rift p q a b -> Rift p q a c
rmap b -> c
bd Rift p q a b
f = 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 {k} {k} {k} (p :: 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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap b -> c
bd)
  {-# INLINE rmap #-}
  q b c
bd #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Rift p q a b -> Rift p q a c
#. Rift p q a b
f = 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 -> forall {k} {k} {k} (p :: 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 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 .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Rift p q b c -> q a b -> Rift p q a c
.# q a b
ca = 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 -> forall {k} {k} {k} (p :: 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 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 :: forall a b. (a -> b) -> Rift p q a a -> Rift p q a b
fmap a -> b
bd Rift p q a a
f = 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 {k} {k} {k} (p :: 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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (p :: * -> * -> *) a b c.
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 :: forall (a :: k). Rift p q a a
id = 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 {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 . :: forall (b :: k) (c :: k) (a :: k).
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 {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 b x -> q a x
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 :: forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *).
Procompose p (Rift p q) :-> q
decomposeRift (Procompose p x b
p (Rift forall (x :: k). p x x -> q a x
pq)) = forall (x :: k). p x x -> q a x
pq p x b
p
{-# INLINE decomposeRift #-}

instance ProfunctorAdjunction (Procompose p) (Rift p) where
  counit :: forall (p :: * -> * -> *).
Profunctor p =>
Procompose p (Rift p p) :-> p
counit (Procompose p x b
p (Rift forall x. p x x -> p a x
pq)) = forall x. p x x -> p a x
pq p x b
p
  unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> Rift p (Procompose p p)
unit p a b
q = 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 a b. (a -> b) -> a -> b
$ \p b x
p -> 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 :: forall (p :: * -> * -> *). (Profunctor p, Category p) => (->) :-> p
eta a -> b
f = forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
f forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

mu :: Category p => Procompose p p :-> p
mu :: forall {k} (p :: k -> k -> *). Category p => Procompose p p :-> p
mu (Procompose p x b
f p a x
g) = p x b
f 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