{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2014-2018 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  portable
--
----------------------------------------------------------------------------
module Data.Profunctor.Closed
  ( Closed(..)
  , Closure(..)
  , close
  , unclose
  , Environment(..)
  , curry'
  ) where

import Control.Applicative
import Control.Arrow
import Control.Category
import Control.Comonad
import Data.Bifunctor.Product (Product(..))
import Data.Bifunctor.Sum (Sum(..))
import Data.Bifunctor.Tannen (Tannen(..))
import Data.Coerce (Coercible, coerce)
import Data.Distributive
import Data.Profunctor.Adjunction
import Data.Profunctor.Monad
import Data.Profunctor.Strong
import Data.Profunctor.Types
import Data.Profunctor.Unsafe
import Data.Semigroup hiding (Product, Sum)
import Data.Tagged
import Data.Tuple
import Prelude hiding ((.),id)

--------------------------------------------------------------------------------
-- * Closed
--------------------------------------------------------------------------------

-- | A strong profunctor allows the monoidal structure to pass through.
--
-- A closed profunctor allows the closed structure to pass through.
class Profunctor p => Closed p where
  -- | Laws:
  --
  -- @
  -- 'lmap' ('.' f) '.' 'closed' ≡ 'rmap' ('.' f) '.' 'closed'
  -- 'closed' '.' 'closed' ≡ 'dimap' 'uncurry' 'curry' '.' 'closed'
  -- 'dimap' 'const' ('$'()) '.' 'closed' ≡ 'id'
  -- @
  closed :: p a b -> p (x -> a) (x -> b)

instance Closed Tagged where
  closed :: forall a b x. Tagged a b -> Tagged (x -> a) (x -> b)
closed (Tagged b
b) = forall {k} (s :: k) b. b -> Tagged s b
Tagged (forall a b. a -> b -> a
const b
b)

instance Closed (->) where
  closed :: forall a b x. (a -> b) -> (x -> a) -> (x -> b)
closed = forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(.)

instance Functor f => Closed (Costar f) where
  closed :: forall a b x. Costar f a b -> Costar f (x -> a) (x -> b)
closed (Costar f a -> b
fab) = forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar forall a b. (a -> b) -> a -> b
$ \f (x -> a)
fxa x
x -> f a -> b
fab (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> a -> b
$ x
x) f (x -> a)
fxa)

instance Functor f => Closed (Cokleisli f) where
  closed :: forall a b x. Cokleisli f a b -> Cokleisli f (x -> a) (x -> b)
closed (Cokleisli f a -> b
fab) = forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli forall a b. (a -> b) -> a -> b
$ \f (x -> a)
fxa x
x -> f a -> b
fab (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> a -> b
$ x
x) f (x -> a)
fxa)

instance Distributive f => Closed (Star f) where
  closed :: forall a b x. Star f a b -> Star f (x -> a) (x -> b)
closed (Star a -> f b
afb) = forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star forall a b. (a -> b) -> a -> b
$ \x -> a
xa -> forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute forall a b. (a -> b) -> a -> b
$ \x
x -> a -> f b
afb (x -> a
xa x
x)

instance (Distributive f, Monad f) => Closed (Kleisli f) where
  closed :: forall a b x. Kleisli f a b -> Kleisli f (x -> a) (x -> b)
closed (Kleisli a -> f b
afb) = forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli forall a b. (a -> b) -> a -> b
$ \x -> a
xa -> forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
distribute forall a b. (a -> b) -> a -> b
$ \x
x -> a -> f b
afb (x -> a
xa x
x)

instance (Closed p, Closed q) => Closed (Product p q) where
  closed :: forall a b x. Product p q a b -> Product p q (x -> a) (x -> b)
closed (Pair p a b
p q a b
q) = forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed p a b
p) (forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed q a b
q)

instance (Closed p, Closed q) => Closed (Sum p q) where
  closed :: forall a b x. Sum p q a b -> Sum p q (x -> a) (x -> b)
closed (L2 p a b
p) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed p a b
p)
  closed (R2 q a b
q) = forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed q a b
q)

instance (Functor f, Closed p) => Closed (Tannen f p) where
  closed :: forall a b x. Tannen f p a b -> Tannen f p (x -> a) (x -> b)
