0 | ||| This module defines profunctor costrength with respect to a particular
  1 | ||| monoidal structure.
  2 | |||
  3 | ||| Since the homset profunctor (`Morphism`) is not costrong, very few
  4 | ||| profunctors implement this interface.
  5 | |||
  6 | ||| Unlike Haskell's profunctors library, `Costrong` and `Cochoice` are here
  7 | ||| special cases of the interface `GenCostrong`, which defines costrength with
  8 | ||| respect to an arbitrary tensor product. When writing implementations for
  9 | ||| a profunctor, `GenCostrong Pair` and `GenCostrong Either` should be used instead
 10 | ||| of `Costrong` and `Cochoice` respectively.
 11 | module Data.Profunctor.Costrong
 12 |
 13 | import Data.Morphisms
 14 | import Data.Tensor
 15 | import Data.Profunctor.Functor
 16 | import Data.Profunctor.Types
 17 |
 18 | %default total
 19 |
 20 |
 21 | ------------------------------------------------------------------------------
 22 | -- Costrength interface
 23 | ------------------------------------------------------------------------------
 24 |
 25 |
 26 | ||| Profunctor costrength with respect to a tensor product.
 27 | |||
 28 | ||| These constraints are not required by the interface, but the tensor product
 29 | ||| `ten` is generally expected to implement `(Tensor ten i, Symmetric ten)`.
 30 | |||
 31 | ||| Laws:
 32 | ||| * `costrongl = costrongr . dimap swap' swap'`
 33 | ||| * `costrongl . dimap unitr.rightToLeft unitr.leftToRight = id`
 34 | ||| * `costrongl . lmap (mapSnd f) = costrongl . rmap (mapSnd f)`
 35 | ||| * `costrongr . costrongr = costrongr . dimap assocl assocr`
 36 | |||
 37 | ||| @ ten The tensor product of the monoidal structure
 38 | public export
 39 | interface Profunctor p => GenCostrong (0 ten : Type -> Type -> Type) p where
 40 |   ||| The left action of a costrong profunctor.
 41 |   costrongl : p (a `ten` c) (b `ten` c) -> p a b
 42 |   ||| The right action of a costrong profunctor.
 43 |   costrongr : p (c `ten` a) (c `ten` b) -> p a b
 44 |
 45 |
 46 | ||| Profunctor costrength with respect to the product (`Pair`).
 47 | public export
 48 | Costrong : (p : Type -> Type -> Type) -> Type
 49 | Costrong = GenCostrong Pair
 50 |
 51 | ||| A special case of `costrongl` with constraint `Costrong`.
 52 | ||| This is useful if the typechecker has trouble inferring the tensor product.
 53 | public export
 54 | unfirst : Costrong p => p (a, c) (b, c) -> p a b
 55 | unfirst = costrongl {ten=Pair}
 56 |
 57 | ||| A special case of `costrongr` with constraint `Costrong`.
 58 | ||| This is useful if the typechecker has trouble inferring the tensor product.
 59 | public export
 60 | unsecond : Costrong p => p (c, a) (c, b) -> p a b
 61 | unsecond = costrongr {ten=Pair}
 62 |
 63 | ||| Profunctor costrength with respect to the coproduct (`Either`).
 64 | public export
 65 | Cochoice : (p : Type -> Type -> Type) -> Type
 66 | Cochoice = GenCostrong Either
 67 |
 68 | ||| A special case of `costrongl` with constraint `Cochoice`.
 69 | ||| This is useful if the typechecker has trouble inferring the tensor product.
 70 | public export
 71 | unleft : Cochoice p => p (Either a c) (Either b c) -> p a b
 72 | unleft = costrongl {ten=Either}
 73 |
 74 | ||| A special case of `costrongr` with constraint `Cochoice`.
 75 | ||| This is useful if the typechecker has trouble inferring the tensor product.
 76 | public export
 77 | unright : Cochoice p => p (Either c a) (Either c b) -> p a b
 78 | unright = costrongr {ten=Either}
 79 |
 80 |
 81 | ------------------------------------------------------------------------------
 82 | -- Implementations
 83 | ------------------------------------------------------------------------------
 84 |
 85 |
 86 | public export
 87 | GenCostrong Pair Tagged where
 88 |   costrongl (Tag (x,_)) = Tag x
 89 |   costrongr (Tag (_,x)) = Tag x
 90 |
 91 | public export
 92 | GenCostrong Either (Forget r) where
 93 |   costrongl (MkForget k) = MkForget (k . Left)
 94 |   costrongr (MkForget k) = MkForget (k . Right)
 95 |
 96 | public export
 97 | GenCostrong Pair (Coforget r) where
 98 |   costrongl (MkCoforget k) = MkCoforget (fst . k)
 99 |   costrongr (MkCoforget k) = MkCoforget (snd . k)
