Data.Container.Base.Endofunctor.Instances

Definitions

Deriv : (c : Cont) -> IsDecidable c => Cont

  The derivative of a container `c` can be thought of as a shape `s : c.Shp`, 
  a distinguished position `p : c.Pos s`, and the set of *all other positions*
  Technically, this is an endofunctor only on cartesian containers

Totality: total
Visibility: public export

compositionBangPos : Functor m => (m <!> (c >@ d)) =%> (c >@ (m <!> d))

Totality: total
Visibility: public export

joinBwComp : Monad m => (m <!> (c >@ d)) =%> (m <!> (c >@ (m <!> d)))

  Composition product analogue of `joinBw`
  On the backward pass, it flattens an `m` of (position, `m` of positions)
  pairs into a single `m` of full positions.

Totality: total
Visibility: public export

coproductBang : (m <!> (c >+< d)) =%> ((m <!> c) >+< (m <!> d))

Totality: total
Visibility: public export

tensorBang : Applicative m => (m <!> (c >< d)) =%> ((m <!> c) >< (m <!> d))

Totality: total
Visibility: public export

compositionBang : Monoid (d .Shp) => (!!) (c >@ d) =%> ((!!) c >@ (!!) d)

Totality: total
Visibility: public export

compositionBangBack : Monad m => ((m <!> c) >@ (m <!> d)) =%> (m <!> (c >@ d))

Totality: total
Visibility: public export

setLens : IsDecidable c => (Pointed c >*< Scalar) =%> c

  Can also be written in terms of unplug and plug

Totality: total
Visibility: public export

set : IsDecidable c => (e : Ext c x) -> c .Pos (shapeExt e) -> x -> Ext c x

  The `index` field of an extension defines a "getter" for a container
  This is the container setter

Totality: total
Visibility: public export