closed (Tannen f (p a b)
fp) = forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed f (p a b)
fp)

-- instance Monoid r => Closed (Forget r) where
--  closed _ = Forget $ \_ -> mempty

curry' :: Closed p => p (a, b) c -> p a (b -> c)
curry' :: forall (p :: * -> * -> *) a b c.
Closed p =>
p (a, b) c -> p a (b -> c)
curry' = forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (,) 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 x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed

--------------------------------------------------------------------------------
-- * Closure
--------------------------------------------------------------------------------

-- | 'Closure' adjoins a 'Closed' structure to any 'Profunctor'.
--
-- Analogous to 'Data.Profunctor.Tambara.Tambara' for 'Strong'.

newtype Closure p a b = Closure { forall (p :: * -> * -> *) a b.
Closure p a b -> forall x. p (x -> a) (x -> b)
runClosure :: forall x. p (x -> a) (x -> b) }

instance Profunctor p => Profunctor (Closure p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Closure p b c -> Closure p a d
dimap a -> b
f c -> d
g (Closure forall x. p (x -> b) (x -> c)
p) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g) forall x. p (x -> b) (x -> c)
p
  lmap :: forall a b c. (a -> b) -> Closure p b c -> Closure p a c
lmap a -> b
f (Closure forall x. p (x -> b) (x -> c)
p) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) forall x. p (x -> b) (x -> c)
p
  rmap :: forall b c a. (b -> c) -> Closure p a b -> Closure p a c
rmap b -> c
f (Closure forall x. p (x -> a) (x -> b)
p) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c
f) forall x. p (x -> a) (x -> b)
p

  (#.) :: forall a b c q. Coercible c b => q b c -> Closure p a b -> Closure p a c
  q b c
_ #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Closure p a b -> Closure p a c
#. Closure forall x. p (x -> a) (x -> b)
p = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (coerce :: forall a b. Coercible a b => a -> b
coerce (forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id :: c -> c) :: b -> c) forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. forall x. p (x -> a) (x -> b)
p

  (.#) :: forall a b c q. Coercible b a => Closure p b c -> q a b -> Closure p a c
  Closure forall x. p (x -> b) (x -> c)
p .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Closure p b c -> q a b -> Closure p a c
.# q a b
_ = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall x. p (x -> b) (x -> c)
p forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (coerce :: forall a b. Coercible a b => a -> b
coerce (forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id :: b -> b) :: a -> b)

instance ProfunctorFunctor Closure where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Closure p :-> Closure q
promap p :-> q
f (Closure forall x. p (x -> a) (x -> b)
p) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (p :-> q
f forall x. p (x -> a) (x -> b)
p)

instance ProfunctorComonad Closure where
  proextract :: forall (p :: * -> * -> *). Profunctor p => Closure p :-> p
proextract Closure p a b
p = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. a -> b -> a
const (forall a b. (a -> b) -> a -> b
$ ()) forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b.
Closure p a b -> forall x. p (x -> a) (x -> b)
runClosure Closure p a b
p
  produplicate :: forall (p :: * -> * -> *).
Profunctor p =>
Closure p :-> Closure (Closure p)
produplicate (Closure forall x. p (x -> a) (x -> b)
p) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall x. p (x -> a) (x -> b)
p

instance Profunctor p => Closed (Closure p) where
  closed :: forall a b x. Closure p a b -> Closure p (x -> a) (x -> b)
closed Closure p a b
p = forall (p :: * -> * -> *) a b.
Closure p a b -> forall x. p (x -> a) (x -> b)
runClosure forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> t (t p)
produplicate Closure p a b
p

instance Strong p => Strong (Closure p) where
  first' :: forall a b c. Closure p a b -> Closure p (a, c) (b, c)
first' (Closure forall x. p (x -> a) (x -> b)
p) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall s a b. (s -> (a, b)) -> (s -> a, s -> b)
hither forall s a b. (s -> a, s -> b) -> s -> (a, b)
yon forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' forall x. p (x -> a) (x -> b)
p

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

hither :: (s -> (a,b)) -> (s -> a, s -> b)
hither :: forall s a b. (s -> (a, b)) -> (s -> a, s -> b)
hither s -> (a, b)
h = (forall a b. (a, b) -> a
fst forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. s -> (a, b)
h, forall a b. (a, b) -> b
snd forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. s -> (a, b)
h)

yon :: (s -> a, s -> b) -> s -> (a,b)
yon :: forall s a b. (s -> a, s -> b) -> s -> (a, b)
yon (s -> a, s -> b)
h s
s = (forall a b. (a, b) -> a
fst (s -> a, s -> b)
h s
s, forall a b. (a, b) -> b
snd (s -> a, s -> b)
h s
s)

instance Arrow p => Arrow (Closure p) where
  arr :: forall b c. (b -> c) -> Closure p b c
arr b -> c
f = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (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
.))
  first :: forall b c d. Closure p b c -> Closure p (b, d) (c, d)
