yoko-0.2: generic programming with disbanded constructors

Portabilitysee LANGUAGE pragmas (... GHC)



Catamorphism for mutually-recursive datatypes.



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

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

Builds an Each of algebras via AlgebraDT.

data CataU ts m t whereSource

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.


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 


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

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