0 | module Data.Container.Base.Properties.Definitions
  1 |
  2 | import Data.Fin
  3 | import Data.Finite
  4 |
  5 | import Data.Container.Base.Object.Definition
  6 | import Data.Container.Base.Morphism.Definition
  7 | import Data.Container.Base.Extension.Definition
  8 |
  9 | import Misc
 10 |
 11 | {-------------------------------------------------------------------------------
 12 | States various properties a container can have
 13 | Some of these mirror aliases in `Object.Definitions`, they're purposefully 
 14 | separated with imports, and don't refer to each other
 15 |
 16 | These are thought of as extensional declarations: we need not know anything 
 17 | about concrete instances to define these?
 18 |
 19 | -------------------------------------------------------------------------------}
 20 |
 21 | ||| Convenience datatype for storing the data that a container `c` has an
 22 | ||| interface `i` on its positions
 23 | public export
 24 | data InterfaceOnPositions : (c : Cont) -> (i : Type -> Type) -> Type where
 25 |   ||| For every shape `s` the set of positions `c.Pos s` has that interface
 26 |   MkI : ((s : c.Shp) -> i (c.Pos s)) -> InterfaceOnPositions c i
 27 |
 28 | ||| A container is finite when for every shape the set of positions is finite.
 29 | ||| Examples: vectors, lists, but also finite binary trees.
 30 | ||| Note, provision of a finite instance for trees requires a choice of a tree
 31 | ||| traversal. (All of these choices isomorphic, but are necessary to make)
 32 | public export
 33 | IsFinite : Cont -> Type
 34 | IsFinite c = InterfaceOnPositions c Finite
 35 |
 36 | ||| A container is non-dependent when positions do not depend on shapes
 37 | public export
 38 | data IsNonDep : Cont -> Type where
 39 |   MkIsNonDep : (s, p : Type) -> IsNonDep ((_ : s) !> p)
 40 |
 41 | ||| Used in learning, where we want to know that the tangent space over a
 42 | ||| particular parameter is equal to the parameter space itself
 43 | public export
 44 | data IsConst : Cont -> Type where
 45 |   ItIsConst : (p : Type) -> IsConst ((_ : p) !> p)
 46 |
 47 | ||| Following the flat-sharp terminology
 48 | public export
 49 | data IsFlat : Cont -> Type where
 50 |   ItIsFlat : (s : Type) -> IsFlat ((_ : s) !> Unit)
 51 |
 52 | public export
 53 | data IsSharp : Cont -> Type where
 54 |   ItIsSharp : (s : Type) -> IsSharp ((_ : s) !> Void)
 55 |
 56 | namespace Naperian
 57 |   ||| Local alias used solely to keep `MkIsNaperian`'s index out of raw
 58 |   ||| record-constructor form. Without this, pattern matches like
 59 |   ||| `(MkIsNaperian p :: as)` against `All IsNaperian shape` trip an
 60 |   ||| Idris 2 coverage-checker incompleteness (see issue #3721).
 61 |   ||| Definitionally equal to `Nap pos` from `Object.Instances`,
 62 |   ||| but defined here to avoid an import cycle.
 63 |   public export
 64 |   NaperianCont : Type -> Cont
 65 |   NaperianCont pos = (_ : Unit) !> pos
 66 |
 67 |   ||| A container is Naperian when the set of shapes is `Unit`, i.e. when it
 68 |   ||| contains only one set of positions.
 69 |   ||| Examples: Scalar, UnitCont, Pair, Vect n, Stream.
 70 |   ||| Notably, Naperian does not imply Finite, as the `Stream` example shows.
 71 |   public export
 72 |   data IsNaperian : Cont -> Type where
 73 |     MkIsNaperian : (pos : Type) -> IsNaperian (NaperianCont pos)
 74 |   
 75 |   public export
 76 |   LogHelper : IsNaperian c => Type
 77 |   LogHelper @{MkIsNaperian pos} = pos
 78 |   
 79 |   public export
 80 |   Log : (0 c : Cont) -> IsNaperian c => Type
 81 |   Log _ @{MkIsNaperian pos} = pos
 82 |   
 83 |   public export
 84 |   naperianPosEq : IsNaperian c => {0 x, y : c.Shp} -> c.Pos x = c.Pos y
 85 |   naperianPosEq @{MkIsNaperian _} = Refl
 86 |
 87 | namespace Cubical
 88 |   ||| Will be removed later, temp fix for now as otherwise the coverage 
 89 |   ||| checker complains
 90 |   public export
 91 |   CubicalCont : Nat -> Cont
 92 |   CubicalCont n = (_ : Unit) !> Fin n
 93 |
 94 |   ||| A container is cubical whenever it is Finite and Naperian
 95 |   ||| Effectively, captures `Vect n` containers, up to isomorphism
 96 |   ||| Examples: for any `n : Nat`, `Vect n`. Those are all the examples, up to
 97 |   ||| isomorphism. Notably, this also includes a container whose unique set of
 98 |   ||| positions is the set of positions of a binary tree of a particular shape.
 99 |   ||| This is isomorphic to the `Vect k` container, for some `k`,  assuming a 
100 |   ||| choice of tree traversal (though all of them yield the same `k`). Here 
101 |   ||| `k` corresponds to the number of positions in that binary tree
102 |   public export
103 |   data IsCubical : Cont -> Type where
104 |     MkIsCubical : (n : Nat) -> IsCubical (CubicalCont n)
105 |     
106 |   public export
107 |   dimHelper : IsCubical c -> Nat
108 |   dimHelper (MkIsCubical n) = n
109 |     
110 |   ||| We call dimension the size of the set of positions of a finite container 
111 |   public export
112 |   dim : (0 c : Cont) -> IsCubical c => Nat
113 |   dim _ @{ic} = dimHelper ic
114 |   
115 |   ||| Every cubical container is `Nap (Fin n)` with `n = dim ic` (used for rewrites).
116 |   public export
117 |   isCubicalContEq : IsCubical d -> d = ((_ : Unit) !> (Fin (dim {c=d})))
118 |   isCubicalContEq (MkIsCubical n) = Refl
119 |
120 |
121 | namespace IsFoldable
122 |   ||| A container is foldable if `c ≃ List`
123 |   ||| That is, there ought to exist a dependent lens `c =%> List` and back
124 |   ||| Here we only encode one part of this
125 |   public export
126 |   interface IsFoldable (0 c : Cont) where
127 |     constructor MkIsFoldable
128 |     mapToList : c =%> ((n : Nat) !> Fin n)
129 |
130 |
131 | namespace IsConcrete
132 |   ||| Many datatypes in the Idris standard library are already
133 |   ||| concrete representations of particular containers
134 |   public export
135 |   interface IsConcrete (0 c : Cont) where
136 |     constructor MkIsConcrete
137 |     concreteType : Type -> Type
138 |     concreteFunctor : Functor concreteType
139 |     fromConcreteTy : concreteType a -> Ext c a
140 |     toConcreteTy : Ext c a -> concreteType a
141 |
142 |   public export prefix 0 >#, #>
143 |
144 |   public export
145 |   (>#) : IsConcrete c => concreteType {c=c} a -> Ext c a
146 |   (>#) = fromConcreteTy
147 |
148 |   public export
149 |   (#>) : IsConcrete c => Ext c a -> concreteType {c=c} a
150 |   (#>) = toConcreteTy