first (Closure forall x. p (x -> b) (x -> c)
f) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall s a b. (s -> a, s -> b) -> s -> (a, b)
yon forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall x. p (x -> b) (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 (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall s a b. (s -> (a, b)) -> (s -> a, s -> b)
hither

instance ArrowLoop p => ArrowLoop (Closure p) where
  loop :: forall b d c. Closure p (b, d) (c, d) -> Closure p b c
loop (Closure forall x. p (x -> (b, d)) (x -> (c, d))
f) = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall s a b. (s -> (a, b)) -> (s -> a, s -> b)
hither 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 -> (b, d)) (x -> (c, d))
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall s a b. (s -> a, s -> b) -> s -> (a, b)
yon)

instance ArrowZero p => ArrowZero (Closure p) where
  zeroArrow :: forall b c. Closure p b c
zeroArrow = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow

instance ArrowPlus p => ArrowPlus (Closure p) where
  Closure forall x. p (x -> b) (x -> c)
f <+> :: forall b c. Closure p b c -> Closure p b c -> Closure p b c
<+> Closure forall x. p (x -> b) (x -> c)
g = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (forall x. p (x -> b) (x -> c)
f forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> forall x. p (x -> b) (x -> c)
g)

instance Profunctor p => Functor (Closure p a) where
  fmap :: forall a b. (a -> b) -> Closure p a a -> Closure p a b
fmap = forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap

instance (Profunctor p, Arrow p) => Applicative (Closure p a) where
  pure :: forall a. a -> Closure p a a
pure a
x = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b. a -> b -> a
const a
x)
  Closure p a (a -> b)
f <*> :: forall a b. Closure p a (a -> b) -> Closure p a a -> Closure p a b
<*> Closure p a a
g = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Closure p a (a -> b)
f forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Closure p a a
g)

instance (Profunctor p, ArrowPlus p) => Alternative (Closure p a) where
  empty :: forall a. Closure p a a
empty = forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow
  Closure p a a
f <|> :: forall a. Closure p a a -> Closure p a a -> Closure p a a
<|> Closure p a a
g = Closure p a a
f forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> Closure p a a
g

instance (Profunctor p, Arrow p, Semigroup b) => Semigroup (Closure p a b) where
  <> :: Closure p a b -> Closure p a b -> Closure p a b
(<>) = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Semigroup a => a -> a -> a
(<>)

instance (Profunctor p, Arrow p, Semigroup b, Monoid b) => Monoid (Closure p a b) where
  mempty :: Closure p a b
mempty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
#if !(MIN_VERSION_base(4,11,0))
  mappend = (<>)
#endif

-- |
-- @
-- 'close' '.' 'unclose' ≡ 'id'
-- 'unclose' '.' 'close' ≡ 'id'
-- @
close :: Closed p => (p :-> q) -> p :-> Closure q
close :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Closed p =>
(p :-> q) -> p :-> Closure q
close p :-> q
f p a b
p = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure forall a b. (a -> b) -> a -> b
$ p :-> q
f forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed p a b
p

-- |
-- @
-- 'close' '.' 'unclose' ≡ 'id'
-- 'unclose' '.' 'close' ≡ 'id'
-- @
unclose :: Profunctor q => (p :-> Closure q) -> p :-> q
unclose :: forall (q :: * -> * -> *) (p :: * -> * -> *).
Profunctor q =>
(p :-> Closure q) -> p :-> q
unclose p :-> Closure q
f p a b
p = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a b. a -> b -> a
const (forall a b. (a -> b) -> a -> b
$ ()) forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b.
Closure p a b -> forall x. p (x -> a) (x -> b)
runClosure forall a b. (a -> b) -> a -> b
$ p :-> Closure q
f p a b
p

