Data.Container.Additive.Object.Instances

Reexports

Definitions

Const2 : Type -> ComMonoid -> AddCont

  Constant (non-dependent) add. container, positions not dependent on shapes
  As a polynomial functor: F(Y) = aY^b

Totality: total
Visibility: public export

Const : (a : Type) -> ComMonoid a => AddCont

  Constant additive container whose shapes and positions coincide
  Also arises from Num instance

Totality: total
Visibility: public export

data IsConst : AddCont -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsConst : (p : Type) -> {auto mon : ComMonoid p} -> IsConst (Const p)

numOnPositions : Num p => {auto mon : ComMonoid p} -> InterfaceOnPositions (Const p) Num

  Every constant additive container on a numeric type carries `Num` on its
  positions: `(Const p @{mon}).PosSet s` reduces to `p` at every shape, so the
  witness is the numeric instance itself, constantly.
  A `%hint`, so that matching an `IsConst` witness into scope is enough for
  search to discharge an `InterfaceOnPositions` goal.

Totality: total
Visibility: public export

Nap : ComMonoid -> AddCont

  Naperian additive container: a constant container with a single shape
  As a polynomial functor: F(Y) = Y^b

Totality: total
Visibility: public export

Flat : Type -> AddCont

  Flat additive container: a constant container with a single position
  As a polynomial functor: F(Y) = aY
  Notably, unlike with `Data.Container.Base`, there is no `Sharp`

Totality: total
Visibility: public export

Empty : AddCont

  Empty additive container
  As a polynomial functor: F(Y) = 0
  Initial additive container

Totality: total
Visibility: public export

Scalar : AddCont

  Container of a single thing
  As a polynomial functor: F(Y) = U(Y) where U is forgetful functor
  Unit of the tensor product

Totality: total
Visibility: public export

UnitCont : AddCont

  Additive container with a single shape and position
  As a polynomial functor F(Y) = 1
  Terminal additive container

Totality: total
Visibility: public export