0 | module Data.Container.Base.Object.Definition
  1 |
  2 | import Data.Fin
  3 | import Data.Finite
  4 |
  5 | ||| Containers capture the idea that datatypes consist of groups of memory 
  6 | ||| locations where data can be stored. Locations for a particular group are 
  7 | ||| referred to as 'positions' and a particular group is referred to as a
  8 | ||| 'shape'.
  9 | public export
 10 | record Cont where
 11 |   constructor (!>)
 12 |   ||| A type of shapes
 13 |   Shp : Type
 14 |   ||| For each shape, a set of positions
 15 |   Pos : Shp -> Type
 16 |
 17 | export typebind infixr 0 !>
 18 |
 19 | %name Cont c, c', c''
 20 |
 21 | ||| Constant container, one where positions do not depend on shapes
 22 | public export
 23 | Const2 : Type -> Type -> Cont
 24 | Const2 a b = (_ : a) !> b
 25 |
 26 | ||| Constant container, one where positions do not depend on shapes
 27 | public export 
 28 | Const : Type -> Cont
 29 | Const a = Const2 a a
 30 |
 31 | ||| Naperian container: a constant container with a single shape
 32 | public export
 33 | Nap : Type -> Cont
 34 | Nap b = Const2 Unit b
 35 |
 36 | ||| Convenience datatype for storing the data that a container `c` has an
 37 | ||| interface `i` on its positions
 38 | ||| TODO does the argument of MkI need to be auto implicit?
 39 | public export
 40 | data InterfaceOnPositions : (c : Cont) -> (i : Type -> Type) -> Type where
 41 |   ||| For every shape `s` the set of positions `c.Pos s` has that interface
 42 |   MkI : (p : (s : c.Shp) -> i (c.Pos s)) =>
 43 |     InterfaceOnPositions c i
 44 |
 45 | ||| A container is finite when for every shape the set of positions is finite.
 46 | ||| Examples: vectors, lists, but also finite binary trees.
 47 | ||| Note, provision of a finite instance for trees requires a choice of a tree
 48 | ||| traversal. (All of these choices isomorphic, but are necessary to make)
 49 | public export
 50 | IsFinite : Cont -> Type
 51 | IsFinite c = InterfaceOnPositions c Finite
 52 |
 53 | ||| A container is Naperian when the set of shapes is `Unit`, i.e. when it
 54 | ||| contains only one set of positions.
 55 | ||| Examples: Scalar, UnitCont, Pair, Vect n, Stream.
 56 | ||| Notably, Naperian does not imply Finite, as the `Stream` example shows.
 57 | public export
 58 | data IsNaperian : Cont -> Type where
 59 |   MkIsNaperian : (pos : Type) -> IsNaperian (Nap pos)
 60 |
 61 | public export
 62 | LogHelper : IsNaperian c => Type
 63 | LogHelper @{MkIsNaperian pos} = pos
 64 |
 65 | public export
 66 | Log : (0 c : Cont) -> IsNaperian c => Type
 67 | Log _ @{MkIsNaperian pos} = pos
 68 |
 69 | -- ||| If we have a Naperian container, we can always produce (the unique)
 70 | -- ||| inhabitant of it shape
 71 | -- public export
 72 | -- naperianShape : IsNaperian c => c.Shp
 73 | -- naperianShape @{(MkIsNaperian pos)} = ()
 74 | -- 
 75 | public export
 76 | naperianPosEq : IsNaperian c => {0 x, y : c.Shp} -> c.Pos x = c.Pos y
 77 | naperianPosEq @{MkIsNaperian _} = Refl
 78 |
 79 | ||| A container is cubical whenever it is Finite and Naperian
 80 | ||| Effectively, captures `Vect n` containers, up to isomorphism
 81 | ||| Examples: for any `n : Nat`, `Vect n`. Those are all the examples, up to
 82 | ||| isomorphism. Notably, this also includes a container whose unique set of
 83 | ||| positions is the set of positions of a binary tree of a particular shape.
 84 | ||| This is isomorphic to the `Vect k` container, for some `k`,  assuming a 
 85 | ||| choice of tree traversal (though all of them yield the same `k`). Here 
 86 | ||| `k` corresponds to the number of positions in that binary tree
 87 | public export
 88 | data IsCubical : Cont -> Type where
 89 |   MkIsCubical : (n : Nat) -> IsCubical (Nap (Fin n))
 90 |   
 91 | public export
 92 | dimHelper : IsCubical c -> Nat
 93 | dimHelper (MkIsCubical n) = n
 94 |   
 95 | ||| We call dimension the size of the set of positions of a finite container 
 96 | public export
 97 | dim : (0 c : Cont) -> IsCubical c => Nat
 98 | dim _ @{ic} = dimHelper ic
 99 |
100 |
101 | ||| Used in learning, where we want to know that the tangent space over a
102 | ||| particular parameter is equal to the parameter space itself
103 | public export
104 | data IsFlat : Cont -> Type where
105 |   MkIsFlat : (p : Type) -> IsFlat ((_ : p) !> p)
106 |