0 | module Data.Profunctor.Cayley
 1 |
 2 | import Data.Profunctor
 3 | import Data.Profunctor.Costrong
 4 | import Data.Profunctor.Traversing
 5 | import Data.Profunctor.Mapping
 6 | import Data.Profunctor.Sieve
 7 |
 8 | %default total
 9 |
10 |
11 | -- NOTE: This may be better as a type synonym instead of a new type?
12 |
13 | ||| A profunctor lifted into a functor.
14 | public export
15 | record Cayley {0 k1,k2,k3 : Type} f (p : k1 -> k2 -> k3) a b where
16 |   constructor MkCayley
17 |   runCayley : f (p a b)
18 |
19 |
20 | public export
21 | Functor f => Profunctor p => Profunctor (Cayley f p) where
22 |   dimap f g (MkCayley p) = MkCayley (dimap f g <$> p)
23 |   lmap f (MkCayley p) = MkCayley (lmap f <$> p)
24 |   rmap g (MkCayley p) = MkCayley (rmap g <$> p)
25 |
26 | public export
27 | Functor f => ProfunctorFunctor (Cayley f) where
28 |   promap f (MkCayley p) = MkCayley (map f p)
29 |
30 | public export
31 | Monad m => ProfunctorMonad (Cayley m) where
32 |   propure = MkCayley . pure
33 |   projoin (MkCayley p) = MkCayley $ p >>= runCayley
34 |
35 | public export
36 | Functor f => GenStrong ten p => GenStrong ten (Cayley f p) where
37 |   strongl (MkCayley p) = MkCayley (strongl {ten} <$> p)
38 |   strongr (MkCayley p) = MkCayley (strongr {ten} <$> p)
39 |
40 | public export
41 | Functor f => GenCostrong ten p => GenCostrong ten (Cayley f p) where
42 |   costrongl (MkCayley p) = MkCayley (costrongl {ten} <$> p)
43 |   costrongr (MkCayley p) = MkCayley (costrongr {ten} <$> p)
44 |
45 | public export
46 | Functor f => Closed p => Closed (Cayley f p) where
47 |   closed (MkCayley p) = MkCayley (closed <$> p)
48 |
49 | public export
50 | Functor f => Traversing p => Traversing (Cayley f p) where
51 |   traverse' (MkCayley p) = MkCayley (traverse' <$> p)
52 |   wander f (MkCayley p) = MkCayley (wander f <$> p)
53 |
54 | public export
55 | Functor f => Mapping p => Mapping (Cayley f p) where
56 |   map' (MkCayley p) = MkCayley (map' <$> p)
57 |   roam f (MkCayley p) = MkCayley (roam f <$> p)
58 |
59 | public export
60 | Functor g => Sieve p f => Sieve (Cayley g p) (g . f) using Functor.Compose where
61 |   sieve (MkCayley p) x = ($ x) . sieve <$> p
62 |
63 |
64 | public export
65 | mapCayley : (forall x. f x -> g x) -> Cayley f p :-> Cayley g p
66 | mapCayley f (MkCayley p) = MkCayley (f p)
67 |