yoko-0.1: generic programming with disbanded constructors

Portabilitysee LANGUAGE pragmas (... GHC)



Algebras and catamorphisms for mutually-recursive datatypes.



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

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

newtype Algebra m t Source


Alg (Alg m t) 


type Algebras ts m = Each ts (Algebra m)Source

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

Builds an Each of algebras via Reduce.

data CataD ts m t whereSource

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.


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 


(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)Source

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

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