0 | module Data.Profunctor.Traversing
  1 |
  2 | import Control.Applicative.Const
  3 | import Data.Morphisms
  4 | import Data.Tensor
  5 | import Data.Profunctor
  6 |
  7 | %default total
  8 |
  9 |
 10 | ------------------------------------------------------------------------------
 11 | -- Default implementation machinery
 12 | ------------------------------------------------------------------------------
 13 |
 14 |
 15 | [FoldablePair] Foldable (Pair c) where
 16 |   foldr op init (_, x) = x `op` init
 17 |   foldl op init (_, x) = init `op` x
 18 |   null _ = False
 19 |
 20 | [TraversablePair] Traversable (Pair c) using FoldablePair where
 21 |   traverse f (l, r) = (l,) <$> f r
 22 |
 23 |
 24 | record Bazaar a b t where
 25 |   constructor MkBazaar
 26 |   runBazaar : forall f. Applicative f => (a -> f b) -> f t
 27 |
 28 | Functor (Bazaar a b) where
 29 |   map f (MkBazaar g) = MkBazaar (map f . g)
 30 |
 31 | Applicative (Bazaar a b) where
 32 |   pure a = MkBazaar $ \_ => pure a
 33 |   mf <*> ma = MkBazaar $ \k => runBazaar mf k <*> runBazaar ma k
 34 |
 35 | sell : a -> Bazaar a b b
 36 | sell a = MkBazaar ($ a)
 37 |
 38 | record Baz t b a where
 39 |   constructor MkBaz
 40 |   runBaz : forall f. Applicative f => (a -> f b) -> f t
 41 |
 42 | Functor (Baz t b) where
 43 |   map f (MkBaz g) = MkBaz (g . (. f))
 44 |
 45 |
 46 | sold : Baz t a a -> t
 47 | sold m = runBaz @{ApplicativeId} m id
 48 |
 49 | Foldable (Baz t b) where
 50 |   foldr f i bz = runBaz bz @{appEndo} f i
 51 |     where
 52 |       -- Equivalent to `Const (Endomorphism acc)`
 53 |       appEndo : Applicative (\_ => acc -> acc)
 54 |       appEndo = MkApplicative @{MkFunctor (const id)} (const id) (.)
 55 |
 56 | Traversable (Baz t b) where
 57 |   traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x
 58 |
 59 | public export
 60 | wanderDef : Profunctor p => (forall f. Traversable f => p a b -> p (f a) (f b))
 61 |                          -> (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
 62 | wanderDef tr f = dimap (\s => MkBaz $ \afb => f afb s) sold . tr
 63 |
 64 |
 65 | ------------------------------------------------------------------------------
 66 | -- Traversing interface
 67 | ------------------------------------------------------------------------------
 68 |
 69 |
 70 | ||| The interface of profunctors that implement `wander`.
 71 | ||| NOTE: Definitions in terms of `wander` are much more efficient!
 72 | |||
 73 | ||| Laws:
 74 | ||| * `traverse' = wander traverse`
 75 | ||| * `traverse' . lmap f = lmap (map f) . traverse'`
 76 | ||| * `traverse' . rmap f = rmap (map f) . traverse'`
 77 | ||| * `traverse' . traverse' = traverse' @{Compose}`
 78 | ||| * `dimap Id runIdentity . traverse' = id`
 79 | public export
 80 | interface (Strong p, Choice p) => Traversing p where
 81 |   traverse' : Traversable f => p a b -> p (f a) (f b)
 82 |   traverse' = wander traverse
 83 |
 84 |   wander : (forall f. Applicative f => (a -> f b) -> s -> f t) -> p a b -> p s t
 85 |   wander = wanderDef traverse'
 86 |
 87 |
 88 | ------------------------------------------------------------------------------
 89 | -- Implementations
 90 | ------------------------------------------------------------------------------
 91 |
 92 |
 93 | public export
 94 | Traversing Morphism where
 95 |   traverse' (Mor f) = Mor (map f)
 96 |   wander f (Mor p) = Mor (f @{ApplicativeId} p)
 97 |
 98 | ||| A named implementation of `Traversing` for function types.
 99 | ||| Use this to avoid having to use a type wrapper like `Morphism`.
100 | public export
101 | [Function] Traversing (\a,b => a -> b) using Strong.Function where
102 |   traverse' = map
103 |   wander f = f @{ApplicativeId}
104 |
105 | public export
106 | Applicative f => Traversing (Kleislimorphism f) where
107 |   traverse' (Kleisli p) = Kleisli (traverse p)
108 |   wander f (Kleisli p) = Kleisli (f p)
109 |
110 | public export
111 | Applicative f => Traversing (Star f) where
112 |   traverse' (MkStar p) = MkStar (traverse p)
113 |   wander f (MkStar p) = MkStar (f p)
114 |
115 | public export
116 | Monoid r => Traversing (Forget r) where
117 |   traverse' (MkForget k) = MkForget (foldMap k)
118 |   wander f (MkForget k) = MkForget (runConst . f (MkConst . k))
119 |
120 |
121 | ------------------------------------------------------------------------------
122 | -- CofreeTraversing
123 | ------------------------------------------------------------------------------
124 |
125 |
126 | ||| The comonad generated by the reflective subcategory of profunctors that
127 | ||| implement `Traversing`.
128 | public export
129 | record CofreeTraversing p a b where
130 |   constructor MkCFT
131 |   runCFT : forall f. Traversable f => p (f a) (f b)
132 |
133 | public export
134 | Profunctor p => Profunctor (CofreeTraversing p) where
135 |   lmap f (MkCFT p) = MkCFT (lmap (map f) p)
136 |   rmap g (MkCFT p) = MkCFT (rmap (map g) p)
137 |   dimap f g (MkCFT p) = MkCFT (dimap (map f) (map g) p)
138 |
139 | public export
140 | Profunctor p => GenStrong Pair (CofreeTraversing p) where
141 |   strongr (MkCFT p) = MkCFT (p @{Compose @{%search} @{TraversablePair}})
142 |   strongl = dimap swap' swap' . strongr {p=CofreeTraversing p}
143 |
144 | public export
145 | Profunctor p => GenStrong Either (CofreeTraversing p) where
146 |   strongr (MkCFT p) = MkCFT (p @{Compose {f=Either c}})
147 |   strongl = dimap swap' swap' . strongr {p=CofreeTraversing p}
148 |
149 | public export
150 | Profunctor p => Traversing (CofreeTraversing p) where
151 |   traverse' (MkCFT p) = MkCFT (p @{Compose})
152 |
153 | public export
154 | ProfunctorFunctor CofreeTraversing where
155 |   promap f (MkCFT p) = MkCFT (f p)
156 |
157 | public export
158 | ProfunctorComonad CofreeTraversing where
159 |   proextract (MkCFT p) = p @{TraversableId}
160 |   produplicate (MkCFT p) = MkCFT $ MkCFT $ p @{Compose}
161 |
162 | public export
163 | Profunctor p => Functor (CofreeTraversing p a) where
164 |   map = rmap
165 |
166 |
167 | public export
168 | cofreeTraversing : Traversing p => p :-> q -> p :-> CofreeTraversing q
169 | cofreeTraversing f p = MkCFT $ f $ traverse' p
170 |
171 | public export
172 | uncofreeTraversing : Profunctor q => p :-> CofreeTraversing q -> p :-> q
173 | uncofreeTraversing f p = proextract $ f p
174 |
175 |
176 | ------------------------------------------------------------------------------
177 | -- FreeTraversing
178 | ------------------------------------------------------------------------------
179 |
180 |
181 | ||| The monad generated by the reflective subcategory of profunctors that
182 | ||| implement `Traversing`.
183 | public export
184 | data FreeTraversing : (p : Type -> Type -> Type) -> Type -> Type -> Type where
185 |   MkFT : Traversable f => (f y -> b) -> p x y -> (a -> f x) -> FreeTraversing p a b
186 |
187 | public export
188 | Profunctor (FreeTraversing p) where
189 |   lmap f (MkFT l m r) = MkFT l m (r . f)
190 |   rmap f (MkFT l m r) = MkFT (f . l) m r
191 |   dimap f g (MkFT l m r) = MkFT (g . l) m (r . f)
192 |
193 | public export
194 | GenStrong Pair (FreeTraversing p) where
195 |   strongr (MkFT l m r) = MkFT @{Compose @{TraversablePair}} (map l) m (map r)
196 |   strongl = dimap swap' swap' . strongr {p=FreeTraversing p}
197 |
198 | public export
199 | GenStrong Either (FreeTraversing p) where
200 |   strongr (MkFT l m r) = MkFT @{Compose {t=Either c}} (map l) m (map r)
201 |   strongl = dimap swap' swap' . strongr {p=FreeTraversing p}
202 |
203 | public export
204 | Traversing (FreeTraversing p) where
205 |   traverse' (MkFT l m r) = MkFT @{Compose} (map l) m (map r)
206 |
207 | public export
208 | ProfunctorFunctor FreeTraversing where
209 |   promap f (MkFT l m r) = MkFT l (f m) r
210 |
211 | public export
212 | ProfunctorMonad FreeTraversing where
213 |   propure p = MkFT @{TraversableId} id p id
214 |   projoin (MkFT l' (MkFT l m r) r') = MkFT @{Compose} (l' . map l) m (map r . r')
215 |
216 |
217 | public export
218 | freeTraversing : Traversing q => p :-> q -> FreeTraversing p :-> q
219 | freeTraversing fn (MkFT {f} l m r) = dimap r l (traverse' {f} (fn m))
220 |
221 | public export
222 | unfreeTraversing : FreeTraversing p :-> q -> p :-> q
223 | unfreeTraversing f p = f (MkFT @{TraversableId} id p id)
224 |