Data.Container.Base.Properties.Definitions

Definitions

data InterfaceOnPositions : (0 _ : Cont) -> (Type -> Type) -> Type

  Convenience datatype for storing the data that a container `c` has an
  interface `i` on its positions

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

GetInterface : InterfaceOnPositions c i -> (s : c .Shp) -> i (c .Pos s)

Totality: total
Visibility: public export

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)

Totality: total
Visibility: public export

data IsNonDep : Cont -> Type

  A container is non-dependent when positions do not depend on shapes

Totality: total
Visibility: public export
Constructor: 

MkIsNonDep : (s : Type) -> (p : Type) -> IsNonDep (s !> (\{_:17162} => p))

data IsConst : 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: 

ItIsConst : (p : Type) -> IsConst (p !> (\{_:17177} => p))

data IsFlat : Cont -> Type

  Following the flat-sharp terminology

Totality: total
Visibility: public export
Constructor: 

ItIsFlat : (s : Type) -> IsFlat (s !> (\{_:17191} => ()))

data IsSharp : Cont -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsSharp : (s : Type) -> IsSharp (s !> (\{_:17205} => Void))

NaperianCont : Type -> Cont

  Will be removed later, temp fix for now as otherwise the coverage 
  checker complains

Totality: total
Visibility: public export

data 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 (NaperianCont pos)

Hints:

IsNaperian c => Applicative (Ext c)

IsNaperian c => SeqMonoid c

IsNaperian c => TensorMonoid c

LogHelper : IsNaperian c => Type

Totality: total
Visibility: public export

Log : (0 c : Cont) -> IsNaperian c => Type

Totality: total
Visibility: public export

naperianPosEq : IsNaperian c => c .Pos x = c .Pos y

Totality: total
Visibility: public export

CubicalCont : Nat -> Cont

  Will be removed later, temp fix for now as otherwise the coverage 
  checker complains

Totality: total
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 (CubicalCont n)

dimHelper : IsCubical c -> Nat

Totality: total
Visibility: public export

dim : (0 c : Cont) -> IsCubical c => Nat

  We call dimension the size of the set of positions of a finite container 

Totality: total
Visibility: public export

isCubicalContEq : ({arg:17308} : IsCubical d) -> d = () !> (\{_:17315} => Fin (dim d))

  Every cubical container is `Nap (Fin n)` with `n = dim ic` (used for rewrites).

Totality: total
Visibility: public export

interface IsFoldable : Cont -> Type

  A container is foldable if `c ≃ List`
  That is, there ought to exist a dependent lens `c =%> List` and back
  Here we only encode one part of this

Parameters: c
Constructor: 

MkIsFoldable

Methods:

mapToList : c =%> (Nat !> (\n => Fin n))

Implementations:

IsFoldable List

IsFoldable (Vect n)

IsFoldable BinTreeLeaf

IsFoldable BinTreeNode

IsFoldable BinTree

mapToList : IsFoldable c => c =%> (Nat !> (\n => Fin n))

Totality: total
Visibility: public export

interface IsConcrete : Cont -> Type

  Many datatypes in the Idris standard library are already
  concrete representations of particular containers

Parameters: c
Constructor: 

MkIsConcrete

Methods:

func : Type -> Type

functorInstance : Functor func

fromConcreteTy : func a -> Ext c a

toConcreteTy : Ext c a -> func a

Implementations:

IsConcrete Scalar

IsConcrete Maybe

IsConcrete Pair

IsConcrete c => IsConcrete d => IsConcrete (c >< d)

IsConcrete c => IsConcrete d => IsConcrete (c >@ d)

IsConcrete List

IsConcrete (Vect n)

IsConcrete (Grid (h, w))

IsConcrete BinTree

IsConcrete BinTreeNode

IsConcrete BinTreeLeaf

func : IsConcrete c => Type -> Type

Totality: total
Visibility: public export

functorInstance : {auto __con : IsConcrete c} -> Functor func

Totality: total
Visibility: public export

fromConcreteTy : {auto __con : IsConcrete c} -> func a -> Ext c a

Totality: total
Visibility: public export

toConcreteTy : {auto __con : IsConcrete c} -> Ext c a -> func a

Totality: total
Visibility: public export

(>#) : {auto {conArg:17476} : IsConcrete c} -> func a -> Ext c a

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 0

(#>) : {auto {conArg:17498} : IsConcrete c} -> Ext c a -> func a

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 0