Algebra.hs

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