{-# LANGUAGE QuasiQuotes, ScopedTypeVariables, TypeOperators, GADTs, MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances, FlexibleInstances, UndecidableInstances, TypeFamilies #-} {- | Module : Data.Yoko.Reduce Copyright : (c) The University of Kansas 2011 License : BSD3 Maintainer : nicolas.frisby@gmail.com Stability : experimental Portability : see LANGUAGE pragmas (... GHC) Reduction of a band of constructors into a mediation of their range. -} module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where import Type.Yoko import Data.Yoko.Generic import Data.Yoko.Reflect type AnRMNUni m ts = AnRMN m (Uni ts) -- | @reduce@ embeds a mediated sum of constructors into a mediation of their -- range. class (dcs ::: All IsDC) => Reduce m dcs where reduce :: AnRMNUni m dcs -> Med m (LeftmostRange dcs) instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us), Reduce m ts, Reduce m us) => Reduce m (ts :+ us) where reduce = reduce `two` reduce instance ReduceDC m dc => Reduce m (N dc) where reduce = reduceDC . unRMNUni where unRMNUni :: AnRMNUni m (N dc) -> RMN m dc unRMNUni (NP (Uni (Here Refl)) x) = x -- | @reduceDC@ embeds a mediated constructor into a mediation of its range. class DC dc => ReduceDC m dc where reduceDC :: 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