0 | module Data.Container.Base.Extension.Definition
 1 |
 2 | import Data.Container.Base.Object.Definition
 3 | import Data.Container.Base.Morphism.Definition
 4 |
 5 | import Misc
 6 |
 7 | ||| Extension of a container
 8 | ||| This allows us to talk about the content, or payload of a container
 9 | public export
10 | record Ext (0 c : Cont) (x : Type) where
11 |   constructor (<|)
12 |   shapeExt : c.Shp
13 |   index : c.Pos shapeExt -> x
14 |
15 | ||| In `Ext c x`, the container `c` is said to be "full off" values of type `x`
16 | ||| `fullOf` is sometimes used as infix operator to aid readability
17 | public export
18 | fullOf : Cont -> Type -> Type
19 | fullOf c x = Ext c x 
20 |
21 | ||| Every extension is a functor : Type -> Type
22 | public export
23 | Functor (Ext c) where
24 |   map {c=shp !> pos} f (s <| v) = s <| f . v
25 |
26 | ||| Composition of extensions is a functor
27 | public export
28 | Functor (Ext d . Ext c) where
29 |   map f e = (map f) <$> e
30 |
31 | ||| Ext is a functor of type Cont -> [Type, Type]
32 | ||| On objects it maps a container to a polynomial functor
33 | ||| On morphisms it maps a dependent lens to a natural transformation
34 | ||| This is the action on morphisms
35 | public export
36 | extMap : c =%> d -> Ext c a -> Ext d a
37 | extMap f (sh <| index) = let (y ** ky) = (%!) f sh
38 |                          in y <| (index . ky)
39 |
40 |
41 | namespace ExtProofs
42 |   ||| Mapping over an extension preserves its shape 
43 |   public export
44 |   mapShapeExt : {0 c : Cont} ->
45 |     {0 f : a -> b} ->
46 |     (l : c `fullOf` a) ->
47 |     shapeExt (f <$> l) = shapeExt l
48 |   mapShapeExt {c=shp !> pos} (sh <| _) = Refl
49 |
50 |   ||| Indexing over a mapped extension is the same as indexing over a rewrite
51 |   ||| of the map
52 |   public export
53 |   mapIndexCont : {c : Cont} ->
54 |     {0 f : a -> b} -> 
55 |     (l : c `fullOf` a) ->
56 |     (ps : c.Pos (shapeExt (f <$> l))) ->
57 |     f (index l (rewrite sym (mapShapeExt {f=f} l) in ps))
58 |       = index (f <$> l) ps
59 |   mapIndexCont {c=shp !> pos} (sh <| contentAt) ps = Refl
60 |
61 | ||| Structure needed to store equality data for Ext.
62 | ||| To prove that two extensions `e1, e2` are equal, we need to provide a proof
63 | ||| in two steps, and use the first one to rewrite the second. That is, we need
64 | ||| a) a proof that the chosen shape types are equal. This allows us to 
65 | ||| rewrite the position maps of both extensions to the same type.
66 | ||| b) for each shape, a proof that the positions are equal as types
67 | public export
68 | record EqExt (e1, e2 : Ext c a) where
69 |   constructor MkEqExt
70 |   ||| The shapes must be equal
71 |   shapesEqual : e1.shapeExt = e2.shapeExt
72 |   ||| For each position in that shape, the values must be equal
73 |   ||| Relying on rewrite to get the correct type for the position
74 |   valuesEqual : (p : c.Pos (e1.shapeExt)) ->
75 |     e1.index p =
76 |     e2.index (rewrite__impl (c.Pos) (sym shapesEqual) p)
77 |
78 |
79 | ||| Another alternative is to use DecEq, and a different explicit rewrite
80 | public export
81 | decEqExt : (e1, e2 : Ext c a) ->
82 |   EqExt e1 e2 ->
83 |   Dec (e1 = e2)
84 |
85 | {-
86 | TODO how does automatic deriving of equality work if the number of positions is infinite? (As is the case with some containers)
87 | Checking for equality by simple brute-force clearly cannot be done in finite time (this works for DecEq, but also for Eq since it is marked as total)
88 |
89 | Can decidability work if the user provides a function to perform that check (perhaps by higher-order symbolic manipulation, as opposed to brute-force)?
90 |
91 | TODO the trick of using DecEq to create an Eq instance is used in DPair?
92 |
93 | -- decEqExt e1 e2 (MkEqExt shapesEqual valuesEqual)
94 | --   = Yes ?decEqExt_rhs_0 -- complicated, but doable?
95 | -}