Data.Container(source)

Definitions

record Container : Type

Totality: total
Visibility: public export
Constructor: 

MkContainer : (Shape : Type) -> (Shape -> Type) -> Container

Projections:

.Position : ({rec:0} : Container) -> Shape {rec:0} -> Type

.Shape : Container -> Type

Hint: 

Functor (Extension c)

.Shape : Container -> Type

Totality: total
Visibility: public export

Shape : Container -> Type

Totality: total
Visibility: public export

.Position : ({rec:0} : Container) -> Shape {rec:0} -> Type

Totality: total
Visibility: public export

Position : ({rec:0} : Container) -> Shape {rec:0} -> Type

Totality: total
Visibility: public export

record Extension : Container -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkExtension : (shape : Shape c) -> (Position c shape -> x) -> Extension c x

Projections:

.payloads : ({rec:0} : Extension c x) -> Position c (shape {rec:0}) -> x

.shape : Extension c x -> Shape c

Hint: 

Functor (Extension c)

.shape : Extension c x -> Shape c

Totality: total
Visibility: public export

shape : Extension c x -> Shape c

Totality: total
Visibility: public export

.payloads : ({rec:0} : Extension c x) -> Position c (shape {rec:0}) -> x

Totality: total
Visibility: public export

payloads : ({rec:0} : Extension c x) -> Position c (shape {rec:0}) -> x

Totality: total
Visibility: public export

record Morphism : Container -> Container -> Type

Totality: total
Visibility: public export
Constructor: 

MkMorphism : (shapeMorphism : (Shape c -> Shape d)) -> (Position d (shapeMorphism s) -> Position c s) -> Morphism c d

Projections:

.positionMorphism : ({rec:0} : Morphism c d) -> Position d (shapeMorphism {rec:0} s) -> Position c s

.shapeMorphism : Morphism c d -> Shape c -> Shape d

.shapeMorphism : Morphism c d -> Shape c -> Shape d

Totality: total
Visibility: public export

shapeMorphism : Morphism c d -> Shape c -> Shape d

Totality: total
Visibility: public export

.positionMorphism : ({rec:0} : Morphism c d) -> Position d (shapeMorphism {rec:0} s) -> Position c s

Totality: total
Visibility: public export

positionMorphism : ({rec:0} : Morphism c d) -> Position d (shapeMorphism {rec:0} s) -> Position c s

Totality: total
Visibility: public export

Extension : Morphism c d -> Extension c x -> Extension d x

Totality: total
Visibility: public export

Const : Type -> Container

Totality: total
Visibility: public export

toConst : k -> Extension (Const k) x

Totality: total
Visibility: export

fromConst : Extension (Const k) x -> k

Totality: total
Visibility: export

Identity : Container

Totality: total
Visibility: public export

toIdentity : x -> Extension Identity x

Totality: total
Visibility: export

fromIdentity : Extension Identity x -> x

Totality: total
Visibility: export

Compose : Container -> Container -> Container

Totality: total
Visibility: public export

toCompose : (.) (Extension d) (Extension c) x -> Extension (Compose d c) x

Totality: total
Visibility: export

fromCompose : Extension (Compose d c) x -> (.) (Extension d) (Extension c) x

Totality: total
Visibility: export

Sum : Container -> Container -> Container

Totality: total
Visibility: public export

toSum : Either (Extension c x) (Extension d x) -> Extension (Sum c d) x

Totality: total
Visibility: export

fromSum : Extension (Sum c d) x -> Either (Extension c x) (Extension d x)

Totality: total
Visibility: export

Pair : Container -> Container -> Container

Totality: total
Visibility: public export

toPair : (Extension c x, Extension d x) -> Extension (Pair c d) x

Totality: total
Visibility: export

fromPair : Extension (Pair c d) x -> (Extension c x, Extension d x)

Totality: total
Visibility: export

Exponential : Type -> Container -> Container

Totality: total
Visibility: public export

toExponential : (k -> Extension c x) -> Extension (Exponential k c) x

Totality: total
Visibility: export

fromExponential : Extension (Exponential k c) x -> k -> Extension c x

