
  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 | public export
 19 | DPair : Cont -> Type
 20 | DPair c = (x : c.Shp ** c.Pos x)
 21 | 
 22 | ||| Synonym for `DPair`. The idea is that we can think of a sigma type of 
 23 | ||| a container as a a choice of a shape, and a sequence of choices
 24 | ||| (the "path") to reach a particular position.
 25 | ||| This isn't as easily seen for containers not defined as fixpoints, where
 26 | ||| these "choices" are not made using container machinery, but directly in 
 27 | ||| Idris. But for n-ary containers this becomes more apparent
 28 | public export
 29 | Path : Cont -> Type
 30 | Path = DPair
 31 |