0 | module Data.Container.Base.Properties.Definition
  1 |
  2 | import public Decidable.Equality
  3 | import Data.Fin
  4 | import Data.Finite
  5 | import Data.Vect
  6 |
  7 | import Data.Container.Base.Object.Definition
  8 | import Data.Container.Base.Morphism.Definition
  9 | import Data.Container.Base.Extension.Definition
 10 | import Data.Container.Base.Endofunctor.Definition
 11 |
 12 | import Data.Container.Base.Object.Instances
 13 | import Data.Container.Base.Morphism.Instances
 14 |
 15 | import Misc
 16 |
 17 | {-------------------------------------------------------------------------------
 18 | Properties of containers expressed in terms of two constructions:
 19 | `MapToWith` and `IsA`.
 20 |
 21 | `Properties` is the intentional exception to the rule of `Definition` not importing `Instances`, as the definitions here refer to *specific* containers, such as `List`, `Scalar`, and `Bag`.
 22 | -------------------------------------------------------------------------------}
 23 |
 24 | ||| The data of a lens from `d`, with `i` on its positions into `c`. Used to 
 25 | ||| generically define `IsFoldable`, `IsSummable`, and `InterfaceOnPositions`
 26 | public export
 27 | interface MapToWith (0 i : Type -> Type) (0 c : Cont) (0 d : Cont) where
 28 |   constructor Along
 29 |   mapTo : i <!> d =%> c
 30 |
 31 | public export
 32 | MapTo : {default id i : Type -> Type} -> Cont -> Cont -> Type
 33 | MapTo c d = MapToWith i c d
 34 |
 35 | ||| Stores the data of a container `c` with an interface `i` on its positions
 36 | ||| As a lens `i <!> c =%> Scalar` it is a costate of `i <!> c`
 37 | public export
 38 | InterfaceOnPositions : Cont -> (Type -> Type) -> Type
 39 | InterfaceOnPositions c i = MapTo {i} Scalar c
 40 |
 41 | public export
 42 | MkI : ((s : c.Shp) -> i (c.Pos s)) -> InterfaceOnPositions c i
 43 | MkI f = Along (toCostate f)
 44 |
 45 | ||| For every shape `s` the set of positions `c.Pos s` has that interface
 46 | public export
 47 | GetInterface : InterfaceOnPositions c i -> (s : c.Shp) -> i (c.Pos s)
 48 | GetInterface _ = fromCostate mapTo
 49 |
 50 | %hint
 51 | public export
 52 | fromPositions : {0 c : Cont} -> {0 i : Type -> Type} ->
 53 |   (pos : (s : c.Shp) -> i (c.Pos s)) => InterfaceOnPositions c i
 54 | fromPositions @{pos} = MkI pos
 55 |
 56 | ||| A container is decidable if for every shape its set of positions has 
 57 | ||| decidable equality
 58 | public export
 59 | IsDecidable : Cont -> Type
 60 | IsDecidable c = InterfaceOnPositions c DecEq
 61 |
 62 | ||| A container is non-empty when for every shape the set of positions is
 63 | ||| non-empty. It's witnessed constructively by choosing a position for every
 64 | ||| shape. It's also the same data as a costate of a container.
 65 | ||| TODO can this be done without a specific witness?
 66 | public export
 67 | IsNonEmpty : Cont -> Type 
 68 | IsNonEmpty c = InterfaceOnPositions c id
 69 |
 70 | ||| Name more accurately reflecting the fact that position choice is arbitrary
 71 | public export
 72 | ChosenPositions : Cont -> Type
 73 | ChosenPositions = IsNonEmpty
 74 |
 75 | ||| Proof that a container `c` of the form `f x` for some `x`.
 76 | ||| Does not work with two arguments, i.e. this 
 77 | ||| (https://github.com/bgavran/TensorType/blob/cc67c8b4461467874a55af7756e1b4a7f768c1f0/src/Data/Container/Base/Properties/Definition.idr#L63) does not work with this definition, and would instead 
 78 | ||| require a `IsA2`. (That particular example was removed because nothing 
 79 | ||| depended on it)
 80 | public export
 81 | data IsA : Cont -> (0 f : a -> Cont) -> Type where
 82 |   Via : (x : a) -> IsA (f x) f
 83 |
 84 | public export
 85 | IsFlat : Cont -> Type
 86 | IsFlat c = IsA c Flat
 87 |
 88 | public export
 89 | IsSharp : Cont -> Type
 90 | IsSharp c = IsA c Sharp
 91 |
 92 | ||| Used in learning, where we want to know that the tangent space over a
 93 | ||| particular parameter is equal to the parameter space itself
 94 | public export
 95 | IsConst : Cont -> Type
 96 | IsConst c = IsA c Const
 97 |
 98 | ||| Notably, Naperian does not imply Finite (`Stream` is Naperian)
 99 | public export
100 | IsNaperian : Cont -> Type
101 | IsNaperian c = IsA c Nap
102 |
103 | namespace NaperianHelpers
104 |   public export
105 |   LogHelper : IsNaperian c => Type
106 |   LogHelper @{Via pos} = pos
107 |   
108 |   public export
109 |   Log : (0 c : Cont) -> IsNaperian c => Type
110 |   Log _ @{Via pos} = pos
111 |   
112 |   public export
113 |   naperianPosEq : IsNaperian c => {0 x, y : c.Shp} -> c.Pos x = c.Pos y
114 |   naperianPosEq @{Via _} = Refl
115 |
116 | ||| A container is cubical whenever it is Finite and Naperian.
117 | ||| All of such containers are `Vect n`, up to isomorphism. Notably, this also 
118 | ||| includes a container whose positions are the set of positions of a binary 
119 | ||| tree of a particular shape.  This is isomorphic to the `Vect k` container, 
120 | ||| for some `k`, assuming a choice of tree traversal
121 | public export
122 | IsCubical : Cont -> Type
123 | IsCubical c = IsA c Vect
124 |
125 | namespace CubicalHelpers
126 |   public export
127 |   dimHelper : IsCubical c -> Nat
128 |   dimHelper (Via n) = n
129 |   
130 |   ||| We call dimension the size of the set of positions of a finite container 
131 |   public export
132 |   dim : (0 c : Cont) -> IsCubical c => Nat
133 |   dim _ @{ic} = dimHelper ic
134 |   
135 |   ||| Every cubical container is `Vect n` with `n = dim ic` (used for rewrites).
136 |   public export
137 |   isCubicalContEq : IsCubical d -> d = Vect (dim {c=d})
138 |   isCubicalContEq (Via n) = Refl
139 |
140 | ||| A container is foldable if there exists a lens `c =%> List`
141 | ||| Notably, this isn't required to be an isomorphism. For instance, binary 
142 | ||| trees (with ordered branches) are foldable, but not isomorphic to lists.
143 | public export
144 | IsFoldable : Cont -> Type
145 | IsFoldable c = MapTo List c
146 |
147 | ||| A container is summable if there is a dependent lens `c =%> Bag`. That is,
148 | ||| a fold whose order does not matter.
149 | public export
150 | IsSummable : Cont -> Type
151 | IsSummable c = MapTo Bag c
152 |
153 | ||| The lens of a foldable container into `List`
154 | ||| Ideally we would not need this, but `id <!> c` does not reduce to `c`
155 | public export
156 | mapToList : IsFoldable c => c =%> List
157 | mapToList @{Along toL} = !% (%! toL)
158 |
159 | public export
160 | mapToBag : IsSummable c => c =%> Bag
161 | mapToBag @{Along toB} = !% (%! toB)
162 |
163 | ||| A container is enumerable when at every shape its positions are in
164 | ||| bijection with `Fin n`, i.e. there is a cartesian morphism into `List`
165 | ||| Are these lawful traversables? Every position is visited exactly once, in a 
166 | ||| chosen order.  Unlike with `IsFoldable`, positions can neither be skipped 
167 | ||| nor repeated
168 | public export
169 | interface IsEnumerable (0 c : Cont) where
170 |   constructor MkIsEnum
171 |   enumerate : c =:> List
172 |
173 | namespace IsConcrete
174 |   ||| Many datatypes in the Idris standard library are already
175 |   ||| concrete representations of particular containers
176 |   public export
177 |   interface IsConcrete (0 c : Cont) where
178 |     constructor MkIsConcrete
179 |     func : Type -> Type
180 |     functorInstance : Functor func
181 |     fromConcreteTy : func a -> Ext c a
182 |     toConcreteTy : Ext c a -> func a
183 |
184 |   public export prefix 0 >#, #>
185 |
186 |   public export
187 |   (>#) : IsConcrete c => func {c=c} a -> Ext c a
188 |   (>#) = fromConcreteTy
189 |
190 |   public export
191 |   (#>) : IsConcrete c => Ext c a -> func {c=c} a
192 |   (#>) = toConcreteTy