{-# 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) = (x -> b) -> Tagged (x -> a) (x -> b)
forall {k} (s :: k) b. b -> Tagged s b
Tagged (b -> x -> b
forall a b. a -> b -> a
const b
b)

instance Closed (->) where
  closed :: forall a b x. (a -> b) -> (x -> a) -> (x -> b)
closed = (a -> b) -> (x -> a) -> x -> b
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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) = (f (x -> a) -> x -> b) -> Costar f (x -> a) (x -> b)
forall {k} (f :: k -> *) (d :: k) c. (f d -> c) -> Costar f d c
Costar ((f (x -> a) -> x -> b) -> Costar f (x -> a) (x -> b))
-> (f (x -> a) -> x -> b) -> Costar f (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ \f (x -> a)
fxa x
x -> f a -> b
fab (((x -> a) -> a) -> f (x -> a) -> f a
forall a b. (a -> b) -> f a -> f 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) 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) = (f (x -> a) -> x -> b) -> Cokleisli f (x -> a) (x -> b)
forall {k} (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
Cokleisli ((f (x -> a) -> x -> b) -> Cokleisli f (x -> a) (x -> b))
-> (f (x -> a) -> x -> b) -> Cokleisli f (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ \f (x -> a)
fxa x
x -> f a -> b
fab (((x -> a) -> a) -> f (x -> a) -> f a
forall a b. (a -> b) -> f a -> f 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) 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) = ((x -> a) -> f (x -> b)) -> Star f (x -> a) (x -> b)
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (((x -> a) -> f (x -> b)) -> Star f (x -> a) (x -> b))
-> ((x -> a) -> f (x -> b)) -> Star f (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ \x -> a
xa -> (x -> f b) -> f (x -> b)
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: * -> *) a. Functor f => f (f a) -> f (f a)
distribute ((x -> f b) -> f (x -> b)) -> (x -> f b) -> f (x -> b)
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) = ((x -> a) -> f (x -> b)) -> Kleisli f (x -> a) (x -> b)
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli (((x -> a) -> f (x -> b)) -> Kleisli f (x -> a) (x -> b))
-> ((x -> a) -> f (x -> b)) -> Kleisli f (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ \x -> a
xa -> (x -> f b) -> f (x -> b)
forall (g :: * -> *) (f :: * -> *) a.
(Distributive g, Functor f) =>
f (g a) -> g (f a)
forall (f :: * -> *) a. Functor f => f (f a) -> f (f a)
distribute ((x -> f b) -> f (x -> b)) -> (x -> f b) -> f (x -> b)
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) = p (x -> a) (x -> b)
-> q (x -> a) (x -> b) -> Product p q (x -> a) (x -> b)
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 (p a b -> p (x -> a) (x -> b)
forall a b x. p a b -> p (x -> a) (x -> b)
forall (p :: * -> * -> *) a b x.
Closed p =>
p a b -> p (x -> a) (x -> b)
closed p a b
p) (q a b -> q (x -> a) (x -> b)
forall a b x. q a b -> q (x -> a) (x -> b)
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) = p (x -> a) (x -> b) -> Sum p q (x -> a) (x -> b)
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (p a b -> p (x -> a) (x -> b)
forall a b x. p a b -> p (x -> a) (x -> b)
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) = q (x -> a) (x -> b) -> Sum p q (x -> a) (x -> b)
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (q a b -> q (x -> a) (x -> b)
forall a b x. q a b -> q (x -> a) (x -> b)
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) = f (p (x -> a) (x -> b)) -> Tannen f p (x -> a) (x -> b)
forall {k} {k1} {k2} (f :: k -> *) (p :: k1 -> k2 -> k) (a :: k1)
       (b :: k2).
