0 | module Data.Profunctor.Closed
  1 |
  2 | import Data.Morphisms
  3 | import Data.Profunctor.Types
  4 | import Data.Profunctor.Functor
  5 | import Data.Profunctor.Strong
  6 |
  7 | %default total
  8 |
  9 |
 10 | ------------------------------------------------------------------------------
 11 | -- Closed interface
 12 | ------------------------------------------------------------------------------
 13 |
 14 |
 15 | ||| Closed profunctors preserve the closed structure of a category.
 16 | |||
 17 | ||| Laws:
 18 | ||| * `lmap (. f) . closed = rmap (. f) . closed`
 19 | ||| * `closed . closed = dimap uncurry curry . closed`
 20 | ||| * `dimap const ($ ()) . closed = id`
 21 | public export
 22 | interface Profunctor p => Closed p where
 23 |   ||| The action of a closed profunctor.
 24 |   closed : p a b -> p (x -> a) (x -> b)
 25 |
 26 |
 27 | ------------------------------------------------------------------------------
 28 | -- Implementations
 29 | ------------------------------------------------------------------------------
 30 |
 31 |
 32 | public export
 33 | Closed Morphism where
 34 |   closed (Mor f) = Mor (f .)
 35 |
 36 | ||| A named implementation of `Closed` for function types.
 37 | ||| Use this to avoid having to use a type wrapper like `Morphism`.
 38 | public export
 39 | [Function] Closed (\a,b => a -> b) using Profunctor.Function where
 40 |   closed = (.)
 41 |
 42 | public export
 43 | Functor f => Closed (Costar f) where
 44 |   closed (MkCostar p) = MkCostar $ \f,x => p (map ($ x) f)
 45 |
 46 |
 47 | public export
 48 | curry' : Closed p => p (a, b) c -> p a (b -> c)
 49 | curry' = lmap (,) . closed
 50 |
 51 |
 52 | ------------------------------------------------------------------------------
 53 | -- Closure
 54 | ------------------------------------------------------------------------------
 55 |
 56 |
 57 | -- Helper functions for working with function types
 58 | hither : (s -> (a, b)) -> (s -> a, s -> b)
 59 | hither h = (fst . h, snd . h)
 60 |
 61 | yon : (s -> a, s -> b) -> s -> (a,b)
 62 | yon h s = (fst h s, snd h s)
 63 |
 64 |
 65 | ||| The comonad generated by the reflective subcategory of profunctors that
 66 | ||| implement `Closed`.
 67 | public export
 68 | record Closure p a b where
 69 |   constructor MkClosure
 70 |   runClosure : forall x. p (x -> a) (x -> b)
 71 |
 72 |
 73 | public export
 74 | Profunctor p => Profunctor (Closure p) where
 75 |   dimap f g (MkClosure p) = MkClosure $ dimap (f .) (g .) p
 76 |   lmap f (MkClosure p) = MkClosure $ lmap (f .) p
 77 |   rmap f (MkClosure p) = MkClosure $ rmap (f .) p
 78 |
 79 | public export
 80 | ProfunctorFunctor Closure where
 81 |   promap f (MkClosure p) = MkClosure (f p)
 82 |
 83 | public export
 84 | ProfunctorComonad Closure where
 85 |   proextract (MkClosure p) = dimap const ($ ()) p
 86 |   produplicate (MkClosure p) = MkClosure $ MkClosure $ dimap uncurry curry p
 87 |
 88 | public export
 89 | Strong p => GenStrong Pair (Closure p) where
 90 |   strongl (MkClosure p) = MkClosure $ dimap hither yon $ first p
 91 |   strongr (MkClosure p) = MkClosure $ dimap hither yon $ second p
 92 |
 93 | public export
 94 | Profunctor p => Closed (Closure p) where
 95 |   closed p = runClosure $ produplicate p
 96 |
 97 | public export
 98 | Profunctor p => Functor (Closure p a) where
 99 |   map = rmap
100 |
101 |
102 | public export
103 | close : Closed p => p :-> q -> p :-> Closure q
104 | close f p = MkClosure $ f $ closed p
105 |
106 | public export
107 | unclose : Profunctor q => p :-> Closure q -> p :-> q
108 | unclose f p = dimap const ($ ()) $ runClosure $ f p
109 |
110 |
111 | ------------------------------------------------------------------------------
112 | -- Environment
113 | ------------------------------------------------------------------------------
114 |
115 |
116 | ||| The monad generated by the reflective subcategory of profunctors that
117 | ||| implement `Closed`.
118 | public export
119 | data Environment : (p : Type -> Type -> Type) -> Type -> Type -> Type where
120 |   MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
121 |
122 |
123 | public export
124 | Profunctor (Environment p) where
125 |   dimap f g (MkEnv l m r) = MkEnv (g . l) m (r . f)
126 |   lmap f (MkEnv l m r) = MkEnv l m (r . f)
127 |   rmap g (MkEnv l m r) = MkEnv (g . l) m r
128 |
129 | public export
130 | ProfunctorFunctor Environment where
131 |   promap f (MkEnv l m r) = MkEnv l (f m) r
132 |
133 | public export
134 | ProfunctorMonad Environment where
135 |   propure p = MkEnv ($ ()) p const
136 |   projoin (MkEnv {x=x',y=y',z=z'} l' (MkEnv {x,y,z} l m r) r') = MkEnv (ll . curry) m rr
137 |     where
138 |       ll : (z' -> z -> y) -> b
139 |       ll zr = l' (l . zr)
140 |       rr : a -> (z', z) -> x
141 |       rr a (b, c) = r (r' a b) c
142 |
143 | public export
144 | ProfunctorAdjunction Environment Closure where
145 |   prounit p = MkClosure (MkEnv id p id)
146 |   procounit (MkEnv l (MkClosure x) r) = dimap r l x
147 |
148 | public export
149 | Closed (Environment p) where
150 |   closed {x=x'} (MkEnv {x,y,z} l m r) = MkEnv l' m r'
151 |     where
152 |       l' : ((z, x') -> y) -> x' -> b
153 |       l' f x = l (\z => f (z,x))
154 |       r' : (x' -> a) -> (z, x') -> x
155 |       r' f (z,x) = r (f x) z
156 |
157 | public export
158 | Profunctor p => Functor (Environment p a) where
159 |   map = rmap
160 |
161 |
162 | public export
163 | environment : Closed q => p :-> q -> Environment p :-> q
164 | environment f (MkEnv l m r) = dimap r l $ closed (f m)
165 |
166 | public export
167 | unenvironment : Environment p :-> q -> p :-> q
168 | unenvironment f p = f (MkEnv ($ ()) p const)
169 |