100 |
101 |
102 | ------------------------------------------------------------------------------
103 | -- Cotambara
104 | ------------------------------------------------------------------------------
105 |
106 |
107 | ||| The comonad generated by the reflective subcategory of profunctors that
108 | ||| implement `GenCostrong ten`.
109 | public export
110 | data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
111 |   MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b
112 |
113 | public export
114 | Profunctor (GenCotambara ten p) where
115 |   lmap f (MkCotambara n p) = MkCotambara n (lmap f p)
116 |   rmap f (MkCotambara n p) = MkCotambara n (rmap f p)
117 |   dimap f g (MkCotambara n p) = MkCotambara n (dimap f g p)
118 |
119 | public export
120 | ProfunctorFunctor (GenCotambara ten) where
121 |   promap f (MkCotambara n p) = MkCotambara (f . n) p
122 |
123 | public export
124 | GenCostrong ten (GenCotambara ten p) where
125 |   costrongl (MkCotambara @{costr} n p) = MkCotambara n (costrongl @{costr} p)
126 |   costrongr (MkCotambara @{costr} n p) = MkCotambara n (costrongr @{costr} p)
127 |
128 | public export
129 | ProfunctorComonad (GenCotambara ten) where
130 |   proextract (MkCotambara n p) = n p
131 |   produplicate (MkCotambara n p) = MkCotambara id (MkCotambara n p)
132 |
133 | public export
134 | Functor (GenCotambara ten p a) where
135 |   map = rmap
136 |
137 |
138 | ||| The comonad generated by the reflective subcategory of profunctors that
139 | ||| implement `Costrong`.
140 | |||
141 | ||| This is a special case of `GenCotambara`.
142 | public export
143 | Cotambara : (p : Type -> Type -> Type) -> Type -> Type -> Type
144 | Cotambara = GenCotambara Pair
145 |
146 | ||| The comonad generated by the reflective subcategory of profunctors that
147 | ||| implement `Cochoice`.
148 | |||
149 | ||| This is a special case of `GenCotambara`.
150 | public export
151 | CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
152 | CotambaraSum = GenCotambara Either
153 |
154 |
155 | public export
156 | cotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
157 | cotambara f = MkCotambara f
158 |
159 | public export
160 | uncotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
161 | uncotambara f p = proextract (f p)
162 |
163 |
164 | ------------------------------------------------------------------------------
165 | -- Copastro
166 | ------------------------------------------------------------------------------
167 |
168 |
169 | ||| The monad generated by the reflective subcategory of profunctors that
170 | ||| implement `GenCostrong ten`.
171 | public export
172 | record GenCopastro (ten, p : Type -> Type -> Type) a b where
173 |   constructor MkCopastro
174 |   runCopastro : forall q. GenCostrong ten q => p :-> q -> q a b
175 |
176 | public export
177 | Profunctor (GenCopastro ten p) where
178 |   dimap f g (MkCopastro h) = MkCopastro $ \n => dimap f g (h n)
179 |   lmap f (MkCopastro h) = MkCopastro $ \n => lmap f (h n)
180 |   rmap f (MkCopastro h) = MkCopastro $ \n => rmap f (h n)
181 |
182 | public export
183 | ProfunctorFunctor (GenCopastro ten) where
184 |   promap f (MkCopastro h) = MkCopastro $ \n => h (n . f)
185 |
186 | public export
187 | ProfunctorMonad (GenCopastro ten) where
188 |   propure p = MkCopastro ($ p)
189 |   projoin p = MkCopastro $ \x => runCopastro p (\y => runCopastro y x)
190 |
191 | public export
192 | GenCostrong ten (GenCopastro ten p) where
193 |   costrongl (MkCopastro h) = MkCopastro $ \n => costrongl {ten} (h n)
194 |   costrongr (MkCopastro h) = MkCopastro $ \n => costrongr {ten} (h n)
195 |
196 | public export
197 | ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where
198 |   prounit p = MkCotambara id (propure {t=GenCopastro ten} p)
199 |   procounit (MkCopastro h) = proextract (h id)
200 |
201 |
202 | ||| The monad generated by the reflective subcategory of profunctors that
203 | ||| implement `Costrong`.
204 | |||
205 | ||| This is a special case of `GenCopastro`.
206 | public export
207 | Copastro : (p : Type -> Type -> Type) -> Type -> Type -> Type
208 | Copastro = GenCopastro Pair
209 |
210 | ||| The monad generated by the reflective subcategory of profunctors that
211 | ||| implement `Cochoice`.
212 | |||
213 | ||| This is a special case of `GenCopastro`.
214 | public export
215 | CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
216 | CopastroSum = GenCopastro Either
217 |
218 |
219 | public export
220 | copastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q
221 | copastro f (MkCopastro h) = h f
222 |
223 | public export
224 | uncopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q
225 | uncopastro f x = f (MkCopastro ($ x))
226 |