f (p a b) -> Tannen f p a b
Tannen ((p a b -> p (x -> a) (x -> b))
-> f (p a b) -> f (p (x -> a) (x -> b))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap p a b -> p (x -> a) (x -> b)
forall a b x. p a b -> p (x -> a) (x -> b)
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' = (a -> b -> (a, b)) -> p (b -> (a, b)) (b -> c) -> p a (b -> c)
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 (,) (p (b -> (a, b)) (b -> c) -> p a (b -> c))
-> (p (a, b) c -> p (b -> (a, b)) (b -> c))
-> p (a, b) c
-> p a (b -> c)
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p (a, b) c -> p (b -> (a, b)) (b -> c)
forall a b x. p a b -> p (x -> a) (x -> b)
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 x. p (x -> a) (x -> d)) -> Closure p a d
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> a) (x -> d)) -> Closure p a d)
-> (forall x. p (x -> a) (x -> d)) -> Closure p a d
forall a b. (a -> b) -> a -> b
$ ((x -> a) -> x -> b)
-> ((x -> c) -> x -> d)
-> p (x -> b) (x -> c)
-> p (x -> a) (x -> d)
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 ((a -> b) -> (x -> a) -> x -> b
forall a b. (a -> b) -> (x -> a) -> x -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ((c -> d) -> (x -> c) -> x -> d
forall a b. (a -> b) -> (x -> a) -> x -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g) p (x -> b) (x -> c)
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 x. p (x -> a) (x -> c)) -> Closure p a c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> a) (x -> c)) -> Closure p a c)
-> (forall x. p (x -> a) (x -> c)) -> Closure p a c
forall a b. (a -> b) -> a -> b
$ ((x -> a) -> x -> b) -> p (x -> b) (x -> c) -> p (x -> a) (x -> c)
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) -> (x -> a) -> x -> b
forall a b. (a -> b) -> (x -> a) -> x -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) p (x -> b) (x -> c)
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 x. p (x -> a) (x -> c)) -> Closure p a c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> a) (x -> c)) -> Closure p a c)
-> (forall x. p (x -> a) (x -> c)) -> Closure p a c
forall a b. (a -> b) -> a -> b
$ ((x -> b) -> x -> c) -> p (x -> a) (x -> b) -> p (x -> a) (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) -> (x -> b) -> x -> c
forall a b. (a -> b) -> (x -> a) -> x -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c
f) p (x -> a) (x -> b)
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 x. p (x -> a) (x -> c)) -> Closure p a c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> a) (x -> c)) -> Closure p a c)
-> (forall x. p (x -> a) (x -> c)) -> Closure p a c
forall a b. (a -> b) -> a -> b
$ (b -> c) -> (x -> b) -> x -> c
forall a b. (a -> b) -> (x -> a) -> x -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((c -> c) -> b -> c
forall a b. Coercible a b => a -> b
coerce (c -> c
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id :: c -> c) :: b -> c) ((x -> b) -> x -> c) -> p (x -> a) (x -> b) -> p (x -> a) (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
#. p (x -> a) (x -> b)
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 x. p (x -> a) (x -> c)) -> Closure p a c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> a) (x -> c)) -> Closure p a c)
-> (forall x. p (x -> a) (x -> c)) -> Closure p a c
forall a b. (a -> b) -> a -> b
$ p (x -> b) (x -> c)
forall x. p (x -> b) (x -> c)
p p (x -> b) (x -> c) -> ((x -> a) -> x -> b) -> p (x -> a) (x -> c)
forall a b c (q :: * -> * -> *).
Coercible b a =>
p b c -> q a b -> p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible b a) =>
p b c -> q a b -> p a c
.# (a -> b) -> (x -> a) -> x -> b
forall a b. (a -> b) -> (x -> a) -> x -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> a -> b
forall a b. Coercible a b => a -> b
coerce (b -> b
forall a. a -> a
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 x. q (x -> a) (x -> b)) -> Closure q a b
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (p (x -> a) (x -> b) -> q (x -> a) (x -> b)
p :-> q
f p (x -> a) (x -> b)
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 = (a -> () -> a)
-> ((() -> b) -> b) -> p (() -> a) (() -> b) -> p a b
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 a -> () -> a
forall a b. a -> b -> a
const ((() -> b) -> () -> b
forall a b. (a -> b) -> a -> b
$ ()) (p (() -> a) (() -> b) -> p a b) -> p (() -> a) (() -> b) -> p a b
forall a b. (a -> b) -> a -> b
$ Closure p a b -> forall x. p (x -> a) (x -> 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 x. Closure p (x -> a) (x -> b)) -> Closure (Closure p) a b
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. Closure p (x -> a) (x -> b))
 -> Closure (Closure p) a b)
-> (forall x. Closure p (x -> a) (x -> b))
-> Closure (Closure p) a b
forall a b. (a -> b) -> a -> b
$ (forall x. p (x -> x -> a) (x -> x -> b))
-> Closure p (x -> a) (x -> b)
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> x -> a) (x -> x -> b))
 -> Closure p (x -> a) (x -> b))
