Data.Container.Base.Properties.Definitions

Definitions

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

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 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 !> (\{_:17235} => 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 !> (\{_:17250} => p))

data IsFlat : Cont -> Type

  Following the flat-sharp terminology

Totality: total
Visibility: public export
Constructor: 

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

data IsSharp : Cont -> Type

Totality: total
Visibility: public export
Constructor: 

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

NaperianCont : Type -> Cont

  Local alias used solely to keep `MkIsNaperian`'s index out of raw
  record-constructor form. Without this, pattern matches like
  `(MkIsNaperian p :: as)` against `All IsNaperian shape` trip an
  Idris 2 coverage-checker incompleteness (see issue #3721).
  Definitionally equal to `Nap pos` from `Object.Instances`,
  but defined here to avoid an import cycle.

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

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

CubicalCont : Nat -> Cont

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

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

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 export

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

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

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))

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:

concreteType : Type -> Type

concreteFunctor : Functor concreteType

fromConcreteTy : concreteType a -> Ext c a

toConcreteTy : Ext c a -> concreteType 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 BinTree

IsConcrete BinTreeNode

IsConcrete BinTreeLeaf

concreteType : IsConcrete c => Type -> Type

Visibility: public export

concreteFunctor : {auto __con : IsConcrete c} -> Functor concreteType

Visibility: public export

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

Visibility: public export

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

Visibility: public export

(>#) : {auto {conArg:17549} : IsConcrete c} -> concreteType a -> Ext c a

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

(#>) : {auto {conArg:17571} : IsConcrete c} -> Ext c a -> concreteType a

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