{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Safe #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2013-2015 Edward Kmett and Dan Doel
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  Rank2Types, TFs
--
----------------------------------------------------------------------------
module Data.Profunctor.Ran
  ( Ran(..)
  , decomposeRan
  , precomposeRan
  , curryRan
  , uncurryRan
  , Codensity(..)
  , decomposeCodensity
  ) where

import Control.Category
import Data.Profunctor
import Data.Profunctor.Composition
import Data.Profunctor.Monad
import Data.Profunctor.Unsafe
import Prelude hiding (id,(.))

--------------------------------------------------------------------------------
-- * Ran
--------------------------------------------------------------------------------

-- | This represents the right Kan extension 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.
--
-- 'Ran' has a polymorphic kind since @5.6@.

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

instance ProfunctorFunctor (Ran p) where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Ran p p :-> Ran p q
promap p :-> q
f (Ran forall x. p x a -> p x b
g) = (forall x. p x a -> q x b) -> Ran p q a b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran (p x b -> q x b
p :-> q
f (p x b -> q x b) -> (p x a -> p x b) -> p x a -> q x 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 x a -> p x b
forall x. p x a -> p x b
g)

instance Category p => ProfunctorComonad (Ran p) where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Ran p p :-> p
proextract (Ran forall x. p x a -> p x b
f) = p a a -> p a b
forall x. p x a -> p x b
f p a a
forall a. p a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Ran p p :-> Ran p (Ran p p)
produplicate (Ran forall x. p x a -> p x b
f) = (forall x. p x a -> Ran p p x b) -> Ran p (Ran p p) a b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran ((forall x. p x a -> Ran p p x b) -> Ran p (Ran p p) a b)
-> (forall x. p x a -> Ran p p x b) -> Ran p (Ran p p) a b
forall a b. (a -> b) -> a -> b
$ \ p x a
p -> (forall x. p x x -> p x b) -> Ran p p x b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran ((forall x. p x x -> p x b) -> Ran p p x b)
-> (forall x. p x x -> p x b) -> Ran p p x b
forall a b. (a -> b) -> a -> b
$ \p x x
q -> p x a -> p x b
forall x. p x a -> p x b
f (p x a
p p x a -> p x x -> p x a
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 x x
q)

instance (Profunctor p, Profunctor q) => Profunctor (Ran p q) where
  dimap :: forall a b c d. (a -> b) -> (c -> d) -> Ran p q b c -> Ran p q a d
dimap a -> b
ca c -> d
bd Ran p q b c
f = (forall x. p x a -> q x d) -> Ran p q a d
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran ((c -> d) -> q x c -> q x d
forall b c a. (b -> c) -> q a b -> q a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
bd (q x c -> q x d) -> (p x a -> q x c) -> p x a -> q x 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
. Ran p q b c -> forall x. p x b -> q x c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p q b c
f (p x b -> q x c) -> (p x a -> p x b) -> p x a -> q x c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> b) -> p x a -> p x b
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 a -> b
ca)
  {-# INLINE dimap #-}
  lmap :: forall a b c. (a -> b) -> Ran p q b c -> Ran p q a c
lmap a -> b
ca Ran p q b c
f = (forall x. p x a -> q x c) -> Ran p q a c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran (Ran p q b c -> forall x. p x b -> q x c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p q b c
f (p x b -> q x c) -> (p x a -> p x b) -> p x a -> q x c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> b) -> p x a -> p x b
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 a -> b
ca)
  {-# INLINE lmap #-}
  rmap :: forall b c a. (b -> c) -> Ran p q a b -> Ran p q a c
rmap b -> c
bd Ran p q a b
f = (forall x. p x a -> q x c) -> Ran p q a c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran ((b -> c) -> q x b -> q x c
forall b c a. (b -> c) -> q a b -> q a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
bd (q x b -> q x c) -> (p x a -> q x b) -> p x a -> q x 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
. Ran p q a b -> forall x. p x a -> q x b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p q a b
f)
  {-# INLINE rmap #-}
  q b c
bd #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Ran p q a b -> Ran p q a c
#. Ran p q a b
f = (forall x. p x a -> q x c) -> Ran p q a c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran (\p x a
p -> q b c
bd q b c -> q x b -> q x c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> q a b -> q a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. Ran p q a b -> forall x. p x a -> q x b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p q a b
f p x a
p)
  {-# INLINE (#.) #-}
  Ran p q b c
f .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Ran p q b c -> q a b -> Ran p q a c
.# q a b
ca = (forall x. p x a -> q x c) -> Ran p q a c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran (\p x a
p -> Ran p q b c -> forall x. p x b -> q x c
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p q b c
f (q a b
ca q a b -> p x a -> p x b
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> p a b -> p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. p x a
p))
  {-# INLINE (.#) #-}

instance Profunctor q => Functor (Ran p q a) where
  fmap :: forall a b. (a -> b) -> Ran p q a a -> Ran p q a b
fmap a -> b
bd Ran p q a a
f = (forall x. p x a -> q x b) -> Ran p q a b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran ((a -> b) -> q x a -> q x b
forall b c a. (b -> c) -> q a b -> q a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
bd (q x a -> q x b) -> (p x a -> q x a) -> p x a -> q x 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
. Ran p q a a -> forall x. p x a -> q x a
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p q a a
f)
  {-# INLINE fmap #-}

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

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

precomposeRan :: Profunctor q => Procompose q (Ran p (->)) :-> Ran p q
precomposeRan :: forall {k} (q :: * -> * -> *) (p :: * -> k -> *).
Profunctor q =>
Procompose q (Ran p (->)) :-> Ran p q
precomposeRan (Procompose q x b
p Ran p (->) a x
pf) = (forall x. p x a -> q x b) -> Ran p q a b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran (\p x a
pxa -> Ran p (->) a x -> forall x. p x a -> x -> x
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran p (->) a x
pf p x a
pxa (x -> x) -> q x b -> q x b
forall a b c. (a -> b) -> q b c -> q a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
`lmap` q x b
p)
{-# INLINE precomposeRan #-}

curryRan :: (Procompose p q :-> r) -> p :-> Ran q r
curryRan :: forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *)
       (r :: k -> k -> *).
(Procompose p q :-> r) -> p :-> Ran q r
curryRan Procompose p q :-> r
f p a b
p = (forall (x :: k). q x a -> r x b) -> Ran q r a b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
(forall (x :: k). p x a -> q x b) -> Ran p q a b
Ran ((forall (x :: k). q x a -> r x b) -> Ran q r a b)
-> (forall (x :: k). q x a -> r x b) -> Ran q r a b
forall a b. (a -> b) -> a -> b
$ \q x a
q -> Procompose p q x b -> r x b
Procompose p q :-> r
f (p a b -> q x a -> Procompose p q x b
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose p a b
p q x a
q)
{-# INLINE curryRan #-}

uncurryRan :: (p :-> Ran q r) -> Procompose p q :-> r
uncurryRan :: forall {k} {k1} {k} (p :: k -> k1 -> *) (q :: k -> k -> *)
       (r :: k -> k1 -> *).
(p :-> Ran q r) -> Procompose p q :-> r
uncurryRan p :-> Ran q r
f (Procompose p x b
p q a x
q) = Ran q r x b -> forall (x :: k). q x x -> r x b
forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *) (a :: k)
       (b :: k).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan (p x b -> Ran q r x b
p :-> Ran q r
f p x b
p) q a x
q
{-# INLINE uncurryRan #-}

--------------------------------------------------------------------------------
-- * Codensity
--------------------------------------------------------------------------------

-- | This represents the right Kan extension of a 'Profunctor' @p@ along
-- itself. This provides a generalization of the \"difference list\" trick to
-- profunctors.
--
-- 'Codensity' has a polymorphic kind since @5.6@.

-- Codensity :: (k1 -> k2 -> Type) -> (k2 -> k2 -> Type)
newtype Codensity p a b = Codensity { forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity :: forall x. p x a -> p x b }

instance Profunctor p => Profunctor (Codensity p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Codensity p b c -> Codensity p a d
dimap a -> b
ca c -> d
bd Codensity p b c
f = (forall x. p x a -> p x d) -> Codensity p a d
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity ((c -> d) -> p x c -> p x d
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 c -> d
bd (p x c -> p x d) -> (p x a -> p x c) -> p x a -> p x 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
. Codensity p b c -> forall x. p x b -> p x c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity Codensity p b c
f (p x b -> p x c) -> (p x a -> p x b) -> p x a -> p x c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> b) -> p x a -> p x b
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 a -> b
ca)
  {-# INLINE dimap #-}
  lmap :: forall a b c. (a -> b) -> Codensity p b c -> Codensity p a c
lmap a -> b
ca Codensity p b c
f = (forall x. p x a -> p x c) -> Codensity p a c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (Codensity p b c -> forall x. p x b -> p x c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity Codensity p b c
f (p x b -> p x c) -> (p x a -> p x b) -> p x a -> p x c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> b) -> p x a -> p x b
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 a -> b
ca)
  {-# INLINE lmap #-}
  rmap :: forall b c a. (b -> c) -> Codensity p a b -> Codensity p a c
rmap b -> c
bd Codensity p a b
f = (forall x. p x a -> p x c) -> Codensity p a c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity ((b -> c) -> p x b -> p x 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
bd (p x b -> p x c) -> (p x a -> p x b) -> p x a -> p x 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
. Codensity p a b -> forall x. p x a -> p x b
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity Codensity p a b
f)
  {-# INLINE rmap #-}
  q b c
bd #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Codensity p a b -> Codensity p a c
#. Codensity p a b
f = (forall x. p x a -> p x c) -> Codensity p a c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (\p x a
p -> q b c
bd q b c -> p x b -> p x c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> p a b -> p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. Codensity p a b -> forall x. p x a -> p x b
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity Codensity p a b
f p x a
p)
  {-# INLINE (#.) #-}
  Codensity p b c
f .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Codensity p b c -> q a b -> Codensity p a c
.# q a b
ca = (forall x. p x a -> p x c) -> Codensity p a c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (\p x a
p -> Codensity p b c -> forall x. p x b -> p x c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity Codensity p b c
f (q a b
ca q a b -> p x a -> p x b
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> p a b -> p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. p x a
p))
  {-# INLINE (.#) #-}

instance Profunctor p => Functor (Codensity p a) where
  fmap :: forall a b. (a -> b) -> Codensity p a a -> Codensity p a b
fmap a -> b
bd Codensity p a a
f = (forall x. p x a -> p x b) -> Codensity p a b
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity ((a -> b) -> p x a -> p x b
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 a -> b
bd (p x a -> p x b) -> (p x a -> p x a) -> p x a -> p x 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
. Codensity p a a -> forall x. p x a -> p x a
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
Codensity p a b -> forall (x :: k). p x a -> p x b
runCodensity Codensity p a a
f)
  {-# INLINE fmap #-}

instance Category (Codensity p) where
  id :: forall (a :: k). Codensity p a a
id = (forall (x :: k). p x a -> p x a) -> Codensity p a a
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity p x a -> p x a
forall (x :: k). p x a -> p x a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
  {-# INLINE id #-}
  Codensity forall (x :: k). p x b -> p x c
f . :: forall (b :: k) (c :: k) (a :: k).
Codensity p b c -> Codensity p a b -> Codensity p a c
. Codensity forall (x :: k). p x a -> p x b
g = (forall (x :: k). p x a -> p x c) -> Codensity p a c
forall {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (p x b -> p x c
forall (x :: k). p x b -> p x c
f (p x b -> p x c) -> (p x a -> p x b) -> p x a -> p x 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 x a -> p x b
forall (x :: k). p x a -> p x b
g)
  {-# INLINE (.) #-}

decomposeCodensity :: Procompose (Codensity p) p a b -> p a b
decomposeCodensity :: forall {k2} {k1} (p :: k2 -> k1 -> *) (a :: k2) (b :: k1).
Procompose (Codensity p) p a b -> p a b
decomposeCodensity (Procompose (Codensity forall (x :: k2). p x x -> p x b
pp) p a x
p) = p a x -> p a b
forall (x :: k2). p x x -> p x b
pp p a x
p
{-# INLINE decomposeCodensity #-}