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