Data.Yoko.Algebra

Algebras and catamorphisms for mutually-recursive datatypes.

Documentation

type Alg m t = AnRMNUni m (DCs t) -> Med m t

A t-algebra maps a sum of a t's constructors into a mediation of t.

newtype Algebra m t

Constructors

Alg (Alg m t)

Instances

Wrapper (Algebra m)

type Algebras ts m = Each ts (Algebra m)

type SiblingAlgs t m = Algebras (Siblings t) m

algebras :: forall ts m. ts ::: (All (ReduceD m)) => Proxy (KS m) -> Algebras ts m

Builds an Each of algebras via Reduce.

data CataD ts m t where

t inhabits CataD ts m if

1. t is an instance of DT and ts ~ Siblings t
2. the recursive reduction can be mapped as a FromAt function via RMMap across all constructors of t and
3. all of t's siblings also inhabit the same universe.

Constructors

CataD :: (DT t, ts ~ Siblings t, t ::: (Uni ts), (DCs t) ::: (All (YieldsArrowTSSD (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N)))), ts ::: (All (CataD ts m))) => CataD ts m t

Instances

(ts ~ Siblings t, DT t, t ::: (Uni ts), (DCs t) ::: (All (YieldsArrowTSSD (AsComp (:. (RMMap (SiblingsU t) (FromAt m) IdM) N)))), ts ::: (All (CataD ts m))) => t ::: (CataD ts m)

catas :: forall m ts. ts ::: (All (CataD ts m)) => Algebras ts m -> Each ts (FromAt m IdM)

cata :: t ::: (CataD (Siblings t) m) => SiblingAlgs t m -> t -> Med m t

Uses the m-mediated algebras for t's siblings to reduce a t to Med m t.

module Data.Yoko.Reduce