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