
  0 | module Data.Container.Base.Object.Definition
  1 | 
  2 | ||| Containers capture the idea that datatypes consist of groups of memory 
  3 | ||| locations where data can be stored. Locations for a particular group are 
  4 | ||| referred to as 'positions' and a particular group is referred to as a
  5 | ||| 'shape'.
  6 | public export
  7 | record Cont where
  8 |   constructor (!>)
  9 |   ||| A type of shapes
 10 |   Shp : Type
 11 |   ||| For each shape, a set of positions
 12 |   Pos : Shp -> Type
 13 | 
 14 | export typebind infixr 0 !>
 15 | 
 16 | %name Cont c, c', c''
 17 | 
 18 | ||| Also, states for charts
 19 | public export
 20 | DPair : Cont -> Type
 21 | DPair c = (x : c.Shp ** c.Pos x)
 22 | 
 23 | ||| Synonym for `DPair`. The idea is that we can think of a sigma type of 
 24 | ||| a container as a a choice of a shape, and a sequence of choices
 25 | ||| (the "path") to reach a particular position.
 26 | ||| This isn't as easily seen for containers not defined as fixpoints, where
 27 | ||| these "choices" are not made using container machinery, but directly in 
 28 | ||| Idris. But for n-ary containers this becomes more apparent
 29 | public export
 30 | Path : Cont -> Type
 31 | Path = DPair
 32 |