Data.Container.Base.Endofunctor.Definition

Definitions

(<!>) : (Type -> Type) -> Cont -> Cont

  If `f` is a monad, then `f <!> -` is a comonad, and vice versa

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

(<!>) : (f : (Type -> Type)) -> Functor f => c =%> d -> (f <!> c) =%> (f <!> d)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

(!!) : Cont -> Cont

  Comonad of the adjunction between Cont and Cont_Mon
  BANG. List on positions, always has a monoid structure

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

(!*) : Cont -> Cont

  Comonad of the adjunction between Cont and AddCont
  Bag on positions, always has a commutative monoid structure

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

(!!) : c =%> d -> (!!) c =%> (!!) d

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

(!*) : c =%> d -> (!*) c =%> (!*) d

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 9

pureBw : Monad m => (m <!> c) =%> c

  Turn a banged container into a container
  Requires pure on the backward pass
  At `m = Bag` this is the counit of `UC -| !*`, i.e. `addContTransposeInv id`

Totality: total
Visibility: public export

joinBw : Monad m => (m <!> c) =%> (m <!> (m <!> c))

Totality: total
Visibility: public export

sumBw : InterfaceOnPositions c ComMonoid => c =%> (Bag <!> c)

  A bag of positions is added up using their monoid structure
  This is the underlying lens of the unit of `UC -| !*`, i.e. of
  `addContTranspose id`.

Totality: total
Visibility: public export

ListAll : Cont -> Cont

Totality: total
Visibility: public export

ListAny : Cont -> Cont

Totality: total
Visibility: public export

BagAll : Cont -> Cont

Totality: total
Visibility: public export

unitBag : c =%> BagAll c

Totality: total
Visibility: public export

bww : (f : c =%> d) -> (cs : List (c .Shp)) -> All (d .Pos) (f .fwd <$> cs) -> All (c .Pos) cs

Totality: total
Visibility: public export

List : c =%> d -> ListAll c =%> ListAll d

Totality: total
Visibility: public export

Deriv : (c : Cont) -> InterfaceOnPositions c DecEq => Cont

  Derivative of a container
  Given c=(Shp !> pos) the derivative can be thought of as
  a shape s : Shp, a distinguished position p : pos s, and the set of *all other positions*

Totality: total
Visibility: public export