Data.Container.Base.Object.Definition

Definitions

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:

IsFoldable c => Num a => Algebra (Ext c) a

ProdMonoid c => Alternative (Ext c)

TensorMonoid c => Applicative (Ext c)

IsNaperian c => Applicative (Ext c)

IsFoldable c => Foldable (Ext c)

Functor (Ext c)

Functor (Ext d . Ext c)

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

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

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

IsEnumerable c => IsFoldable c

IsFoldable c => IsSummable c

SeqMonoid c => Monad (Ext c)

IsNaperian c => SeqMonoid c

SeqComonoid c -> TensorComonoid c

IsNaperian c => TensorMonoid c

SeqMonoid c -> TensorMonoid c

{auto {conArg:8213} : TensorMonoid c} -> TensorMonoid ApplicativeRoseTree

{auto {conArg:8303} : TensorMonoid c} -> TensorMonoid ApplicativeRoseTreeLeaf

{auto {conArg:8347} : TensorMonoid c} -> TensorMonoid ApplicativeRoseTreeNode

IsEnumerable c => Traversable (Ext c)

.Shp : Cont -> Type

  A type of shapes

Totality: total
Visibility: public export

Shp : Cont -> Type

  A type of shapes

Totality: total
Visibility: public export

.Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type

  For each shape, a set of positions

Totality: total
Visibility: public export

Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type

  For each shape, a set of positions

Totality: total
Visibility: public export

DPair : Cont -> Type

  Also, states for charts

Totality: total
Visibility: public export

Path : Cont -> Type

  Synonym for `DPair`. The idea is that we can think of a sigma type of 
  a container as a a choice of a shape, and a sequence of choices
  (the "path") to reach a particular position.
  This isn't as easily seen for containers not defined as fixpoints, where
  these "choices" are not made using container machinery, but directly in 
  Idris. But for n-ary containers this becomes more apparent

Totality: total
Visibility: public export