0 | ------------------------------------------------------------------------
  1 | -- This module is based on the following papers:
  2 |
  3 | -- Categories of Containers
  4 | -- Abbott, Altenkirch, Ghani
  5 |
  6 | -- Derivatives of Containers
  7 | -- Abbott, Altenkirch, Ghani, McBride
  8 | ------------------------------------------------------------------------
  9 |
 10 | module Data.Container
 11 |
 12 | import Data.Either
 13 | import Decidable.Equality
 14 |
 15 | %default total
 16 |
 17 | ------------------------------------------------------------------------
 18 | -- Container and their morphisms
 19 | -- * Extension is a functor from Container to Type
 20 |
 21 | -- Objects of the category of containers
 22 | namespace Container
 23 |
 24 |   public export
 25 |   record Container where
 26 |     constructor MkContainer
 27 |     Shape : Type
 28 |     Position : Shape -> Type
 29 |
 30 |   public export
 31 |   record Extension (c : Container) (x : Type) where
 32 |     constructor MkExtension
 33 |     shape    : Shape c
 34 |     payloads : Position c shape -> x
 35 |
 36 |   ||| The image of a container by @Extension@ is a functor
 37 |   public export
 38 |   Functor (Extension c) where map f (MkExtension s p) = MkExtension s (f . p)
 39 |
 40 | -- Morphisms of the category of containers
 41 | namespace Morphism
 42 |
 43 |   public export
 44 |   record Morphism (c, d : Container) where
 45 |     constructor MkMorphism
 46 |     shapeMorphism : Shape c -> Shape d
 47 |     positionMorphism : {s : Shape c} -> Position d (shapeMorphism s) -> Position c s
 48 |
 49 |   public export
 50 |   Extension : Morphism c d -> Extension c x -> Extension d x
 51 |   Extension phi (MkExtension s p)
 52 |     = MkExtension (shapeMorphism phi s) (p . positionMorphism phi)
 53 |
 54 | ------------------------------------------------------------------------
 55 | -- Combinators to build containers
 56 |
 57 | namespace Combinators
 58 |
 59 |   -- Constant
 60 |   public export
 61 |   Const : Type -> Container
 62 |   Const k = MkContainer k (const Void)
 63 |
 64 |   export
 65 |   toConst : k -> Extension (Const k) x
 66 |   toConst v = MkExtension v absurd
 67 |
 68 |   export
 69 |   fromConst : Extension (Const k) x -> k
 70 |   fromConst (MkExtension v _) = v
 71 |
 72 |   -- Identity
 73 |   public export
 74 |   Identity : Container
 75 |   Identity = MkContainer () (\ () => ())
 76 |
 77 |   export
 78 |   toIdentity : x -> Extension Identity x
 79 |   toIdentity v = MkExtension () (const v)
 80 |
 81 |   export
 82 |   fromIdentity : Extension Identity x -> x
 83 |   fromIdentity (MkExtension () chld) = chld ()
 84 |
 85 |   -- Composition
 86 |   public export
 87 |   Compose : (d, c : Container) -> Container
 88 |   Compose d c = MkContainer
 89 |     (Extension d (Shape c))
 90 |     (\ (MkExtension shp chld) => (p : Position d shp ** Position c (chld p)))
 91 |
 92 |   export
 93 |   toCompose : (Extension d . Extension c) x -> Extension (Compose d c) x
 94 |   toCompose (MkExtension shp1 chld)
 95 |     = MkExtension (MkExtension shp1 (shape . chld)) (\ (p ** q) => payloads (chld p) q)
 96 |
 97 |   export
 98 |   fromCompose : Extension (Compose d c) x -> (Extension d . Extension c) x
 99 |   fromCompose (MkExtension (MkExtension shp1 shp2) chld)
