module Data.Yoko.Reduce
(Alg, Algebra(..), AlgebraU(..),
algebraFin, AlgebraDT(..), AlgebraUni, AlgebraDC(..)) where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.Reflect
type Alg m t = Disbanded m 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 AlgebraU m t where
AlgebraU :: (DT t, AlgebraDT m t) => AlgebraU m t
instance (DT t, AlgebraDT m t
) => t ::: AlgebraU m where inhabits = AlgebraU
algebraFin :: (AlgebraUni m (Inhabitants u), Finite u) =>
AnRMN m u -> Med m (LeftmostRange (Inhabitants u))
algebraFin = algebraUni . finiteNP
class DT t => AlgebraDT m t where algebraDT :: Disbanded m t -> Med m t
class AlgebraUni m dcs where
algebraUni :: AnRMN m (Uni dcs) -> Med m (LeftmostRange dcs)
instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us),
AlgebraUni m ts, AlgebraUni m us) => AlgebraUni m (ts :+ us) where
algebraUni = algebraUni `two` algebraUni
instance AlgebraDC m dc => AlgebraUni m (N dc) where
algebraUni (NP (Uni (Here Refl)) x) = algebraDC x
class DC dc => AlgebraDC m dc where algebraDC :: RMN m dc -> Med m (Range dc)
type OneOf ts = NP (Uni ts)
two :: (OneOf ts f -> a) -> (OneOf us f -> a) -> (OneOf (ts :+ us) f -> a)
two f g (NP (Uni tag) x) = case tag of
OnLeft u -> f $ NP (Uni u) x
OnRight v -> g $ NP (Uni v) x