8 | module Data.Profunctor.Strong
10 | import Data.Morphisms
12 | import Data.Profunctor.Functor
13 | import Data.Profunctor.Types
36 | interface Profunctor p => GenStrong (0 ten : Type -> Type -> Type) p where
38 | strongl : p a b -> p (a `ten` c) (b `ten` c)
40 | strongr : p a b -> p (c `ten` a) (c `ten` b)
45 | Strong : (p : Type -> Type -> Type) -> Type
46 | Strong = GenStrong Pair
52 | first : Strong p => p a b -> p (a, c) (b, c)
53 | first = strongl {ten=Pair}
59 | second : Strong p => p a b -> p (c, a) (c, b)
60 | second = strongr {ten=Pair}
64 | Choice : (p : Type -> Type -> Type) -> Type
65 | Choice = GenStrong Either
71 | left : Choice p => p a b -> p (Either a c) (Either b c)
72 | left = strongl {ten=Either}
78 | right : Choice p => p a b -> p (Either c a) (Either c b)
79 | right = strongr {ten=Either}
83 | uncurry' : Strong p => p a (b -> c) -> p (a, b) c
84 | uncurry' = rmap (uncurry id) . first
87 | strong : Strong p => (a -> b -> c) -> p a b -> p a c
88 | strong f = dimap dup (uncurry $
flip f) . first
97 | Bifunctor ten => GenStrong ten Morphism where
98 | strongl (Mor f) = Mor (mapFst f)
99 | strongr (Mor f) = Mor (mapSnd f)
104 | [Function] Bifunctor ten => GenStrong ten (\a,b => a -> b)
105 | using Profunctor.Function where
110 | Functor f => GenStrong Pair (Kleislimorphism f) where
111 | strongl (Kleisli f) = Kleisli $
\(a,c) => (,c) <$> f a
112 | strongr (Kleisli f) = Kleisli $
\(c,a) => (c,) <$> f a
115 | Applicative f => GenStrong Either (Kleislimorphism f) where
116 | strongl (Kleisli f) = Kleisli $
either (map Left . f) (pure . Right)
117 | strongr (Kleisli f) = Kleisli $
either (pure . Left) (map Right . f)
120 | Functor f => GenStrong Pair (Star f) where
121 | strongl (MkStar f) = MkStar $
\(a,c) => (,c) <$> f a
122 | strongr (MkStar f) = MkStar $
\(c,a) => (c,) <$> f a
125 | Applicative f => GenStrong Either (Star f) where
126 | strongl (MkStar f) = MkStar $
either (map Left . f) (pure . Right)
127 | strongr (MkStar f) = MkStar $
either (pure . Left) (map Right . f)
130 | GenStrong Either Tagged where
131 | strongl (Tag x) = Tag (Left x)
132 | strongr (Tag x) = Tag (Right x)
135 | GenStrong Pair (Forget r) where
136 | strongl (MkForget k) = MkForget (k . fst)
137 | strongr (MkForget k) = MkForget (k . snd)
140 | Monoid r => GenStrong Either (Forget r) where
141 | strongl (MkForget k) = MkForget (either k (const neutral))
142 | strongr (MkForget k) = MkForget (either (const neutral) k)
145 | GenStrong Either (Coforget r) where
146 | strongl (MkCoforget k) = MkCoforget (Left . k)
147 | strongr (MkCoforget k) = MkCoforget (Right . k)
158 | record GenTambara (ten, p : Type -> Type -> Type) a b where
159 | constructor MkTambara
160 | runTambara : forall c. p (a `ten` c) (b `ten` c)
163 | Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where
164 | dimap f g (MkTambara p) = MkTambara $
dimap (mapFst f) (mapFst g) p
167 | ProfunctorFunctor (GenTambara ten) where
168 | promap f (MkTambara p) = MkTambara (f p)
171 | Tensor ten i => ProfunctorComonad (GenTambara ten) where
172 | proextract (MkTambara p) = dimap unitr.rightToLeft unitr.leftToRight p
173 | produplicate (MkTambara p) = MkTambara $
MkTambara $
dimap assocr assocl p
176 | Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where
177 | strongl (MkTambara p) = MkTambara $
dimap assocr assocl p
178 | strongr (MkTambara p) = MkTambara $
dimap (assocr . mapFst swap')
179 | (mapFst swap' . assocl) p
182 | Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where
191 | Tambara : (p : Type -> Type -> Type) -> Type -> Type -> Type
192 | Tambara = GenTambara Pair
199 | TambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
200 | TambaraSum = GenTambara Either
204 | tambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q
205 | tambara @{gs} f x = MkTambara $
f $
strongl @{gs} x
208 | untambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q
209 | untambara f x = dimap unitr.rightToLeft unitr.leftToRight $
runTambara $
f x
220 | data GenPastro : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
221 | MkPastro : (y `ten` z -> b) -> p x y -> (a -> x `ten` z) -> GenPastro ten p a b
225 | Profunctor (GenPastro ten p) where
226 | dimap f g (MkPastro l m r) = MkPastro (g . l) m (r . f)
227 | lmap f (MkPastro l m r) = MkPastro l m (r . f)
228 | rmap g (MkPastro l m r) = MkPastro (g . l) m r
231 | ProfunctorFunctor (GenPastro ten) where
232 | promap f (MkPastro l m r) = MkPastro l (f m) r
235 | (Tensor ten i, Symmetric ten) => ProfunctorMonad (GenPastro ten) where
236 | propure x = MkPastro unitr.leftToRight x unitr.rightToLeft
237 | projoin (MkPastro {x=x',y=y',z=z'} l' (MkPastro {x,y,z} l m r) r') = MkPastro ll m rr
239 | ll : y `ten` (z' `ten` z) -> b
240 | ll = l' . mapFst l . assocl . mapSnd swap'
242 | rr : a -> x `ten` (z' `ten` z)
243 | rr = mapSnd swap' . assocr . mapFst r . r'
246 | ProfunctorAdjunction (GenPastro ten) (GenTambara ten) where
247 | prounit x = MkTambara (MkPastro id x id)
248 | procounit (MkPastro l (MkTambara x) r) = dimap r l x
251 | (Associative ten, Symmetric ten) => GenStrong ten (GenPastro ten p) where
252 | strongl (MkPastro {x,y,z} l m r) = MkPastro l' m r'
254 | l' : y `ten` (z `ten` c) -> b `ten` c
255 | l' = mapFst l . assocl
256 | r' : a `ten` c -> x `ten` (z `ten` c)
257 | r' = assocr . mapFst r
258 | strongr (MkPastro {x,y,z} l m r) = MkPastro l' m r'
260 | l' : y `ten` (c `ten` z) -> c `ten` b
261 | l' = swap' . mapFst l . assocl . mapSnd swap'
262 | r' : c `ten` a -> x `ten` (c `ten` z)
263 | r' = mapSnd swap' . assocr . mapFst r . swap'
271 | Pastro : (p : Type -> Type -> Type) -> Type -> Type -> Type
272 | Pastro = GenPastro Pair
279 | PastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
280 | PastroSum = GenPastro Either
284 | pastro : GenStrong ten q => p :-> q -> GenPastro ten p :-> q
285 | pastro @{gs} f (MkPastro l m r) = dimap r l (strongl @{gs} (f m))
288 | unpastro : Tensor ten i => GenPastro ten p :-> q -> p :-> q
289 | unpastro f x = f (MkPastro unitr.leftToRight x unitr.rightToLeft)