record Cont : Type Containers capture the idea that datatypes consist of groups of memory
locations where data can be stored. Locations for a particular group are
referred to as 'positions' and a particular group is referred to as a
'shape'.
Totality: total
Visibility: public export
Constructor: (!>) : (Shp : Type) -> (Shp -> Type) -> Cont
Projections:
.Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type For each shape, a set of positions
.Shp : Cont -> Type A type of shapes
Hints:
ProdMonoid c => Alternative (Ext c)TensorMonoid c => Applicative (Ext c)IsNaperian c => Applicative (Ext c)Functor (Ext c)Functor (Ext d . Ext c)SeqMonoid c => Monad (Ext c)IsCubical c => SeqMonoid cIsNaperian c => TensorMonoid c
.Shp : Cont -> Type A type of shapes
Visibility: public exportShp : Cont -> Type A type of shapes
Visibility: public export.Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type For each shape, a set of positions
Visibility: public exportPos : ({rec:0} : Cont) -> Shp {rec:0} -> Type For each shape, a set of positions
Visibility: public exportConst2 : Type -> Type -> Cont Constant container, one where positions do not depend on shapes
Visibility: public exportConst : Type -> Cont Constant container, one where positions do not depend on shapes
Visibility: public exportNap : Type -> Cont Naperian container: a constant container with a single shape
Visibility: public exportdata InterfaceOnPositions : Cont -> (Type -> Type) -> Type Convenience datatype for storing the data that a container `c` has an
interface `i` on its positions
TODO does the argument of MkI need to be auto implicit?
Totality: total
Visibility: public export
Constructor: MkI : ((s : c .Shp) -> i (c .Pos s)) => InterfaceOnPositions c i For every shape `s` the set of positions `c.Pos s` has that interface
IsFinite : Cont -> Type A container is finite when for every shape the set of positions is finite.
Examples: vectors, lists, but also finite binary trees.
Note, provision of a finite instance for trees requires a choice of a tree
traversal. (All of these choices isomorphic, but are necessary to make)
Visibility: public exportdata IsNaperian : Cont -> Type A container is Naperian when the set of shapes is `Unit`, i.e. when it
contains only one set of positions.
Examples: Scalar, UnitCont, Pair, Vect n, Stream.
Notably, Naperian does not imply Finite, as the `Stream` example shows.
Totality: total
Visibility: public export
Constructor: MkIsNaperian : (pos : Type) -> IsNaperian (Nap pos)
Hints:
IsNaperian c => Applicative (Ext c)IsNaperian c => TensorMonoid c
LogHelper : IsNaperian c => Type- Visibility: public export
Log : (0 c : Cont) -> IsNaperian c => Type- Visibility: public export
naperianPosEq : IsNaperian c => c .Pos x = c .Pos y- Visibility: public export
data IsCubical : Cont -> Type A container is cubical whenever it is Finite and Naperian
Effectively, captures `Vect n` containers, up to isomorphism
Examples: for any `n : Nat`, `Vect n`. Those are all the examples, up to
isomorphism. Notably, this also includes a container whose unique set of
positions is the set of positions of a binary tree of a particular shape.
This is isomorphic to the `Vect k` container, for some `k`, assuming a
choice of tree traversal (though all of them yield the same `k`). Here
`k` corresponds to the number of positions in that binary tree
Totality: total
Visibility: public export
Constructor: MkIsCubical : (n : Nat) -> IsCubical (Nap (Fin n))
Hint: IsCubical c => SeqMonoid c
dimHelper : IsCubical c -> Nat- Visibility: public export
dim : (0 c : Cont) -> IsCubical c => Nat We call dimension the size of the set of positions of a finite container
Visibility: public exportdata IsFlat : Cont -> Type Used in learning, where we want to know that the tangent space over a
particular parameter is equal to the parameter space itself
Totality: total
Visibility: public export
Constructor: MkIsFlat : (p : Type) -> IsFlat (p !> (\{_:5337} => p))