7 | ||| Extension of a container
8 | ||| This allows us to talk about the content, or payload of a container
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
22 | ||| To be thought of as a choice of a shape, and a sequence of choices one
23 | ||| needs to make to reach a particular position.
24 | ||| For contianers that are not defined as fixpoints, this "choices" are not
25 | ||| made using container machinery, but directly in Idris
26 | ||| Nonetheless, even for `List`, to define a value of `Fin n` we have to
27 | ||| recursively go through a "path"
32 | ||| Every extension is a functor : Type -> Type
37 | ||| Composition of extensions is a functor
42 | ||| Ext is a functor of type Cont -> [Type, Type]
43 | ||| On objects it maps a container to a polynomial functor
44 | ||| On morphisms it maps a dependent lens to a natural transformation
45 | ||| This is the action on morphisms
53 | ||| Mapping over an extension preserves its shape
61 | ||| Indexing over a mapped extension is the same as indexing over a rewrite
62 | ||| of the map
72 | ||| Structure needed to store equality data for Ext.
73 | ||| To prove that two extensions `e1, e2` are equal, we need to provide a proof
74 | ||| in two steps, and use the first one to rewrite the second. That is, we need
75 | ||| a) a proof that the chosen shape types are equal. This allows us to
76 | ||| rewrite the position maps of both extensions to the same type.
77 | ||| b) for each shape, a proof that the positions are equal as types
81 | ||| The shapes must be equal
83 | ||| For each position in that shape, the values must be equal
84 | ||| Relying on rewrite to get the correct type for the position
90 | ||| Another alternative is to use DecEq, and a different explicit rewrite
96 | {-
97 | TODO how does automatic deriving of equality work if the number of positions is infinite? (As is the case with some containers)
98 | 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)
100 | Can decidability work if the user provides a function to perform that check (perhaps by higher-order symbolic manipulation, as opposed to brute-force)?
102 | TODO the trick of using DecEq to create an Eq instance is used in DPair?
104 | -- decEqExt e1 e2 (MkEqExt shapesEqual valuesEqual)
105 | -- = Yes ?decEqExt_rhs_0 -- complicated, but doable?
106 | -}