{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, UndecidableInstances #-} {- | Module : Data.Yoko.Algebra Copyright : (c) The University of Kansas 2011 License : BSD3 Maintainer : nicolas.frisby@gmail.com Stability : experimental Portability : see LANGUAGE pragmas (... GHC) Algebras and catamorphisms for mutually-recursive datatypes. -} module Data.Yoko.Algebra (Alg, Algebra(..), Algebras, SiblingAlgs, algebras, CataD(..), catas, cata, module Data.Yoko.Reduce) where import Type.Yoko import Data.Yoko.Generic import Data.Yoko.Reflect import Data.Yoko.Reduce -- | A @t@-algebra maps a sum of a @t@'s constructors into a mediation of @t@. type Alg m t = AnRMNUni m (DCs t) -> Med m t newtype Algebra m t = Alg (Alg m t) type instance Unwrap (Algebra m) t = Alg m t instance Wrapper (Algebra m) where wrap = Alg; unwrap (Alg x) = x data ReduceD m t where ReduceD :: (Reduce m (DCs t), t ~ LeftmostRange (DCs t)) => ReduceD m t instance (Reduce m (DCs t), t ~ LeftmostRange (DCs t) ) => t ::: ReduceD m where inhabits = ReduceD type Algebras ts m = Each ts (Algebra m) type SiblingAlgs t m = Algebras (Siblings t) m -- | Builds an 'Each' of algebras via 'Reduce'. algebras :: forall ts m. (ts ::: All (ReduceD m)) => [qP|m|] -> Algebras ts m algebras _ = each [qP|ReduceD m :: *->*|] $ \ReduceD -> reduce -- | @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. data CataD ts m t where 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 instance (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) ) => t ::: CataD ts m where inhabits = CataD catas :: forall m ts. (ts ::: All (CataD ts m)) => Algebras ts m -> Each ts (FromAt m IdM) catas fs = each [qP|CataD ts m :: *->*|] $ \d@CataD -> cataD d fs cataD :: forall m t. CataD (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t cataD CataD fs = prjEach (inhabitsFor [qP|t|]) fs . appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $ RMMap $ catas fs) . firstNP toUni . disband -- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med -- m t@. cata :: (t ::: CataD (Siblings t) m) => SiblingAlgs t m -> t -> Med m t cata = cataD inhabits