-> (forall x. p (x -> x -> a) (x -> x -> b))
-> Closure p (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ ((x -> x -> a) -> (x, x) -> a)
-> (((x, x) -> b) -> x -> x -> b)
-> p ((x, x) -> a) ((x, x) -> b)
-> p (x -> x -> a) (x -> x -> b)
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 (x -> x -> a) -> (x, x) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((x, x) -> b) -> x -> x -> b
forall a b c. ((a, b) -> c) -> a -> b -> c
curry p ((x, x) -> a) ((x, x) -> b)
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 = Closure (Closure p) a b -> forall x. Closure p (x -> a) (x -> b)
forall (p :: * -> * -> *) a b.
Closure p a b -> forall x. p (x -> a) (x -> b)
runClosure (Closure (Closure p) a b -> forall x. Closure p (x -> a) (x -> b))
-> Closure (Closure p) a b -> forall x. Closure p (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ Closure p a b -> Closure (Closure p) a b
Closure p :-> Closure (Closure p)
forall (p :: * -> * -> *).
Profunctor p =>
Closure p :-> Closure (Closure p)
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 x. p (x -> (a, c)) (x -> (b, c)))
-> Closure p (a, c) (b, c)
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> (a, c)) (x -> (b, c)))
 -> Closure p (a, c) (b, c))
