Data.Yoko.Cata

Catamorphism for mutually-recursive datatypes.

Documentation

type Algebras ts m = Each ts (Algebra m)

type SiblingAlgs t m = Algebras (Siblings t) m

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

Builds an Each of algebras via AlgebraDT.

data CataU ts m t where

t inhabits CataU 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

CataU :: (DT t, ts ~ Siblings t, ts ::: (Exists (:=: t)), (DCs t) ::: (All (YieldsArrowTSSU (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N)))), ts ::: (All (CataU ts m))) => CataU ts m t

Instances

(ts ~ Siblings t, DT t, ts ::: (Exists (:=: t)), (DCs t) ::: (All (YieldsArrowTSSU (AsComp (:. (RMMap (SiblingsU t) (FromAt m) IdM) N)))), ts ::: (All (CataU ts m))) => t ::: (CataU ts m)

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

cata :: t ::: (CataU (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