Reduce.hs

{-# 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)

A @t@-algebra reduces a disbanded @t@ into a mediation of @t@.

-}
module Data.Yoko.Reduce
  (Alg, Algebra(..), AlgebraU(..),
   algebraFin, AlgebraDT(..), AlgebraUni, AlgebraDC(..)) where

import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect





-- | A @t@-algebra reduces a disbanded @t@ to the same mediation of @t@.
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



-- | @algebraDT@ determines the algebra from the type and mediator.
class DT t => AlgebraDT m t where algebraDT :: Disbanded m t -> Med m t


-- | @algebraUni@ determines the \"algebra\" from the type-sum and mediator.
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

-- | @algebraDC@ determines the \"alegbra\" from the constructor type and
-- mediator.
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