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