0 | module Data.Profunctor.Mapping
  1 |
  2 | import Data.Morphisms
  3 | import Data.Tensor
  4 | import Data.Profunctor
  5 | import Data.Profunctor.Traversing
  6 |
  7 | %default total
  8 |
  9 |
 10 | functor : Functor (\a => (a -> b) -> t)
 11 | functor = MkFunctor (\f => (. (. f)))
 12 |
 13 | ------------------------------------------------------------------------------
 14 | -- Mapping interface
 15 | ------------------------------------------------------------------------------
 16 |
 17 |
 18 | ||| The interface of profunctors that implement `roam`.
 19 | |||
 20 | ||| Laws:
 21 | ||| * `map' . lmap f = lmap (map f) . map'`
 22 | ||| * `map' . rmap f = rmap (map f) . map'`
 23 | ||| * `map' . map' = map' @{Compose}`
 24 | ||| * `dimap Id runIdentity . map' = id`
 25 | public export
 26 | interface (Traversing p, Closed p) => Mapping p where
 27 |   map' : Functor f => p a b -> p (f a) (f b)
 28 |   map' = roam map
 29 |
 30 |   roam : ((a -> b) -> s -> t) -> p a b -> p s t
 31 |   roam f = dimap (flip f) ($ id) . map' @{%search} @{functor}
 32 |
 33 |
 34 | ------------------------------------------------------------------------------
 35 | -- Implementations
 36 | ------------------------------------------------------------------------------
 37 |
 38 |
 39 | public export
 40 | Mapping Morphism where
 41 |   map' (Mor f) = Mor (map f)
 42 |   roam f (Mor x) = Mor (f x)
 43 |
 44 | ||| A named implementation of `Mapping` for function types.
 45 | ||| Use this to avoid having to use a type wrapper like `Morphism`.
 46 | public export
 47 | [Function] Mapping (\a,b => a -> b)
 48 |     using Traversing.Function Closed.Function where
 49 |   map' = map
 50 |   roam = id
 51 |
 52 |
 53 | ------------------------------------------------------------------------------
 54 | -- CofreeMapping
 55 | ------------------------------------------------------------------------------
 56 |
 57 |
 58 | ||| The comonad generated by the reflective subcategory of profunctors that
 59 | ||| implement `Mapping`.
 60 | public export
 61 | record CofreeMapping p a b where
 62 |   constructor MkCFM
 63 |   runCFM : forall f. Functor f => p (f a) (f b)
 64 |
 65 | public export
 66 | Profunctor p => Profunctor (CofreeMapping p) where
 67 |   lmap f (MkCFM p) = MkCFM (lmap (map f) p)
 68 |   rmap f (MkCFM p) = MkCFM (rmap (map f) p)
 69 |   dimap f g (MkCFM p) = MkCFM (dimap (map f) (map g) p)
 70 |
 71 | public export
 72 | Profunctor p => Functor (CofreeMapping p a) where
 73 |   map = rmap
 74 |
 75 | public export
 76 | ProfunctorFunctor CofreeMapping where
 77 |   promap f (MkCFM p) = MkCFM (f p)
 78 |
 79 | public export
 80 | ProfunctorComonad CofreeMapping where
 81 |   proextract (MkCFM p) = p @{FunctorId}
 82 |   produplicate (MkCFM p) = MkCFM $ MkCFM $ p @{Compose}
 83 |
 84 | public export
 85 | Symmetric ten => Profunctor p => GenStrong ten (CofreeMapping p) where
 86 |   strongr (MkCFM p) = MkCFM (p @{Compose {g=ten c} @{%search} @{MkFunctor mapSnd}})
 87 |   strongl (MkCFM p) = MkCFM (p @{Compose {g=(`ten` c)} @{%search} @{MkFunctor mapFst}})
 88 |
 89 | public export
 90 | Profunctor p => Closed (CofreeMapping p) where
 91 |   closed (MkCFM p) = MkCFM (p @{Compose {g = \b => x -> b} @{%search} @{MkFunctor (.)}})
 92 |
 93 | roamCofree : Profunctor p => ((a -> b) -> s -> t) -> CofreeMapping p a b -> CofreeMapping p s t
 94 | roamCofree f (MkCFM p) = MkCFM $ dimap (map (flip f)) (map ($ id)) $
 95 |       p @{Compose @{%search} @{functor}}
 96 |
 97 | public export
 98 | Profunctor p => Traversing (CofreeMapping p) where
 99 |   traverse' (MkCFM p) = MkCFM (p @{Compose})
100 |   wander f = roamCofree $ f @{ApplicativeId}
101 |
102 | public export
103 | Profunctor p => Mapping (CofreeMapping p) where
104 |   map' (MkCFM p) = MkCFM (p @{Compose})
105 |   roam = roamCofree
106 |
107 | ------------------------------------------------------------------------------
108 | -- FreeMapping
109 | ------------------------------------------------------------------------------
110 |
111 | ||| The monad generated by the reflective subcategory of profunctors that
112 | ||| implement `Mapping`.
113 | public export
114 | data FreeMapping : (p : Type -> Type -> Type) -> Type -> Type -> Type where
115 |   MkFM : Functor f => (f y -> b) -> p x y -> (a -> f x) -> FreeMapping p a b
116 |
117 | public export
118 | Profunctor (FreeMapping p) where
119 |   lmap f (MkFM l m r) = MkFM l m (r . f)
120 |   rmap f (MkFM l m r) = MkFM (f . l) m r
121 |   dimap f g (MkFM l m r) = MkFM (g . l) m (r . f)
122 |
123 | public export
124 | ProfunctorFunctor FreeMapping where
125 |   promap f (MkFM l m r) = MkFM l (f m) r
126 |
127 | public export
128 | ProfunctorMonad FreeMapping where
129 |   propure p = MkFM @{FunctorId} id p id
130 |   projoin (MkFM l' (MkFM l m r) r') = MkFM @{Compose} (l' . map l) m (map r . r')
131 |
132 | public export
133 | Functor (FreeMapping p a) where
134 |   map = rmap
135 |
136 | public export
137 | GenStrong Pair (FreeMapping p) where
138 |   strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
139 |   strongl = dimap swap' swap' . strongr {p=FreeMapping p}
140 |
141 | public export
142 | GenStrong Either (FreeMapping p) where
143 |   strongr (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
144 |   strongl = dimap swap' swap' . strongr {p=FreeMapping p}
145 |
146 | public export
147 | Closed (FreeMapping p) where
148 |   closed (MkFM l m r) = dimap Mor applyMor $ MkFM @{Compose} (map l) m (map r)
149 |
150 | roamFree : ((a -> b) -> s -> t) -> FreeMapping p a b -> FreeMapping p s t
151 | roamFree f (MkFM l m r) = MkFM @{Compose @{functor}} (($ id) . map @{functor} l) m (map @{functor} r . flip f)
152 |
153 | public export
154 | Traversing (FreeMapping p) where
155 |   traverse' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
156 |   wander f = roamFree $ f @{ApplicativeId}
157 |
158 | public export
159 | Mapping (FreeMapping p) where
160 |   map' (MkFM l m r) = MkFM @{Compose} (map l) m (map r)
161 |   roam = roamFree
162 |