{-# 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 {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 :-> 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 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) = forall x. p x a -> p x b
f 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 {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 a b. (a -> b) -> a -> b
$ \ p x a
p -> 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 a b. (a -> b) -> a -> b
$ \p x x
q -> forall x. p x a -> p x b
f (p x a
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)

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 {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 (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
bd 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).
Ran p q a b -> forall (x :: k). p x a -> q x b
runRan Ran 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 :: * -> * -> *) 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 {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 {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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 {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 (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
bd 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).
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 {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 forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a 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 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 {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 -> 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 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 {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 (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
bd 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).
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 {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 {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 {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). p x b -> q x 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 (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} {k} (q :: k -> k -> *) (p :: k -> k -> *).
Procompose (Ran q p) q :-> p
decomposeRan (Procompose (Ran forall (x :: k). q x x -> p x b
qp) q a x
q) = 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 {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 -> 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 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 {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 a b. (a -> b) -> a -> b
$ \q x a
q -> Procompose p q :-> r
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 p a b
p q x a
q)
{-# INLINE curryRan #-}

uncurryRan :: (p :-> Ran q r) -> Procompose p q :-> r
uncurryRan :: forall {k} {k} {k} (p :: k -> k -> *) (q :: k -> k -> *)
       (r :: k -> k -> *).
(p :-> Ran q r) -> Procompose p q :-> r
uncurryRan p :-> Ran q r
f (Procompose p x b
p q a x
q) = 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 :-> 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 {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
bd 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} (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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> 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 Codensity p 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 :: * -> * -> *) 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 {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> c
bd 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} (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 {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 forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a 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 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 {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 -> 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 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 {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap a -> b
bd 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} (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 {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity 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 {k} {k} (p :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k). p x a -> p x b) -> Codensity p a b
Codensity (forall (x :: k). p x b -> p x 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 (x :: k). p x a -> p x b
g)
  {-# INLINE (.) #-}

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