Totality: total
Visibility: export

data W : Container -> Type

Totality: total
Visibility: public export
Constructor: 

MkW : Extension c (W c) -> W c

map : Morphism c d -> W c -> W d

Totality: total
Visibility: export

foldr : (Extension c x -> x) -> W c -> x

Totality: total
Visibility: export

para : (Extension c (x, W c) -> x) -> W c -> x

Totality: total
Visibility: export

record Free : Container -> Type -> Type

  @Free@ is a wrapper around @W@ to make it inference friendly.
  Without this wrapper, neither @pure@ nor @bind@ are able to infer their @c@ argument.

Totality: total
Visibility: public export
Constructor: 

MkFree : W (Sum c (Const x)) -> Free c x

Projection: 

.runFree : Free c x -> W (Sum c (Const x))

.runFree : Free c x -> W (Sum c (Const x))

Totality: total
Visibility: public export

runFree : Free c x -> W (Sum c (Const x))

Totality: total
Visibility: public export

pure : x -> Free c x

Totality: total
Visibility: export

(>>=) : Free c x -> (x -> Free c y) -> Free c y

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 1

join : Free c (Free c x) -> Free c x

Totality: total
Visibility: export

data M : Container -> Type

Totality: total
Visibility: public export
Constructor: 

MkM : Extension c (Inf (M c)) -> M c

unfoldr : (s -> Extension c s) -> s -> M c

Totality: total
Visibility: export

record Cofree : Container -> Type -> Type

  @Cofree@ is a wrapper around @M@ to make it inference friendly.
  Without this wrapper, neither @extract@ nor @extend@ are able to infer their @c@ argument.

Totality: total
Visibility: public export
Constructor: 

MkCofree : M (Pair (Const x) c) -> Cofree c x

Projection: 

.runCofree : Cofree c x -> M (Pair (Const x) c)

.runCofree : Cofree c x -> M (Pair (Const x) c)

Totality: total
Visibility: public export

runCofree : Cofree c x -> M (Pair (Const x) c)

Totality: total
Visibility: public export

extract : Cofree c x -> x

Totality: total
Visibility: export

extend : (Cofree c a -> b) -> Cofree c a -> Cofree c b

Totality: total
Visibility: export

duplicate : Cofree c a -> Cofree c (Cofree c a)

Totality: total
Visibility: export

Derivative : Container -> Container

Totality: total
Visibility: public export

hole : (v : Extension (Derivative c) x) -> Position c (fst (shape v))

Totality: total
Visibility: export

unplug : (v : Extension c x) -> Position c (shape v) -> (Extension (Derivative c) x, x)

Totality: total
Visibility: export

plug : (v : Extension (Derivative c) x) -> DecEq (Position c (fst (shape v))) => x -> Extension c x

Totality: total
Visibility: export

toConst : Extension (Const Void) x -> Extension (Derivative (Const k)) x

Totality: total
Visibility: export

fromConst : Extension (Derivative (Const k)) x -> Extension (Const Void) x

Totality: total
Visibility: export

toIdentity : Extension (Derivative Identity) x

Totality: total
Visibility: export

toSum : Extension (Sum (Derivative c) (Derivative d)) x -> Extension (Derivative (Sum c d)) x

Totality: total
Visibility: export

fromSum : Extension (Derivative (Sum c d)) x -> Extension (Sum (Derivative c) (Derivative d)) x

Totality: total
Visibility: export

toPair : Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x -> Extension (Derivative (Pair c d)) x

Totality: total
Visibility: export

fromPair : Extension (Derivative (Pair c d)) x -> Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x

Totality: total
Visibility: export

fromCompose : Extension (Derivative (Compose c d)) x -> Extension (Pair (Derivative d) (Compose (Derivative c) d)) x

Totality: total
Visibility: export

toCompose : ((s : c .Shape) -> DecEq (Position c s)) -> ((s : d .Shape) -> DecEq (Position d s)) -> Extension (Pair (Derivative d) (Compose (Derivative c) d)) x -> Extension (Derivative (Compose c d)) x

Totality: total
Visibility: export