100 |     = MkExtension shp1 (\ p => MkExtension (shp2 p) (\ q => chld (p ** q)))
101 |
102 |   -- Direct sum
103 |   public export
104 |   Sum : (c, d : Container) -> Container
105 |   Sum c d = MkContainer (Either (Shape c) (Shape d)) (either (Position c) (Position d))
106 |
107 |   export
108 |   toSum : Either (Extension c x) (Extension d x) -> Extension (Sum c d) x
109 |   toSum (Left (MkExtension shp chld)) = MkExtension (Left shp) chld
110 |   toSum (Right (MkExtension shp chld)) = MkExtension (Right shp) chld
111 |
112 |   export
113 |   fromSum : Extension (Sum c d) x -> Either (Extension c x) (Extension d x)
114 |   fromSum (MkExtension (Left shp) chld) = Left (MkExtension shp chld)
115 |   fromSum (MkExtension (Right shp) chld) = Right (MkExtension shp chld)
116 |
117 |   -- Pairing
118 |   public export
119 |   Pair : (c, d : Container) -> Container
120 |   Pair c d = MkContainer (Shape c, Shape d) (\ (p, q) => Either (Position c p) (Position d q))
121 |
122 |   export
123 |   toPair : (Extension c x, Extension d x) -> Extension (Pair c d) x
124 |   toPair (MkExtension shp1 chld1, MkExtension shp2 chld2)
125 |     = MkExtension (shp1, shp2) (either chld1 chld2)
126 |
127 |   export
128 |   fromPair : Extension (Pair c d) x -> (Extension c x, Extension d x)
129 |   fromPair (MkExtension (shp1, shp2) chld)
130 |     = (MkExtension shp1 (chld . Left), MkExtension shp2 (chld . Right))
131 |
132 |   -- Branching over a Type
133 |   public export
134 |   Exponential : Type -> Container -> Container
135 |   Exponential k c = MkContainer (k -> Shape c) (\ p => (v : k ** Position c (p v)))
136 |
137 |   export
138 |   toExponential : (k -> Extension c x) -> Extension (Exponential k c) x
139 |   toExponential f = MkExtension (shape . f) (\ (v ** p) => payloads (f v) p)
140 |
141 |   export
142 |   fromExponential : Extension (Exponential k c) x -> (k -> Extension c x)
143 |   fromExponential (MkExtension  shp chld) k = MkExtension (shp k) (\ p => chld (k ** p))
144 |
145 | ------------------------------------------------------------------------
146 | -- Taking various fixpoints of containers
147 |
148 | namespace Initial
149 |
150 |   public export
151 |   data W : Container -> Type where
152 |     MkW : Extension c (W c) -> W c
153 |
154 |   export
155 |   map : Morphism c d -> W c -> W d
156 |   map f (MkW (MkExtension shp chld)) = MkW $ Extension f (MkExtension shp (\ p => map f (chld p)))
157 |   --  Container.map inlined because of -------------------^
158 |   --  termination checking
159 |
160 |   export
161 |   foldr : (Extension c x -> x) -> W c -> x
162 |   foldr alg (MkW (MkExtension shp chld)) = alg (MkExtension shp (\ p => foldr alg (chld p)))
163 |
164 |   export
165 |   para : (Extension c (x, W c) -> x) -> W c -> x
166 |   para alg (MkW (MkExtension shp chld)) = alg (MkExtension shp (\ p => let w = chld p in (para alg w, w)))
167 |
168 | namespace Monad
169 |
170 |   ||| @Free@ is a wrapper around @W@ to make it inference friendly.
171 |   ||| Without this wrapper, neither @pure@ nor @bind@ are able to infer their @c@ argument.
172 |   public export
173 |   record Free (c : Container) (x : Type) where
174 |     constructor MkFree
175 |     runFree : W (Sum c (Const x))
176 |
177 |   export
178 |   pure : x -> Free c x
179 |   pure x = MkFree $ MkW (toSum (Right (toConst x)))
180 |
181 |   export
182 |   (>>=) : Free c x -> (x -> Free c y) -> Free c y
183 |   (>>=) (MkFree mx) k = foldr (alg . fromSum {c} {d = Const x}) mx where
184 |
185 |     alg : Either (Extension c (Free c y)) (Extension (Const x) (Free c y)) -> Free c y
186 |     alg  = either (MkFree . MkW . toSum {c} {d = Const y} . Left . map (runFree {c}))
187 |                   (k . fromConst {k = x})
188 |
189 |   export
190 |   join : Free c (Free c x) -> Free c x
191 |   join = (>>= id)
192 |
193 | namespace Final
194 |
195 |   public export
196 |   data M : Container -> Type where
197 |     MkM : Extension c (Inf (M c)) -> M c
198 |
199 |   export
200 |   unfoldr : (s -> Extension c s) -> s -> M c
201 |   unfoldr next seed =
202 |     let (MkExtension shp chld) = next seed in
203 |     MkM (MkExtension shp (\ p => unfoldr next (chld p)))
204 |
205 | namespace Comonad
206 |
207 |   ||| @Cofree@ is a wrapper around @M@ to make it inference friendly.
208 |   ||| Without this wrapper, neither @extract@ nor @extend@ are able to infer their @c@ argument.
209 |   public export
210 |   record Cofree (c : Container) (x : Type) where
211 |     constructor MkCofree
212 |     runCofree : M (Pair (Const x) c)
213 |
214 |   export
215 |   extract : Cofree c x -> x
216 |   extract (MkCofree (MkM m)) = fst (shape m)
217 |
218 |   export
219 |   extend : (Cofree c a -> b) -> Cofree c a -> Cofree c b
220 |   extend alg = MkCofree . unfoldr next . runCofree where
221 |
222 |     next : M (Pair (Const a) c) -> Extension (Pair (Const b) c) (M (Pair (Const a) c))
223 |     next m@(MkM layer) =
224 |       let (_, (MkExtension shp chld)) = fromPair {c = Const a} layer in
225 |       let b = toConst (alg (MkCofree m)) in
226 |       toPair (b, MkExtension shp (\ p => chld p))
227 | -- Eta-expanded to force Inf ------^
228 |
229 |   export
230 |   duplicate : Cofree c a -> Cofree c (Cofree c a)
231 |   duplicate = extend id
232 |
233 | ------------------------------------------------------------------------
234 | -- Derivative
235 |
236 | namespace Derivative
237 |
238 |   public export
239 |   Derivative : Container -> Container
240 |   Derivative c = MkContainer
241 |     (s : Shape c ** Position c s)
242 |     (\ (s ** p) => (p' : Position c s ** Not (p === p')))
243 |
244 |   export
245 |   hole : (v : Extension (Derivative c) x) -> Position c (fst (shape v))
246 |   hole (MkExtension (shp ** p) _) = p
247 |
248 |   export
249 |   unplug : (v : Extension c x) -> Position c (shape v) -> (Extension (Derivative c) x, x)
250 |   unplug (MkExtension shp chld) p = (MkExtension (shp ** p) (chld . fst), chld p)
251 |
252 |   export
253 |   plug : (v : Extension (Derivative c) x) -> DecEq (Position c (fst (shape v))) => x -> Extension c x
254 |   plug (MkExtension (shp ** p) chld) x = MkExtension shp $ \ p' => case decEq p p' of
255 |     Yes eq => x
256 |     No neq => chld (p' ** neq)
257 |
258 |   export
259 |   toConst : Extension (Const Void) x -> Extension (Derivative (Const k)) x
260 |   toConst v = absurd (fromConst v)
261 |
262 |   export
263 |   fromConst : Extension (Derivative (Const k)) x -> Extension (Const Void) x
264 |   fromConst v = absurd (hole {c = Const _} v)
265 |
266 |   export
267 |   toIdentity : Extension (Derivative Identity) x
268 |   toIdentity = MkExtension (() ** ()) (\ (() ** eq) => absurd (eq Refl))
269 |
270 |   export
271 |   toSum : Extension (Sum (Derivative c) (Derivative d)) x ->
272 |           Extension (Derivative (Sum c d)) x
273 |   toSum v = case fromSum {c = Derivative c} {d = Derivative d} v of
274 |     Left (MkExtension (shp ** p) chld) => MkExtension (Left shp ** p) chld
275 |     Right (MkExtension (shp ** p) chld) => MkExtension (Right shp ** p) chld
276 |
277 |   export
278 |   fromSum : Extension (Derivative (Sum c d)) x ->
279 |             Extension (Sum (Derivative c) (Derivative d)) x
280 |   fromSum (MkExtension (shp ** p) chld) = toSum {c = Derivative c} {d = Derivative d} $ case shp of
281 |     Left shp => Left (MkExtension (shp ** p) chld)
282 |     Right shp => Right (MkExtension (shp ** p) chld)
283 |
284 |   export
285 |   toPair : Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x ->
286 |            Extension (Derivative (Pair c d)) x
287 |   toPair v = case fromSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)} v of
288 |     Left p => let (MkExtension (shp1 ** p1) chld1, MkExtension shp2 chld2) = fromPair {c = Derivative c} p in
289 |               MkExtension ((shp1, shp2) ** Left p1) $ \ (p' ** neq) => case p' of
290 |                   Left p1' => chld1 (p1' ** (\prf => neq $ cong Left prf))
291 |                   Right p2' => chld2 p2'
292 |     Right p => let (MkExtension shp1 chld1, MkExtension (shp2 ** p2) chld2) = fromPair {c} {d = Derivative d} p in
293 |                MkExtension ((shp1, shp2) ** Right p2) $ \ (p' ** neq) => case p' of
294 |                   Left p1' => chld1 p1'
295 |                   Right p2' => chld2 (p2' ** (\prf => neq $ cong Right prf))
296 |
297 |   export
298 |   fromPair : Extension (Derivative (Pair c d)) x ->
299 |              Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x
300 |   fromPair (MkExtension ((shp1, shp2) ** p) chld) = case p of
301 |     Left p1 => toSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)}
302 |                      (Left (MkExtension ((shp1 ** p1), shp2) $ either
303 |                          (\ p1' => chld (Left (DPair.fst p1') ** DPair.snd p1' . injective))
304 |                          (\ p2 => chld (Right p2 ** absurd))))
305 |     Right p2 => toSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)}
306 |                      (Right (MkExtension (shp1, (shp2 ** p2)) $ either
307 |                          (\ p1 => chld (Left p1 ** absurd))
308 |                          (\ p2' => chld (Right (DPair.fst p2') ** DPair.snd p2' . injective))))
309 |
310 |
311 |   export
312 |   fromCompose : Extension (Derivative (Compose c d)) x ->
313 |                 Extension (Pair (Derivative d) (Compose (Derivative c) d)) x
314 |   fromCompose (MkExtension (MkExtension shp1 shp2 ** (p1 ** p2)) chld)
315 |     = toPair (left, right) where
316 |
317 |       left : Extension (Derivative d) x
318 |       left = MkExtension (shp2 p1 ** p2)
319 |            $ \ (p2' ** neqp2) => chld ((p1 ** p2') ** neqp2 . mkDPairInjectiveSnd)
320 |
321 |       right : Extension (Compose (Derivative c) d) x
322 |       right = toCompose
323 |             $ MkExtension (shp1 ** p1)
324 |             $ \ (p1' ** neqp1) => MkExtension (shp2 p1')
325 |                                  $ \ p2' => chld ((p1' ** p2') ** (\prf => neqp1 $ cong fst prf))
326 |
327 |   export
328 |   toCompose : ((s : _) -> DecEq (Position c s)) -> ((s : _) -> DecEq (Position d s)) ->
329 |               Extension (Pair (Derivative d) (Compose (Derivative c) d)) x ->
330 |               Extension (Derivative (Compose c d)) x
331 |   toCompose dec1 dec2 v with (fromPair {c = Derivative d} {d = Compose (Derivative c) d} v)
332 |     toCompose dec1 dec2 v | (MkExtension (shp2 ** p2) chld2, w) with (fromCompose w)
333 |       toCompose dec1 dec2 v
334 |         | (MkExtension (shp2 ** p2) chld2, w)
335 |         | (MkExtension (shp1 ** p1) chld1)
336 |         = MkExtension (MkExtension shp1 (\ p1' => shp2' p1' (decEq @{dec1 shp1} p1 p1')) **
337 |                       (p1 ** (p2' (decEq @{dec1 shp1} p1 p1))))
338 |         $ \ ((p1' ** p2'') ** neq) => chld2' p1' p2'' neq
339 |
340 |          where
341 |           shp2' : (p1' : Position c shp1) -> Dec (p1 === p1') -> Shape d
342 |           shp2' p1' (Yes eq) = shp2
343 |           shp2' p1' (No neq) = shape (chld1 (p1' ** neq))
344 |
345 |           p2' : (eq : Dec (p1 === p1)) -> Position d (shp2' p1 eq)
346 |           p2' (Yes Refl) = p2
347 |           p2' (No neq)   = absurd (neq Refl)
348 |
349 |           chld2' : (p1' : Position c shp1) ->
350 |                    (p2'' : Position d (shp2' p1' (decEq @{dec1 shp1} p1 p1'))) ->
351 |                    (neq : Not (MkDPair p1 (p2' (decEq @{dec1 shp1} p1 p1)) = MkDPair p1' p2'')) -> x
352 |           chld2' p1' p2'' neq with (decEq @{dec1 shp1} p1 p1')
353 |             chld2' p1' p2'' neq | No neq1 = payloads (chld1 (p1' ** neq1)) p2''
354 |             chld2' _ p2'' neq | Yes Refl with (decEq @{dec1 shp1} p1 p1)
355 |               chld2' _ p2'' neq | Yes Refl | No argh = absurd (argh Refl)
356 |               chld2' _ p2'' neq | Yes Refl | Yes Refl with (decEq @{dec2 shp2} p2 p2'')
357 |                 chld2' _ p2'' neq | Yes Refl | Yes Refl | No neq2 = chld2 (p2'' ** neq2)
358 |                 chld2' _ _ neq | Yes Refl | Yes Refl | Yes Refl = absurd (neq Refl)
359 |