{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Safe #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Profunctor.Rep
-- Copyright   :  (C) 2011-2015 Edward Kmett,
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  Type-Families
--
----------------------------------------------------------------------------
module Data.Profunctor.Rep
  (
  -- * Representable Profunctors
    Representable(..)
  , tabulated
  , firstRep, secondRep
  -- * Corepresentable Profunctors
  , Corepresentable(..)
  , cotabulated
  , unfirstCorep, unsecondCorep
  , closedCorep
  -- * Prep -| Star
  , Prep(..)
  , prepAdj
  , unprepAdj
  , prepUnit
  , prepCounit
  -- * Coprep -| Costar
  , Coprep(..)
  , coprepAdj
  , uncoprepAdj
  , coprepUnit
  , coprepCounit
  ) where

import Control.Applicative
import Control.Arrow
import Control.Comonad
import Control.Monad ((>=>))
import Data.Functor.Identity
import Data.Profunctor
import Data.Profunctor.Sieve
import Data.Proxy
import Data.Tagged

-- * Representable Profunctors

-- | A 'Profunctor' @p@ is 'Representable' if there exists a 'Functor' @f@ such that
-- @p d c@ is isomorphic to @d -> f c@.
class (Sieve p (Rep p), Strong p) => Representable p where
  type Rep p :: * -> *
  -- | Laws:
  --
  -- @
  -- 'tabulate' '.' 'sieve' ≡ 'id'
  -- 'sieve' '.' 'tabulate' ≡ 'id'
  -- @
  tabulate :: (d -> Rep p c) -> p d c

-- | Default definition for 'first'' given that p is 'Representable'.
firstRep :: Representable p => p a b -> p (a, c) (b, c)
firstRep :: forall (p :: * -> * -> *) a b c.
Representable p =>
p a b -> p (a, c) (b, c)
firstRep p a b
p = ((a, c) -> Rep p (b, c)) -> p (a, c) (b, c)
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate (((a, c) -> Rep p (b, c)) -> p (a, c) (b, c))
-> ((a, c) -> Rep p (b, c)) -> p (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ \(a
a,c
c) -> (\b
b -> (b
b, c
c)) (b -> (b, c)) -> Rep p b -> Rep p (b, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> p a b -> a -> Rep p b
forall a b. p a b -> a -> Rep p b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p a b
p a
a

-- | Default definition for 'second'' given that p is 'Representable'.
secondRep :: Representable p => p a b -> p (c, a) (c, b)
secondRep :: forall (p :: * -> * -> *) a b c.
Representable p =>
p a b -> p (c, a) (c, b)
secondRep p a b
p = ((c, a) -> Rep p (c, b)) -> p (c, a) (c, b)
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate (((c, a) -> Rep p (c, b)) -> p (c, a) (c, b))
-> ((c, a) -> Rep p (c, b)) -> p (c, a) (c, b)
forall a b. (a -> b) -> a -> b
$ \(c
c,a
a) -> (,) c
c (b -> (c, b)) -> Rep p b -> Rep p (c, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> p a b -> a -> Rep p b
forall a b. p a b -> a -> Rep p b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p a b
p a
a

instance Representable (->) where
  type Rep (->) = Identity
  tabulate :: forall d c. (d -> Rep (->) c) -> d -> c
tabulate d -> Rep (->) c
f = Identity c -> c
forall a. Identity a -> a
runIdentity (Identity c -> c) -> (d -> Identity c) -> d -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> Identity c
d -> Rep (->) c
f
  {-# INLINE tabulate #-}

instance (Monad m, Functor m) => Representable (Kleisli m) where
  type Rep (Kleisli m) = m
  tabulate :: forall d c. (d -> Rep (Kleisli m) c) -> Kleisli m d c
tabulate = (d -> m c) -> Kleisli m d c
(d -> Rep (Kleisli m) c) -> Kleisli m d c
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli
  {-# INLINE tabulate #-}

instance Functor f => Representable (Star f) where
  type Rep (Star f) = f
  tabulate :: forall d c. (d -> Rep (Star f) c) -> Star f d c
tabulate = (d -> f c) -> Star f d c
(d -> Rep (Star f) c) -> Star f d c
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star
  {-# INLINE tabulate #-}

instance Representable (Forget r) where
  type Rep (Forget r) = Const r
  tabulate :: forall d c. (d -> Rep (Forget r) c) -> Forget r d c
tabulate = (d -> r) -> Forget r d c
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget ((d -> r) -> Forget r d c)
-> ((d -> Const r c) -> d -> r) -> (d -> Const r c) -> Forget r d c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Const r c -> r
forall {k} a (b :: k). Const a b -> a
getConst (Const r c -> r) -> (d -> Const r c) -> d -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
  {-# INLINE tabulate #-}

{- TODO: coproducts and products
instance (Representable p, Representable q) => Representable (Bifunctor.Product p q)
  type Rep (Bifunctor.Product p q) = Functor.Product p q

instance (Corepresentable p, Corepresentable q) => Corepresentable (Bifunctor.Product p q) where
  type Rep (Bifunctor.Product p q) = Functor.Sum p q
-}

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

-- | 'tabulate' and 'sieve' form two halves of an isomorphism.
--
-- This can be used with the combinators from the @lens@ package.
--
-- @'tabulated' :: 'Representable' p => 'Iso'' (d -> 'Rep' p c) (p d c)@
tabulated :: (Representable p, Representable q) => Iso (d -> Rep p c) (d' -> Rep q c') (p d c) (q d' c')
tabulated :: forall (p :: * -> * -> *) (q :: * -> * -> *) d c d' c'.
(Representable p, Representable q) =>
Iso (d -> Rep p c) (d' -> Rep q c') (p d c) (q d' c')
tabulated = ((d -> Rep p c) -> p d c)
-> (f (q d' c') -> f (d' -> Rep q c'))
-> p (p d c) (f (q d' c'))
-> p (d -> Rep p c) (f (d' -> Rep q c'))
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (d -> Rep p c) -> p d c
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate ((q d' c' -> d' -> Rep q c') -> f (q d' c') -> f (d' -> Rep q c')
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap q d' c' -> d' -> Rep q c'
forall a b. q a b -> a -> Rep q b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve)
{-# INLINE tabulated #-}

-- * Corepresentable Profunctors

-- | A 'Profunctor' @p@ is 'Corepresentable' if there exists a 'Functor' @f@ such that
-- @p d c@ is isomorphic to @f d -> c@.
class (Cosieve p (Corep p), Costrong p) => Corepresentable p where
  type Corep p :: * -> *
  -- | Laws:
  --
  -- @
  -- 'cotabulate' '.' 'cosieve' ≡ 'id'
  -- 'cosieve' '.' 'cotabulate' ≡ 'id'
  -- @
  cotabulate :: (Corep p d -> c) -> p d c

-- | Default definition for 'unfirst' given that @p@ is 'Corepresentable'.
unfirstCorep :: Corepresentable p => p (a, d) (b, d) -> p a b
unfirstCorep :: forall (p :: * -> * -> *) a d b.
Corepresentable p =>
p (a, d) (b, d) -> p a b
unfirstCorep p (a, d) (b, d)
p = (Corep p a -> b) -> p a b
forall d c. (Corep p d -> c) -> p d c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate Corep p a -> b
f
  where f :: Corep p a -> b
f Corep p a
fa = b
b where (b
b, d
d) = p (a, d) (b, d) -> Corep p (a, d) -> (b, d)
forall a b. p a b -> Corep p a -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve p (a, d) (b, d)
p ((\a
a -> (a
a, d
d)) (a -> (a, d)) -> Corep p a -> Corep p (a, d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Corep p a
fa)

-- | Default definition for 'unsecond' given that @p@ is 'Corepresentable'.
unsecondCorep :: Corepresentable p => p (d, a) (d, b) -> p a b
unsecondCorep :: forall (p :: * -> * -> *) d a b.
Corepresentable p =>
p (d, a) (d, b) -> p a b
unsecondCorep p (d, a) (d, b)
p = (Corep p a -> b) -> p a b
forall d c. (Corep p d -> c) -> p d c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate Corep p a -> b
f
  where f :: Corep p a -> b
f Corep p a
fa = b
b where (d
d, b
b) = p (d, a) (d, b) -> Corep p (d, a) -> (d, b)
forall a b. p a b -> Corep p a -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve p (d, a) (d, b)
p ((,) d
d (a -> (d, a)) -> Corep p a -> Corep p (d, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Corep p a
fa)

-- | Default definition for 'closed' given that @p@ is 'Corepresentable'
closedCorep :: Corepresentable p => p a b -> p (x -> a) (x -> b)
closedCorep :: forall (p :: * -> * -> *) a b x.
Corepresentable p =>
p a b -> p (x -> a) (x -> b)
closedCorep p a b
p = (Corep p (x -> a) -> x -> b) -> p (x -> a) (x -> b)
forall d c. (Corep p d -> c) -> p d c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate ((Corep p (x -> a) -> x -> b) -> p (x -> a) (x -> b))
-> (Corep p (x -> a) -> x -> b) -> p (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ \Corep p (x -> a)
fs x
x -> p a b -> Corep p a -> b
forall a b. p a b -> Corep p a -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve p a b
p (((x -> a) -> a) -> Corep p (x -> a) -> Corep p a
forall a b. (a -> b) -> Corep p a -> Corep p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((x -> a) -> x -> a
forall a b. (a -> b) -> a -> b
$ x
x) Corep p (x -> a)
fs)

instance Corepresentable (->) where
  type Corep (->) = Identity
  cotabulate :: forall d c. (Corep (->) d -> c) -> d -> c
cotabulate Corep (->) d -> c
f = Identity d -> c
Corep (->) d -> c
f (Identity d -> c) -> (d -> Identity d) -> d -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> Identity d
forall a. a -> Identity a
Identity
  {-# INLINE cotabulate #-}

instance Functor w => Corepresentable (Cokleisli w) where
  type Corep (Cokleisli w) = w
  cotabulate :: forall d c. (Corep (Cokleisli w) d -> c) -> Cokleisli w d c
cotabulate = (w d -> c) -> Cokleisli w d c
(Corep (Cokleisli w) d -> c) -> Cokleisli w d c
forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli
  {-# INLINE cotabulate #-}

instance Corepresentable Tagged where
  type Corep Tagged = Proxy
  cotabulate :: forall d c. (Corep Tagged d -> c) -> Tagged d c
cotabulate Corep Tagged d -> c
f = c -> Tagged d c
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Corep Tagged d -> c
f Proxy d
Corep Tagged d
forall {k} (t :: k). Proxy t
Proxy)
  {-# INLINE cotabulate #-}

instance Functor f => Corepresentable (Costar f) where
  type Corep (Costar f) = f
  cotabulate :: forall d c. (Corep (Costar f) d -> c) -> Costar f d c
cotabulate = (f d -> c) -> Costar f d c
(Corep (Costar f) d -> c) -> Costar f d c
forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar
  {-# INLINE cotabulate #-}

-- | 'cotabulate' and 'cosieve' form two halves of an isomorphism.
--
-- This can be used with the combinators from the @lens@ package.
--
-- @'cotabulated' :: 'Corep' f p => 'Iso'' (f d -> c) (p d c)@
cotabulated :: (Corepresentable p, Corepresentable q) => Iso (Corep p d -> c) (Corep q d' -> c') (p d c) (q d' c')
cotabulated :: forall (p :: * -> * -> *) (q :: * -> * -> *) d c d' c'.
(Corepresentable p, Corepresentable q) =>
Iso (Corep p d -> c) (Corep q d' -> c') (p d c) (q d' c')
cotabulated = ((Corep p d -> c) -> p d c)
-> (f (q d' c') -> f (Corep q d' -> c'))
-> p (p d c) (f (q d' c'))
-> p (Corep p d -> c) (f (Corep q d' -> c'))
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Corep p d -> c) -> p d c
forall d c. (Corep p d -> c) -> p d c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate ((q d' c' -> Corep q d' -> c')
-> f (q d' c') -> f (Corep q d' -> c')
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap q d' c' -> Corep q d' -> c'
forall a b. q a b -> Corep q a -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
cosieve)
{-# INLINE cotabulated #-}

--------------------------------------------------------------------------------
-- * Prep
--------------------------------------------------------------------------------

-- | @'Prep' -| 'Star' :: [Hask, Hask] -> Prof@
--
-- This gives rise to a monad in @Prof@, @('Star'.'Prep')@, and
-- a comonad in @[Hask,Hask]@ @('Prep'.'Star')@
--
-- 'Prep' has a polymorphic kind since @5.6@.

-- Prep :: (Type -> k -> Type) -> (k -> Type)
data Prep p a where
  Prep :: x -> p x a -> Prep p a

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

instance (Applicative (Rep p), Representable p) => Applicative (Prep p) where
  pure :: forall a. a -> Prep p a
pure a
a = () -> p () a -> Prep p a
forall {k} x (p :: * -> k -> *) (a :: k). x -> p x a -> Prep p a
Prep () (p () a -> Prep p a) -> p () a -> Prep p a
forall a b. (a -> b) -> a -> b
$ (() -> Rep p a) -> p () a
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate ((() -> Rep p a) -> p () a) -> (() -> Rep p a) -> p () a
forall a b. (a -> b) -> a -> b
$ Rep p a -> () -> Rep p a
forall a b. a -> b -> a
const (Rep p a -> () -> Rep p a) -> Rep p a -> () -> Rep p a
forall a b. (a -> b) -> a -> b
$ a -> Rep p a
forall a. a -> Rep p a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
  Prep x
xf p x (a -> b)
pf <*> :: forall a b. Prep p (a -> b) -> Prep p a -> Prep p b
<*> Prep x
xa p x a
pa = (x, x) -> p (x, x) b -> Prep p b
forall {k} x (p :: * -> k -> *) (a :: k). x -> p x a -> Prep p a
Prep (x
xf,x
xa) (((x, x) -> Rep p b) -> p (x, x) b
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate (x, x) -> Rep p b
go) where
    go :: (x, x) -> Rep p b
go (x
xf',x
xa') = p x (a -> b) -> x -> Rep p (a -> b)
forall a b. p a b -> a -> Rep p b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p x (a -> b)
pf x
xf' Rep p (a -> b) -> Rep p a -> Rep p b
forall a b. Rep p (a -> b) -> Rep p a -> Rep p b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> p x a -> x -> Rep p a
forall a b. p a b -> a -> Rep p b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p x a
pa x
xa'

instance (Monad (Rep p), Representable p) => Monad (Prep p) where
  return :: forall a. a -> Prep p a
return a
a = () -> p () a -> Prep p a
forall {k} x (p :: * -> k -> *) (a :: k). x -> p x a -> Prep p a
Prep () (p () a -> Prep p a) -> p () a -> Prep p a
forall a b. (a -> b) -> a -> b
$ (() -> Rep p a) -> p () a
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate ((() -> Rep p a) -> p () a) -> (() -> Rep p a) -> p () a
forall a b. (a -> b) -> a -> b
$ Rep p a -> () -> Rep p a
forall a b. a -> b -> a
const (Rep p a -> () -> Rep p a) -> Rep p a -> () -> Rep p a
forall a b. (a -> b) -> a -> b
$ a -> Rep p a
forall a. a -> Rep p a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  Prep x
xa p x a
pa >>= :: forall a b. Prep p a -> (a -> Prep p b) -> Prep p b
>>= a -> Prep p b
f = x -> p x b -> Prep p b
forall {k} x (p :: * -> k -> *) (a :: k). x -> p x a -> Prep p a
Prep x
xa (p x b -> Prep p b) -> p x b -> Prep p b
forall a b. (a -> b) -> a -> b
$ (x -> Rep p b) -> p x b
forall d c. (d -> Rep p c) -> p d c
forall (p :: * -> * -> *) d c.
Representable p =>
(d -> Rep p c) -> p d c
tabulate ((x -> Rep p b) -> p x b) -> (x -> Rep p b) -> p x b
forall a b. (a -> b) -> a -> b
$ p x a -> x -> Rep p a
forall a b. p a b -> a -> Rep p b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p x a
pa (x -> Rep p a) -> (a -> Rep p b) -> x -> Rep p b
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \a
a -> case a -> Prep p b
f a
a of
    Prep x
xb p x b
pb -> p x b -> x -> Rep p b
forall a b. p a b -> a -> Rep p b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve p x b
pb x
xb

prepAdj :: (forall a. Prep p a -> g a) -> p :-> Star g
prepAdj :: forall {k1} (p :: * -> k1 -> *) (g :: k1 -> *).
(forall (a :: k1). Prep p a -> g a) -> p :-> Star g
prepAdj forall (a :: k1). Prep p a -> g a
k p a b
p = (a -> g b) -> Star g a b
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((a -> g b) -> Star g a b) -> (a -> g b) -> Star g a b
forall a b. (a -> b) -> a -> b
$ \a
x -> Prep p b -> g b
forall (a :: k1). Prep p a -> g a
k (a -> p a b -> Prep p b
forall {k} x (p :: * -> k -> *) (a :: k). x -> p x a -> Prep p a
Prep a
x p a b
p)

unprepAdj :: (p :-> Star g) -> Prep p a -> g a
unprepAdj :: forall {k} (p :: * -> k -> *) (g :: k -> *) (a :: k).
(p :-> Star g) -> Prep p a -> g a
unprepAdj p :-> Star g
k (Prep x
x p x a
p) = Star g x a -> x -> g a
forall {k} (f :: k -> *) d (c :: k). Star f d c -> d -> f c
runStar (p x a -> Star g x a
p :-> Star g
k p x a
p) x
x

prepUnit :: p :-> Star (Prep p)
prepUnit :: forall {k} (p :: * -> k -> *) a (b :: k).
p a b -> Star (Prep p) a b
prepUnit p a b
p = (a -> Prep p b) -> Star (Prep p) a b
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((a -> Prep p b) -> Star (Prep p) a b)
-> (a -> Prep p b) -> Star (Prep p) a b
forall a b. (a -> b) -> a -> b
$ \a
x -> a -> p a b -> Prep p b
forall {k} x (p :: * -> k -> *) (a :: k). x -> p x a -> Prep p a
Prep a
x p a b
p

prepCounit :: Prep (Star f) a -> f a
prepCounit :: forall {k} (f :: k -> *) (a :: k). Prep (Star f) a -> f a
prepCounit (Prep x
x Star f x a
p) = Star f x a -> x -> f a
forall {k} (f :: k -> *) d (c :: k). Star f d c -> d -> f c
runStar Star f x a
p x
x

--------------------------------------------------------------------------------
-- * Coprep
--------------------------------------------------------------------------------

-- | 'Prep' has a polymorphic kind since @5.6@.

-- Coprep :: (k -> Type -> Type) -> (k -> Type)
newtype Coprep p a = Coprep { forall {k} (p :: k -> * -> *) (a :: k).
Coprep p a -> forall r. p a r -> r
runCoprep :: forall r. p a r -> r }

instance Profunctor p => Functor (Coprep p) where
  fmap :: forall a b. (a -> b) -> Coprep p a -> Coprep p b
fmap a -> b
f (Coprep forall r. p a r -> r
g) = (forall r. p b r -> r) -> Coprep p b
forall {k} (p :: k -> * -> *) (a :: k).
(forall r. p a r -> r) -> Coprep p a
Coprep (p a r -> r
forall r. p a r -> r
g (p a r -> r) -> (p b r -> p a r) -> p b r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> p b r -> p a r
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f)

-- | @'Coprep' -| 'Costar' :: [Hask, Hask]^op -> Prof@
--
-- Like all adjunctions this gives rise to a monad and a comonad.
--
-- This gives rise to a monad on Prof @('Costar'.'Coprep')@ and
-- a comonad on @[Hask, Hask]^op@ given by @('Coprep'.'Costar')@ which
-- is a monad in @[Hask,Hask]@
coprepAdj :: (forall a. f a -> Coprep p a) -> p :-> Costar f
coprepAdj :: forall {k} (f :: k -> *) (p :: k -> * -> *).
(forall (a :: k). f a -> Coprep p a) -> p :-> Costar f
coprepAdj forall (a :: k). f a -> Coprep p a
k p a b
p = (f a -> b) -> Costar f a b
forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar ((f a -> b) -> Costar f a b) -> (f a -> b) -> Costar f a b
forall a b. (a -> b) -> a -> b
$ \f a
f -> Coprep p a -> forall r. p a r -> r
forall {k} (p :: k -> * -> *) (a :: k).
Coprep p a -> forall r. p a r -> r
runCoprep (f a -> Coprep p a
forall (a :: k). f a -> Coprep p a
k f a
f) p a b
p

uncoprepAdj :: (p :-> Costar f) -> f a -> Coprep p a
uncoprepAdj :: forall {k} (p :: k -> * -> *) (f :: k -> *) (a :: k).
(p :-> Costar f) -> f a -> Coprep p a
uncoprepAdj p :-> Costar f
k f a
f = (forall r. p a r -> r) -> Coprep p a
forall {k} (p :: k -> * -> *) (a :: k).
(forall r. p a r -> r) -> Coprep p a
Coprep ((forall r. p a r -> r) -> Coprep p a)
-> (forall r. p a r -> r) -> Coprep p a
forall a b. (a -> b) -> a -> b
$ \p a r
p -> Costar f a r -> f a -> r
forall {k} (f :: k -> *) (d :: k) c. Costar f d c -> f d -> c
runCostar (p a r -> Costar f a r
p :-> Costar f
k p a r
p) f a
f

coprepUnit :: p :-> Costar (Coprep p)
coprepUnit :: forall {k} (p :: k -> * -> *) (a :: k) b.
p a b -> Costar (Coprep p) a b
coprepUnit p a b
p = (Coprep p a -> b) -> Costar (Coprep p) a b
forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar ((Coprep p a -> b) -> Costar (Coprep p) a b)
-> (Coprep p a -> b) -> Costar (Coprep p) a b
forall a b. (a -> b) -> a -> b
$ \Coprep p a
f -> Coprep p a -> forall r. p a r -> r
forall {k} (p :: k -> * -> *) (a :: k).
Coprep p a -> forall r. p a r -> r
runCoprep Coprep p a
f p a b
p

coprepCounit :: f a -> Coprep (Costar f) a
coprepCounit :: forall {k} (f :: k -> *) (a :: k). f a -> Coprep (Costar f) a
coprepCounit f a
f = (forall r. Costar f a r -> r) -> Coprep (Costar f) a
forall {k} (p :: k -> * -> *) (a :: k).
(forall r. p a r -> r) -> Coprep p a
Coprep ((forall r. Costar f a r -> r) -> Coprep (Costar f) a)
-> (forall r. Costar f a r -> r) -> Coprep (Costar f) a
forall a b. (a -> b) -> a -> b
$ \Costar f a r
p -> Costar f a r -> f a -> r
forall {k} (f :: k -> *) (d :: k) c. Costar f d c -> f d -> c
runCostar Costar f a r
p f a
f