Data.Functor.Algebra

Definitions

interface Algebra : (Type -> Type) -> Type -> Type

  Generalised sum operation
  Categorically, an F-Algebra

Parameters: f, carrier
Constructor: 

MkAlgebra

Methods:

reduce : f carrier -> carrier

Implementations:

AllAlgebra shape a => Algebra (Tensor shape) a

Num a => Algebra List a

Num a => Algebra (Vect n) a

Num a => Algebra BinTreeLeaf a

Num a => Algebra BinTreeNode a

Num a => Algebra BinTreeSame a

Num a => Algebra RoseTreeSame a

IsFoldable c => Num a => Algebra (Ext c) a

reduce : Algebra f carrier => f carrier -> carrier

Totality: total
Visibility: public export

data Initial : (Type -> Type) -> Type

  Initial algebra for an endofunctor
  Can we make it total by using containers, i.e. strictly positive functors?

Totality: not strictly positive
Visibility: public export
Constructor: 

In : f (Initial f) -> Initial f

  One part of the isomorphism

Out : Initial f -> f (Initial f)

  Second part of the isomorphism 

Totality: total
Visibility: public export

cata : Functor f => Algebra f a -> Initial f -> a

Visibility: public export

data Final : (Type -> Type) -> Type

Totality: not strictly positive
Visibility: public export
Constructor: 

MkFinal : f (Inf (Final f)) -> Final f

embedFinal : Final f -> Inf (Final f)

  For some reason, inlining this function in `ana` causes a compiler error

Visibility: public export

ana : Functor f => (a -> f a) -> a -> Final f

Visibility: public export