--------------------------------------------------------------------------------
-- * Environment
--------------------------------------------------------------------------------

data Environment p a b where
  Environment :: ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b

instance Functor (Environment p a) where
  fmap :: forall a b. (a -> b) -> Environment p a a -> Environment p a b
fmap a -> b
f (Environment (z -> y) -> a
l p x y
m a -> z -> x
r) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (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
. (z -> y) -> a
l) p x y
m a -> z -> x
r

instance Profunctor (Environment p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Environment p b c -> Environment p a d
dimap a -> b
f c -> d
g (Environment (z -> y) -> c
l p x y
m b -> z -> x
r) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (c -> d
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (z -> y) -> c
l) p x y
m (b -> z -> x
r forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)
  lmap :: forall a b c. (a -> b) -> Environment p b c -> Environment p a c
lmap a -> b
f (Environment (z -> y) -> c
l p x y
m b -> z -> x
r) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (z -> y) -> c
l p x y
m (b -> z -> x
r forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
f)
  rmap :: forall b c a. (b -> c) -> Environment p a b -> Environment p a c
rmap b -> c
g (Environment (z -> y) -> b
l p x y
m a -> z -> x
r) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (b -> c
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (z -> y) -> b
l) p x y
m a -> z -> x
r
  q b c
w #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Environment p a b -> Environment p a c
#. Environment (z -> y) -> b
l p x y
m a -> z -> x
r = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (q b c
w forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. (z -> y) -> b
l) p x y
m a -> z -> x
r
  Environment (z -> y) -> c
l p x y
m b -> z -> x
r .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Environment p b c -> q a b -> Environment p a c
.# q a b
w = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (z -> y) -> c
l p x y
m (b -> z -> x
r forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# q a b
w)

instance ProfunctorFunctor Environment where
  promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Environment p :-> Environment q
promap p :-> q
f (Environment (z -> y) -> b
l p x y
m a -> z -> x
r) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (z -> y) -> b
l (p :-> q
f p x y
m) a -> z -> x
r

instance ProfunctorMonad Environment where
  proreturn :: forall (p :: * -> * -> *). Profunctor p => p :-> Environment p
proreturn p a b
p = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (forall a b. (a -> b) -> a -> b
$ ()) p a b
p forall a b. a -> b -> a
const
  projoin :: forall (p :: * -> * -> *).
Profunctor p =>
Environment (Environment p) :-> Environment p
projoin (Environment (z -> y) -> b
l (Environment (z -> y) -> y
m p x y
n x -> z -> x
o) a -> z -> x
p) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment ((z -> z -> y) -> b
lm forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b c. ((a, b) -> c) -> a -> b -> c
curry) p x y
n a -> (z, z) -> x
op where
    op :: a -> (z, z) -> x
op a
a (z
b, z
c) = x -> z -> x
o (a -> z -> x
p a
a z
b) z
c
    lm :: (z -> z -> y) -> b
lm z -> z -> y
zr = (z -> y) -> b
l ((z -> y) -> y
mforall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
.z -> z -> y
zr)

instance ProfunctorAdjunction Environment Closure where
  counit :: forall (p :: * -> * -> *).
Profunctor p =>
Environment (Closure p) :-> p
counit (Environment (z -> y) -> b
g (Closure forall x. p (x -> x) (x -> y)
p) a -> z -> x
f) = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> z -> x
f (z -> y) -> b
g forall x. p (x -> x) (x -> y)
p
  unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> Closure (Environment p)
unit p a b
p = forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id p a b
p forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

instance Closed (Environment p) where
  closed :: forall a b x. Environment p a b -> Environment p (x -> a) (x -> b)
closed (Environment (z -> y) -> b
l p x y
m a -> z -> x
r) = forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment ((z, x) -> y) -> x -> b
l' p x y
m (x -> a) -> (z, x) -> x
r' where
    r' :: (x -> a) -> (z, x) -> x
r' x -> a
wa (z
z,x
w) = a -> z -> x
r (x -> a
wa x
w) z
z
    l' :: ((z, x) -> y) -> x -> b
l' (z, x) -> y
zx2y x
x = (z -> y) -> b
l (\z
z -> (z, x) -> y
zx2y (z
z,x
x))