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