-> (forall x. p (x -> (a, c)) (x -> (b, c)))
-> Closure p (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ ((x -> (a, c)) -> (x -> a, x -> c))
-> ((x -> b, x -> c) -> x -> (b, c))
-> p (x -> a, x -> c) (x -> b, x -> c)
-> p (x -> (a, c)) (x -> (b, 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 (x -> (a, c)) -> (x -> a, x -> c)
forall s a b. (s -> (a, b)) -> (s -> a, s -> b)
hither (x -> b, x -> c) -> x -> (b, c)
forall s a b. (s -> a, s -> b) -> s -> (a, b)
yon (p (x -> a, x -> c) (x -> b, x -> c)
 -> p (x -> (a, c)) (x -> (b, c)))
-> p (x -> a, x -> c) (x -> b, x -> c)
-> p (x -> (a, c)) (x -> (b, c))
forall a b. (a -> b) -> a -> b
$ p (x -> a) (x -> b) -> p (x -> a, x -> c) (x -> b, x -> c)
forall a b c. p a b -> p (a, c) (b, c)
forall (p :: * -> * -> *) a b c.
Strong p =>
p a b -> p (a, c) (b, c)
first' p (x -> a) (x -> b)
forall x. p (x -> a) (x -> b)
p

instance Category p => Category (Closure p) where
  id :: forall a. Closure p a a
id = (forall x. p (x -> a) (x -> a)) -> Closure p a a
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure p (x -> a) (x -> a)
forall a. p a a
forall x. p (x -> a) (x -> a)
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 x. p (x -> a) (x -> c)) -> Closure p a c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (p (x -> b) (x -> c)
forall x. p (x -> b) (x -> c)
p p (x -> b) (x -> c) -> p (x -> a) (x -> b) -> p (x -> a) (x -> c)
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 -> a) (x -> b)
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 = ((a, b) -> a
forall a b. (a, b) -> a
fst ((a, b) -> a) -> (s -> (a, b)) -> s -> a
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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, (a, b) -> b
forall a b. (a, b) -> b
snd ((a, b) -> b) -> (s -> (a, b)) -> s -> b
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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 = ((s -> a, s -> b) -> s -> a
forall a b. (a, b) -> a
fst (s -> a, s -> b)
h s
s, (s -> a, s -> b) -> s -> b
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 x. p (x -> b) (x -> c)) -> Closure p b c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (((x -> b) -> x -> c) -> p (x -> b) (x -> c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b -> c
f (b -> c) -> (x -> b) -> x -> c
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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 x. p (x -> (b, d)) (x -> (c, d)))
-> Closure p (b, d) (c, d)
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> (b, d)) (x -> (c, d)))
 -> Closure p (b, d) (c, d))
-> (forall x. p (x -> (b, d)) (x -> (c, d)))
-> Closure p (b, d) (c, d)
forall a b. (a -> b) -> a -> b
$ ((x -> c, x -> d) -> x -> (c, d))
-> p (x -> c, x -> d) (x -> (c, d))
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (x -> c, x -> d) -> x -> (c, d)
forall s a b. (s -> a, s -> b) -> s -> (a, b)
yon p (x -> c, x -> d) (x -> (c, d))
-> p (x -> (b, d)) (x -> c, x -> d)
-> p (x -> (b, d)) (x -> (c, d))
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 -> b) (x -> c) -> p (x -> b, x -> d) (x -> c, x -> d)
forall b c d. p b c -> p (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first p (x -> b) (x -> c)
forall x. p (x -> b) (x -> c)
f p (x -> b, x -> d) (x -> c, x -> d)
-> p (x -> (b, d)) (x -> b, x -> d)
-> p (x -> (b, d)) (x -> c, x -> d)
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
. ((x -> (b, d)) -> (x -> b, x -> d))
-> p (x -> (b, d)) (x -> b, x -> d)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (x -> (b, d)) -> (x -> b, x -> d)
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 x. p (x -> b) (x -> c)) -> Closure p b c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. p (x -> b) (x -> c)) -> Closure p b c)
-> (forall x. p (x -> b) (x -> c)) -> Closure p b c
forall a b. (a -> b) -> a -> b
$ p (x -> b, x -> d) (x -> c, x -> d) -> p (x -> b) (x -> c)
forall b d c. p (b, d) (c, d) -> p b c
forall (a :: * -> * -> *) b d c.
ArrowLoop a =>
a (b, d) (c, d) -> a b c
loop (((x -> (c, d)) -> (x -> c, x -> d))
-> p (x -> (c, d)) (x -> c, x -> d)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (x -> (c, d)) -> (x -> c, x -> d)
forall s a b. (s -> (a, b)) -> (s -> a, s -> b)
hither p (x -> (c, d)) (x -> c, x -> d)
-> p (x -> b, x -> d) (x -> (c, d))
-> p (x -> b, x -> d) (x -> c, x -> d)
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 -> (b, d)) (x -> (c, d))
forall x. p (x -> (b, d)) (x -> (c, d))
f p (x -> (b, d)) (x -> (c, d))
-> p (x -> b, x -> d) (x -> (b, d))
-> p (x -> b, x -> d) (x -> (c, d))
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
. ((x -> b, x -> d) -> x -> (b, d))
-> p (x -> b, x -> d) (x -> (b, d))
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (x -> b, x -> d) -> x -> (b, d)
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 x. p (x -> b) (x -> c)) -> Closure p b c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure p (x -> b) (x -> c)
forall x. p (x -> b) (x -> c)
forall b c. p b c
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 x. p (x -> b) (x -> c)) -> Closure p b c
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (p (x -> b) (x -> c)
forall x. p (x -> b) (x -> c)
f p (x -> b) (x -> c) -> p (x -> b) (x -> c) -> p (x -> b) (x -> c)
forall b c. p b c -> p b c -> p b c
forall (a :: * -> * -> *) b c.
ArrowPlus a =>
a b c -> a b c -> a b c
<+> p (x -> b) (x -> 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 = (a -> b) -> Closure p a a -> Closure p a b
forall b c a. (b -> c) -> Closure p a b -> Closure p a c
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 = (a -> a) -> Closure p a a
forall b c. (b -> c) -> Closure p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (a -> a -> a
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 = ((a -> b, a) -> b) -> Closure p (a -> b, a) b
forall b c. (b -> c) -> Closure p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (((a -> b) -> a -> b) -> (a -> b, a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> b) -> a -> b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) Closure p (a -> b, a) b -> Closure p a (a -> b, a) -> Closure p a b
forall b c a. Closure p b c -> Closure p a b -> Closure 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
. (Closure p a (a -> b)
f Closure p a (a -> b) -> Closure p a a -> Closure p a (a -> b, a)
forall b c c'.
Closure p b c -> Closure p b c' -> Closure p b (c, c')
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 = Closure p a a
forall b c. Closure p b c
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 Closure p a a -> Closure p a a -> Closure p a a
forall b c. Closure p b c -> Closure p b c -> Closure p b c
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
(<>) = (b -> b -> b) -> Closure p a b -> Closure p a b -> Closure p a b
forall a b c.
(a -> b -> c) -> Closure p a a -> Closure p a b -> Closure p a c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> b -> b
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 = b -> Closure p a b
forall a. a -> Closure p a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
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 x. q (x -> a) (x -> b)) -> Closure q a b
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure ((forall x. q (x -> a) (x -> b)) -> Closure q a b)
-> (forall x. q (x -> a) (x -> b)) -> Closure q a b
forall a b. (a -> b) -> a -> b
$ p (x -> a) (x -> b) -> q (x -> a) (x -> b)
p :-> q
f (p (x -> a) (x -> b) -> q (x -> a) (x -> b))
-> p (x -> a) (x -> b) -> q (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ p a b -> p (x -> a) (x -> b)
forall a b x. p a b -> p (x -> a) (x -> 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 = (a -> () -> a)
-> ((() -> b) -> b) -> q (() -> a) (() -> b) -> q a b
forall a b c d. (a -> b) -> (c -> d) -> q b c -> q a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> () -> a
forall a b. a -> b -> a
const ((() -> b) -> () -> b
forall a b. (a -> b) -> a -> b
$ ()) (q (() -> a) (() -> b) -> q a b) -> q (() -> a) (() -> b) -> q a b
forall a b. (a -> b) -> a -> b
$ Closure q a b -> forall x. q (x -> a) (x -> b)
forall (p :: * -> * -> *) a b.
Closure p a b -> forall x. p (x -> a) (x -> b)
runClosure (Closure q a b -> forall x. q (x -> a) (x -> b))
-> Closure q a b -> forall x. q (x -> a) (x -> b)
forall a b. (a -> b) -> a -> b
$ p a b -> Closure q 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) = ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (a -> b
f (a -> b) -> ((z -> y) -> a) -> (z -> y) -> b
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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) = ((z -> y) -> d) -> p x y -> (a -> z -> x) -> Environment p a d
forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (c -> d
g (c -> d) -> ((z -> y) -> c) -> (z -> y) -> d
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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 (b -> z -> x) -> (a -> b) -> a -> z -> x
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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) = ((z -> y) -> c) -> p x y -> (a -> z -> x) -> Environment p a c
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 (b -> z -> x) -> (a -> b) -> a -> z -> x
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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) = ((z -> y) -> c) -> p x y -> (a -> z -> x) -> Environment p a c
forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (b -> c
g (b -> c) -> ((z -> y) -> b) -> (z -> y) -> c
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
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 = ((z -> y) -> c) -> p x y -> (a -> z -> x) -> Environment p a c
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 q b c -> ((z -> y) -> b) -> (z -> y) -> c
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> (a -> b) -> a -> c
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 = ((z -> y) -> c) -> p x y -> (a -> z -> x) -> Environment p a c
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 (b -> z -> x) -> q a b -> a -> z -> x
forall a b c (q :: * -> * -> *).
Coercible b a =>
(b -> c) -> q a b -> a -> c
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) = ((z -> y) -> b) -> q x y -> (a -> z -> x) -> Environment q a b
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 x y -> q x y
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 = ((() -> b) -> b) -> p a b -> (a -> () -> a) -> Environment p a b
forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment ((() -> b) -> () -> b
forall a b. (a -> b) -> a -> b
$ ()) p a b
p a -> () -> a
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) = (((z, z) -> y) -> b)
-> p x y -> (a -> (z, z) -> x) -> Environment p a b
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 ((z -> z -> y) -> b)
-> (((z, z) -> y) -> z -> z -> y) -> ((z, z) -> y) -> b
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((z, z) -> y) -> z -> z -> y
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
m((z -> y) -> y) -> (z -> z -> y) -> z -> y
forall a b x. (a -> b) -> (x -> a) -> (x -> b)
forall {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) = (a -> z -> x) -> ((z -> y) -> b) -> p (z -> x) (z -> y) -> p a b
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 a -> z -> x
f (z -> y) -> b
g p (z -> x) (z -> y)
forall x. p (x -> x) (x -> y)
p
  unit :: forall (p :: * -> * -> *).
Profunctor p =>
p :-> Closure (Environment p)
unit p a b
p = (forall x. Environment p (x -> a) (x -> b))
-> Closure (Environment p) a b
forall (p :: * -> * -> *) a b.
(forall x. p (x -> a) (x -> b)) -> Closure p a b
Closure (((x -> b) -> x -> b)
-> p a b -> ((x -> a) -> x -> a) -> Environment p (x -> a) (x -> b)
forall z y b (p :: * -> * -> *) x a.
((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
Environment (x -> b) -> x -> b
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id p a b
p (x -> a) -> x -> a
forall a. a -> a
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) = (((z, x) -> y) -> x -> b)
-> p x y
-> ((x -> a) -> (z, x) -> x)
-> Environment p (x -> a) (x -> b)
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))