--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi
  Copyright    :   ( c ) 2011  
-- License     :  BSD3
  Maintainer   :     <  > ,   <  >
-- Stability   :  experimental
  Portability :   non - portable ( GHC Extensions )
--
-- This module defines the infrastructure necessary to use
  /Generalised Compositional Data Types/. Generalised Compositional Data Types
  is an extension of Compositional Data Types with mutually recursive
  data types , and more generally GADTs . Examples of usage are bundled with the
  package in the library @examples\/Examples\/Multi@.
--
--------------------------------------------------------------------------------
module Data.Comp.Multi (
    module Data.Comp.Multi.Term
  , module Data.Comp.Multi.HFunctor
  , module Data.Comp.Multi.Algebra
  , module Data.Comp.Multi.Sum
  , module Data.Comp.Multi.Annotation
  , module Data.Comp.Multi.Equality
  , module Data.Comp.Multi.Generic
    ) where

import Data.Comp.Multi.Algebra
import Data.Comp.Multi.Annotation
import Data.Comp.Multi.Equality
import Data.Comp.Multi.Generic
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Sum
import Data.Comp.Multi.Term

  $ ex1 
 The example illustrates how to use generalised compositional data types 
 to implement a small expression language , with a sub language of values , and 
 an evaluation function mapping expressions to values . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > -- Signature for values and operators 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > 
 > -- Signature for the simple expression language 
 > type Sig = Op : + : Value 
 > 
 > -- Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 > $ ( derive [ makeHFunctor , makeHShowF ,  , smartConstructors ] 
 >           [ '' Value , '' Op ] ) 
 > 
 > -- Term evaluation algebra 
 > class Eval f v where 
 >    evalAlg : : Alg f ( Term v ) 
 > 
 > instance ( Eval f v ,   v ) = > Eval ( f : + : g ) v where 
 >    evalAlg (   ) = evalAlg x 
 >    evalAlg ( Inr x ) = evalAlg x 
 > 
 > -- Lift the evaluation algebra to a catamorphism 
 > eval : : ( HFunctor f ,   v ) = > Term f :-> Term v 
 > eval = cata evalAlg 
 > 
 > instance ( Value : < : v ) = > Eval Value v where 
 >    evalAlg = inject 
 > 
 > instance ( Value : < : v ) = > Eval Op v where 
 >    evalAlg ( Add x y )   = iConst $ ( projC x ) + ( projC y ) 
 >    evalAlg ( Mult x y ) = iConst $ ( projC x ) * ( projC y ) 
 >    evalAlg (   )     = fst $ projP x 
 >    evalAlg ( Snd x )     = snd $ projP x 
 > 
 > projC : : ( Value : < : v ) = > Term v Int - > Int 
 > projC v = case project v of Just ( Const n ) - > n 
 > 
 > projP : : ( Value : < : v ) = > Term v ( s , t ) - > ( Term v s , Term v t ) 
 > projP v = case project v of Just ( Pair x y ) - > ( x , y ) 
 > 
 > -- Example : evalEx = iConst 2 
 > evalEx : : Term Value Int 
 > evalEx = eval ( iFst $ iPair ( iConst 2 ) ( iConst 1 ) : : Term Sig Int ) 

The example illustrates how to use generalised compositional data types
to implement a small expression language, with a sub language of values, and
an evaluation function mapping expressions to values.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> -- Signature for values and operators
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
>
> -- Signature for the simple expression language
> type Sig = Op :+: Value
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors]
>          [''Value, ''Op])
>
> -- Term evaluation algebra
> class Eval f v where
>   evalAlg :: Alg f (Term v)
>
> instance (Eval f v, Eval g v) => Eval (f :+: g) v where
>   evalAlg (Inl x) = evalAlg x
>   evalAlg (Inr x) = evalAlg x
>
> -- Lift the evaluation algebra to a catamorphism
> eval :: (HFunctor f, Eval f v) => Term f :-> Term v
> eval = cata evalAlg
>
> instance (Value :<: v) => Eval Value v where
>   evalAlg = inject
>
> instance (Value :<: v) => Eval Op v where
>   evalAlg (Add x y)  = iConst $ (projC x) + (projC y)
>   evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
>   evalAlg (Fst x)    = fst $ projP x
>   evalAlg (Snd x)    = snd $ projP x
>
> projC :: (Value :<: v) => Term v Int -> Int
> projC v = case project v of Just (Const n) -> n
>
> projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
> projP v = case project v of Just (Pair x y) -> (x,y)
>
> -- Example: evalEx = iConst 2
> evalEx :: Term Value Int
> evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
-}

  $ ex2 
 The example illustrates how to use generalised compositional data types to 
 implement a small expression language , with a sub language of values , and a 
 monadic evaluation function mapping expressions to values . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > import Control .  ( liftM ) 
 > 
 > -- Signature for values and operators 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > 
 > -- Signature for the simple expression language 
 > type Sig = Op : + : Value 
 > 
 > -- Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 > $ ( derive [ makeHFunctor , makeHTraversable , makeHFoldable , 
 >             , makeHShowF , smartConstructors ] 
 >           [ '' Value , '' Op ] ) 
 > 
 > -- Monadic term evaluation algebra 
 > class  f v where 
 >    evalAlgM : : AlgM Maybe f ( Term v ) 
 > 
 > instance ( EvalM f v ,   v ) = > EvalM ( f : + : g ) v where 
 >    evalAlgM (   ) = evalAlgM x 
 >    evalAlgM ( Inr x ) = evalAlgM x 
 > 
 > evalM : : ( HTraversable f ,  f v ) = > Term f l - > Maybe ( Term v l ) 
 > evalM = cataM evalAlgM 
 > 
 > instance ( Value : < : v ) = > EvalM Value v where 
 >    evalAlgM = return . inject 
 > 
 > instance ( Value : < : v ) = > EvalM Op v where 
 >    evalAlgM ( Add x y )   = do n1 < - projC x 
 >                             n2 < - projC y 
 >                             return $ iConst $ n1 + n2 
 >    evalAlgM ( Mult x y ) = do n1 < - projC x 
 >                             n2 < - projC y 
 >                             return $ iConst $ n1 * n2 
 >    evalAlgM (  v )     = liftM fst $ projP v 
 >    evalAlgM ( Snd v )     = liftM snd $ projP v 
 > 
 > projC : : ( Value : < : v ) = > Term v Int - > Maybe Int 
 > projC v = case project v of 
 >              Just ( Const n ) - > return n ; _ - > Nothing 
 > 
 > projP : : ( Value : < : v ) = > Term v ( a , b ) - > Maybe ( Term v a , Term v b ) 
 > projP v = case project v of 
 >              Just ( Pair x y ) - > return ( x , y ) ; _ - > Nothing 
 > 
 > -- Example : evalMEx = Just ( iConst 5 ) 
 > evalMEx : : Maybe ( Term Value Int ) 
 > evalMEx = evalM ( ( iConst 1 ) ` iAdd ` 
 >                   ( iConst 2 ` iMult ` iConst 2 ) : : Term Sig Int ) 

The example illustrates how to use generalised compositional data types to
implement a small expression language, with a sub language of values, and a
monadic evaluation function mapping expressions to values.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
> import Control.Monad (liftM)
>
> -- Signature for values and operators
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
>
> -- Signature for the simple expression language
> type Sig = Op :+: Value
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
>           makeHEqF, makeHShowF, smartConstructors]
>          [''Value, ''Op])
>
> -- Monadic term evaluation algebra
> class EvalM f v where
>   evalAlgM :: AlgM Maybe f (Term v)
>
> instance (EvalM f v, EvalM g v) => EvalM (f :+: g) v where
>   evalAlgM (Inl x) = evalAlgM x
>   evalAlgM (Inr x) = evalAlgM x
>
> evalM :: (HTraversable f, EvalM f v) => Term f l -> Maybe (Term v l)
> evalM = cataM evalAlgM
>
> instance (Value :<: v) => EvalM Value v where
>   evalAlgM = return . inject
>
> instance (Value :<: v) => EvalM Op v where
>   evalAlgM (Add x y)  = do n1 <- projC x
>                            n2 <- projC y
>                            return $ iConst $ n1 + n2
>   evalAlgM (Mult x y) = do n1 <- projC x
>                            n2 <- projC y
>                            return $ iConst $ n1 * n2
>   evalAlgM (Fst v)    = liftM fst $ projP v
>   evalAlgM (Snd v)    = liftM snd $ projP v
>
> projC :: (Value :<: v) => Term v Int -> Maybe Int
> projC v = case project v of
>             Just (Const n) -> return n; _ -> Nothing
>
> projP :: (Value :<: v) => Term v (a,b) -> Maybe (Term v a, Term v b)
> projP v = case project v of
>             Just (Pair x y) -> return (x,y); _ -> Nothing
>
> -- Example: evalMEx = Just (iConst 5)
> evalMEx :: Maybe (Term Value Int)
> evalMEx = evalM ((iConst 1) `iAdd`
>                  (iConst 2 `iMult` iConst 2) :: Term Sig Int)
-}

  $ ex3 
 The example illustrates how to use generalised compositional data types 
 to implement a small expression language , and   an evaluation function mapping 
 intrinsically typed expressions to values . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > -- Signature for values and operators 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > 
 > -- Signature for the simple expression language 
 > type Sig = Op : + : Value 
 > 
 > -- Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 > $ ( derive [ makeHFunctor , makeHShowF ,  , smartConstructors ] 
 >           [ '' Value , '' Op ] ) 
 > 
 > -- Term evaluation algebra 
 > class EvalI f where 
 >    evalAlgI : : Alg f I 
 > 
 > instance ( EvalI f ,   ) = > EvalI ( f : + : g ) where 
 >    evalAlgI (   ) = evalAlgI x 
 >    evalAlgI ( Inr x ) = evalAlgI x 
 > 
 > -- Lift the evaluation algebra to a catamorphism 
 > evalI : : ( HFunctor f , EvalI f ) = > Term f i - > i 
 > evalI = unI . cata evalAlgI 
 > 
 > instance EvalI Value where 
 >    evalAlgI ( Const n ) = I n 
 >    evalAlgI ( Pair ( I x ) ( I y ) ) = I ( x , y ) 
 > 
 > instance EvalI Op where 
 >    evalAlgI ( Add ( I x ) ( I y ) )   = I ( x + y ) 
 >    evalAlgI ( Mult ( I x ) ( I y ) ) = I ( x * y ) 
 >    evalAlgI (  ( I ( x , _ ) ) )     = I x 
 >    evalAlgI ( Snd ( I ( _ , y ) ) )     = I y 
 > 
 > -- Example : evalEx = 2 
 > evalIEx : : Int 
 > evalIEx = evalI ( iFst $ iPair ( iConst 2 ) ( iConst 1 ) : : Term Sig Int ) 

The example illustrates how to use generalised compositional data types
to implement a small expression language, and  an evaluation function mapping
intrinsically typed expressions to values.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> -- Signature for values and operators
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
>
> -- Signature for the simple expression language
> type Sig = Op :+: Value
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors]
>          [''Value, ''Op])
>
> -- Term evaluation algebra
> class EvalI f where
>   evalAlgI :: Alg f I
>
> instance (EvalI f, EvalI g) => EvalI (f :+: g) where
>   evalAlgI (Inl x) = evalAlgI x
>   evalAlgI (Inr x) = evalAlgI x
>
> -- Lift the evaluation algebra to a catamorphism
> evalI :: (HFunctor f, EvalI f) => Term f i -> i
> evalI = unI . cata evalAlgI
>
> instance EvalI Value where
>   evalAlgI (Const n) = I n
>   evalAlgI (Pair (I x) (I y)) = I (x,y)
>
> instance EvalI Op where
>   evalAlgI (Add (I x) (I y))  = I (x + y)
>   evalAlgI (Mult (I x) (I y)) = I (x * y)
>   evalAlgI (Fst (I (x,_)))    = I x
>   evalAlgI (Snd (I (_,y)))    = I y
>
> -- Example: evalEx = 2
> evalIEx :: Int
> evalIEx = evalI (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
-}

  $ ex4 
 The example illustrates how to compose a term homomorphism and an algebra , 
 exemplified via a desugaring term homomorphism and an evaluation algebra . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > -- Signature for values , operators , and syntactic sugar 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > data Sugar e l where 
 >    Neg    : : e Int    - > Sugar e Int 
 >    Swap   : : e ( s , t ) - > Sugar e ( t , s ) 
 > 
 > -- Source position information ( line number , column number ) 
 > data Pos = Pos Int Int 
 >             deriving Show 
 > 
 > -- Signature for the simple expression language 
 > type Sig = Op : + : Value 
 > type SigP = Op : & : Pos : + : Value : & : Pos 
 > 
 > -- Signature for the simple expression language , extended with syntactic sugar 
 > type Sig ' = Sugar : + : Op : + : Value 
 > type SigP ' = Sugar : & : Pos : + : Op : & : Pos : + : Value : & : Pos 
 > 
 > -- Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 > $ ( derive [ makeHFunctor , makeHTraversable , makeHFoldable , 
 >             , makeHShowF , smartConstructors ] 
 >           [ '' Value , '' Op , '' Sugar ] ) 
 > 
 > -- Term homomorphism for desugaring of terms 
 > class ( HFunctor f ,   ) = >  f g where 
 >    desugHom : :    
 >    desugHom = desugHom ' .   
 >    desugHom ' : : Alg f ( Context g a ) 
 >    desugHom ' x = appCxt ( desugHom x ) 
 > 
 > instance (  f h ,   h ) = >  ( f : + : g ) h where 
 >    desugHom (   ) = desugHom x 
 >    desugHom ( Inr x ) = desugHom x 
 >    desugHom ' (   ) = desugHom ' x 
 >    desugHom ' ( Inr x ) = desugHom ' x 
 > 
 > instance ( Value : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , Value : < : v , HFunctor v ) = >   v where 
 >    desugHom ' (   )   = iConst ( -1 ) ` iMult ` x 
 >    desugHom ' ( Swap x ) = iSnd x ` iPair ` iFst x 
 > 
 > -- Term evaluation algebra 
 > class Eval f v where 
 >    evalAlg : : Alg f ( Term v ) 
 > 
 > instance ( Eval f v ,   v ) = > Eval ( f : + : g ) v where 
 >    evalAlg (   ) = evalAlg x 
 >    evalAlg ( Inr x ) = evalAlg x 
 > 
 > instance ( Value : < : v ) = > Eval Value v where 
 >    evalAlg = inject 
 > 
 > instance ( Value : < : v ) = > Eval Op v where 
 >    evalAlg ( Add x y )   = iConst $ ( projC x ) + ( projC y ) 
 >    evalAlg ( Mult x y ) = iConst $ ( projC x ) * ( projC y ) 
 >    evalAlg (   )     = fst $ projP x 
 >    evalAlg ( Snd x )     = snd $ projP x 
 > 
 > projC : : ( Value : < : v ) = > Term v Int - > Int 
 > projC v = case project v of Just ( Const n ) - > n 
 > 
 > projP : : ( Value : < : v ) = > Term v ( s , t ) - > ( Term v s , Term v t ) 
 > projP v = case project v of Just ( Pair x y ) - > ( x , y ) 
 > 
 > -- Compose the evaluation algebra and the desugaring homomorphism to an 
 > -- algebra 
 > eval : : Term Sig ' :-> Term Value 
 > eval = cata ( evalAlg ` compAlg ` ( desugHom : :    Sig ) ) 
 > 
 > -- Example : evalEx = iPair ( iConst 2 ) ( iConst 1 ) 
 > evalEx : : Term Value ( Int , Int ) 
 > evalEx = eval $ iSwap $ iPair ( iConst 1 ) ( iConst 2 ) 

The example illustrates how to compose a term homomorphism and an algebra,
exemplified via a desugaring term homomorphism and an evaluation algebra.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> -- Signature for values, operators, and syntactic sugar
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
> data Sugar e l where
>   Neg   :: e Int   -> Sugar e Int
>   Swap  :: e (s,t) -> Sugar e (t,s)
>
> -- Source position information (line number, column number)
> data Pos = Pos Int Int
>            deriving Show
>
> -- Signature for the simple expression language
> type Sig = Op :+: Value
> type SigP = Op :&: Pos :+: Value :&: Pos
>
> -- Signature for the simple expression language, extended with syntactic sugar
> type Sig' = Sugar :+: Op :+: Value
> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
>           makeHEqF, makeHShowF, smartConstructors]
>          [''Value, ''Op, ''Sugar])
>
> -- Term homomorphism for desugaring of terms
> class (HFunctor f, HFunctor g) => Desugar f g where
>   desugHom :: Hom f g
>   desugHom = desugHom' . hfmap Hole
>   desugHom' :: Alg f (Context g a)
>   desugHom' x = appCxt (desugHom x)
>
> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
>   desugHom (Inl x) = desugHom x
>   desugHom (Inr x) = desugHom x
>   desugHom' (Inl x) = desugHom' x
>   desugHom' (Inr x) = desugHom' x
>
> instance (Value :<: v, HFunctor v) => Desugar Value v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, HFunctor v) => Desugar Op v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
>   desugHom' (Neg x)  = iConst (-1) `iMult` x
>   desugHom' (Swap x) = iSnd x `iPair` iFst x
>
> -- Term evaluation algebra
> class Eval f v where
>   evalAlg :: Alg f (Term v)
>
> instance (Eval f v, Eval g v) => Eval (f :+: g) v where
>   evalAlg (Inl x) = evalAlg x
>   evalAlg (Inr x) = evalAlg x
>
> instance (Value :<: v) => Eval Value v where
>   evalAlg = inject
>
> instance (Value :<: v) => Eval Op v where
>   evalAlg (Add x y)  = iConst $ (projC x) + (projC y)
>   evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
>   evalAlg (Fst x)    = fst $ projP x
>   evalAlg (Snd x)    = snd $ projP x
>
> projC :: (Value :<: v) => Term v Int -> Int
> projC v = case project v of Just (Const n) -> n
>
> projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
> projP v = case project v of Just (Pair x y) -> (x,y)
>
> -- Compose the evaluation algebra and the desugaring homomorphism to an
> -- algebra
> eval :: Term Sig' :-> Term Value
> eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))
>
> -- Example: evalEx = iPair (iConst 2) (iConst 1)
> evalEx :: Term Value (Int,Int)
> evalEx = eval $ iSwap $ iPair (iConst 1) (iConst 2)
-}

  $ ex5 
 The example illustrates how to lift a term homomorphism to annotations , 
 exemplified via a desugaring term homomorphism lifted to terms annotated with 
 source position information . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > -- Signature for values , operators , and syntactic sugar 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > data Sugar e l where 
 >    Neg    : : e Int    - > Sugar e Int 
 >    Swap   : : e ( s , t ) - > Sugar e ( t , s ) 
 > 
 > -- Source position information ( line number , column number ) 
 > data Pos = Pos Int Int 
 >             deriving ( Show , Eq ) 
 > 
 > -- Signature for the simple expression language 
 > type Sig = Op : + : Value 
 > type SigP = Op : & : Pos : + : Value : & : Pos 
 > 
 > -- Signature for the simple expression language , extended with syntactic sugar 
 > type Sig ' = Sugar : + : Op : + : Value 
 > type SigP ' = Sugar : & : Pos : + : Op : & : Pos : + : Value : & : Pos 
 > 
 > -- Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 > $ ( derive [ makeHFunctor , makeHTraversable , makeHFoldable , 
 >             , makeHShowF , smartConstructors ] 
 >           [ '' Value , '' Op , '' Sugar ] ) 
 > 
 > -- Term homomorphism for desugaring of terms 
 > class ( HFunctor f ,   ) = >  f g where 
 >    desugHom : :    
 >    desugHom = desugHom ' .   
 >    desugHom ' : : Alg f ( Context g a ) 
 >    desugHom ' x = appCxt ( desugHom x ) 
 > 
 > instance (  f h ,   h ) = >  ( f : + : g ) h where 
 >    desugHom (   ) = desugHom x 
 >    desugHom ( Inr x ) = desugHom x 
 >    desugHom ' (   ) = desugHom ' x 
 >    desugHom ' ( Inr x ) = desugHom ' x 
 > 
 > instance ( Value : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , Value : < : v , HFunctor v ) = >   v where 
 >    desugHom ' (   )   = iConst ( -1 ) ` iMult ` x 
 >    desugHom ' ( Swap x ) = iSnd x ` iPair ` iFst x 
 > 
 > -- Lift the desugaring term homomorphism to a catamorphism 
 > desug : : Term Sig ' :-> Term Sig 
 > desug = appHom desugHom 
 > 
 > -- Example : desugEx = iPair ( iConst 2 ) ( iConst 1 ) 
 > desugEx : : Term Sig ( Int , Int ) 
 > desugEx = desug $ iSwap $ iPair ( iConst 1 ) ( iConst 2 ) 
 > 
 > -- Lift desugaring to terms annotated with source positions 
 > desugP : : Term SigP ' :-> Term SigP 
 > desugP = appHom (   ) 
 > 
 > iSwapP : : ( DistAnn f p f ' , Sugar : < : f ) = > p - > Term f ' ( a , b ) - > Term f ' ( b , a ) 
 > iSwapP p x = Term ( injectA p $ inj $ Swap x ) 
 > 
 > iConstP : : ( DistAnn f p f ' , Value : < : f ) = > p - > Int - > Term f ' Int 
 > iConstP p x = Term ( injectA p $ inj $ Const x ) 
 > 
 > iPairP : : ( DistAnn f p f ' , Value : < : f ) = > p - > Term f ' a - > Term f ' b - > Term f ' ( a , b ) 
 > iPairP p x y = Term ( injectA p $ inj $ Pair x y ) 
 > 
 > iFstP : : ( DistAnn f p f ' , Op : < : f ) = > p - > Term f ' ( a , b ) - > Term f ' a 
 > iFstP p x = Term ( injectA p $ inj $ Fst x ) 
 > 
 > iSndP : : ( DistAnn f p f ' , Op : < : f ) = > p - > Term f ' ( a , b ) - > Term f ' b 
 >      ( injectA p $ inj $ Snd x ) 
 > 
 > -- Example :  = iPairP ( Pos 1 0 ) 
 > --                             ( iSndP ( Pos 1 0 ) ( iPairP ( Pos 1 1 ) 
 > --                                                      ( iConstP ( Pos 1 2 ) 1 ) 
 > --                                                      ( iConstP ( Pos 1 3 ) 2 ) ) ) 
 > --                             ( iFstP ( Pos 1 0 ) ( iPairP ( Pos 1 1 ) 
 > --                                                      ( iConstP ( Pos 1 2 ) 1 ) 
 > --                                                      ( iConstP ( Pos 1 3 ) 2 ) ) ) 
 > desugPEx : : Term SigP ( Int , Int ) 
 >  = desugP $ iSwapP ( Pos 1 0 ) ( iPairP ( Pos 1 1 ) ( iConstP ( Pos 1 2 ) 1 ) 
 >                                                         ( iConstP ( Pos 1 3 ) 2 ) ) 

The example illustrates how to lift a term homomorphism to annotations,
exemplified via a desugaring term homomorphism lifted to terms annotated with
source position information.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> -- Signature for values, operators, and syntactic sugar
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
> data Sugar e l where
>   Neg   :: e Int   -> Sugar e Int
>   Swap  :: e (s,t) -> Sugar e (t,s)
>
> -- Source position information (line number, column number)
> data Pos = Pos Int Int
>            deriving (Show, Eq)
>
> -- Signature for the simple expression language
> type Sig = Op :+: Value
> type SigP = Op :&: Pos :+: Value :&: Pos
>
> -- Signature for the simple expression language, extended with syntactic sugar
> type Sig' = Sugar :+: Op :+: Value
> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
>
> -- Derive boilerplate code using Template Haskell (GHC 7 needed)
> $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
>           makeHEqF, makeHShowF, smartConstructors]
>          [''Value, ''Op, ''Sugar])
>
> -- Term homomorphism for desugaring of terms
> class (HFunctor f, HFunctor g) => Desugar f g where
>   desugHom :: Hom f g
>   desugHom = desugHom' . hfmap Hole
>   desugHom' :: Alg f (Context g a)
>   desugHom' x = appCxt (desugHom x)
>
> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
>   desugHom (Inl x) = desugHom x
>   desugHom (Inr x) = desugHom x
>   desugHom' (Inl x) = desugHom' x
>   desugHom' (Inr x) = desugHom' x
>
> instance (Value :<: v, HFunctor v) => Desugar Value v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, HFunctor v) => Desugar Op v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
>   desugHom' (Neg x)  = iConst (-1) `iMult` x
>   desugHom' (Swap x) = iSnd x `iPair` iFst x
>
> -- Lift the desugaring term homomorphism to a catamorphism
> desug :: Term Sig' :-> Term Sig
> desug = appHom desugHom
>
> -- Example: desugEx = iPair (iConst 2) (iConst 1)
> desugEx :: Term Sig (Int,Int)
> desugEx = desug $ iSwap $ iPair (iConst 1) (iConst 2)
>
> -- Lift desugaring to terms annotated with source positions
> desugP :: Term SigP' :-> Term SigP
> desugP = appHom (propAnn desugHom)
>
> iSwapP :: (DistAnn f p f', Sugar :<: f) => p -> Term f' (a,b) -> Term f' (b,a)
> iSwapP p x = Term (injectA p $ inj $ Swap x)
>
> iConstP :: (DistAnn f p f', Value :<: f) => p -> Int -> Term f' Int
> iConstP p x = Term (injectA p $ inj $ Const x)
>
> iPairP :: (DistAnn f p f', Value :<: f) => p -> Term f' a -> Term f' b -> Term f' (a,b)
> iPairP p x y = Term (injectA p $ inj $ Pair x y)
>
> iFstP :: (DistAnn f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' a
> iFstP p x = Term (injectA p $ inj $ Fst x)
>
> iSndP :: (DistAnn f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' b
> iSndP p x = Term (injectA p $ inj $ Snd x)
>
> -- Example: desugPEx = iPairP (Pos 1 0)
> --                            (iSndP (Pos 1 0) (iPairP (Pos 1 1)
> --                                                     (iConstP (Pos 1 2) 1)
> --                                                     (iConstP (Pos 1 3) 2)))
> --                            (iFstP (Pos 1 0) (iPairP (Pos 1 1)
> --                                                     (iConstP (Pos 1 2) 1)
> --                                                     (iConstP (Pos 1 3) 2)))
> desugPEx :: Term SigP (Int,Int)
> desugPEx = desugP $ iSwapP (Pos 1 0) (iPairP (Pos 1 1) (iConstP (Pos 1 2) 1)
>                                                        (iConstP (Pos 1 3) 2))
-}

------------------------------------------------------------------------------
 |
 Module      :  Data.Comp.Multi
 License     :  BSD3
 Stability   :  experimental

 This module defines the infrastructure necessary to use

------------------------------------------------------------------------------
 Signature for values and operators 
 Signature for the simple expression language 
 Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 Term evaluation algebra 
 Lift the evaluation algebra to a catamorphism 
 Example : evalEx = iConst 2 
 Signature for values and operators
 Signature for the simple expression language
 Derive boilerplate code using Template Haskell (GHC 7 needed)
 Term evaluation algebra
 Lift the evaluation algebra to a catamorphism
 Example: evalEx = iConst 2
 Signature for values and operators 
 Signature for the simple expression language 
 Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 Monadic term evaluation algebra 
 Example : evalMEx = Just ( iConst 5 ) 
 Signature for values and operators
 Signature for the simple expression language
 Derive boilerplate code using Template Haskell (GHC 7 needed)
 Monadic term evaluation algebra
 Example: evalMEx = Just (iConst 5)
 Signature for values and operators 
 Signature for the simple expression language 
 Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 Term evaluation algebra 
 Lift the evaluation algebra to a catamorphism 
 Example : evalEx = 2 
 Signature for values and operators
 Signature for the simple expression language
 Derive boilerplate code using Template Haskell (GHC 7 needed)
 Term evaluation algebra
 Lift the evaluation algebra to a catamorphism
 Example: evalEx = 2
 Signature for values , operators , and syntactic sugar 
 Source position information ( line number , column number ) 
 Signature for the simple expression language 
 Signature for the simple expression language , extended with syntactic sugar 
 Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 Term homomorphism for desugaring of terms 
 Term evaluation algebra 
 Compose the evaluation algebra and the desugaring homomorphism to an 
 algebra 
 Example : evalEx = iPair ( iConst 2 ) ( iConst 1 ) 
 Signature for values, operators, and syntactic sugar
 Source position information (line number, column number)
 Signature for the simple expression language
 Signature for the simple expression language, extended with syntactic sugar
 Derive boilerplate code using Template Haskell (GHC 7 needed)
 Term homomorphism for desugaring of terms
 Term evaluation algebra
 Compose the evaluation algebra and the desugaring homomorphism to an
 algebra
 Example: evalEx = iPair (iConst 2) (iConst 1)
 Signature for values , operators , and syntactic sugar 
 Source position information ( line number , column number ) 
 Signature for the simple expression language 
 Signature for the simple expression language , extended with syntactic sugar 
 Derive boilerplate code using Template Haskell ( GHC 7 needed ) 
 Term homomorphism for desugaring of terms 
 Lift the desugaring term homomorphism to a catamorphism 
 Example : desugEx = iPair ( iConst 2 ) ( iConst 1 ) 
 Lift desugaring to terms annotated with source positions 
 Example :  = iPairP ( Pos 1 0 ) 
                             ( iSndP ( Pos 1 0 ) ( iPairP ( Pos 1 1 ) 
                                                      ( iConstP ( Pos 1 2 ) 1 ) 
                                                      ( iConstP ( Pos 1 3 ) 2 ) ) ) 
                             ( iFstP ( Pos 1 0 ) ( iPairP ( Pos 1 1 ) 
                                                      ( iConstP ( Pos 1 2 ) 1 ) 
                                                      ( iConstP ( Pos 1 3 ) 2 ) ) ) 
 Signature for values, operators, and syntactic sugar
 Source position information (line number, column number)
 Signature for the simple expression language
 Signature for the simple expression language, extended with syntactic sugar
 Derive boilerplate code using Template Haskell (GHC 7 needed)
 Term homomorphism for desugaring of terms
 Lift the desugaring term homomorphism to a catamorphism
 Example: desugEx = iPair (iConst 2) (iConst 1)
 Lift desugaring to terms annotated with source positions
 Example: desugPEx = iPairP (Pos 1 0)
                            (iSndP (Pos 1 0) (iPairP (Pos 1 1)
                                                     (iConstP (Pos 1 2) 1)
                                                     (iConstP (Pos 1 3) 2)))
                            (iFstP (Pos 1 0) (iPairP (Pos 1 1)
                                                     (iConstP (Pos 1 2) 1)
                                                     (iConstP (Pos 1 3) 2)))
  Copyright    :   ( c ) 2011  
  Maintainer   :     <  > ,   <  >
  Portability :   non - portable ( GHC Extensions )
  /Generalised Compositional Data Types/. Generalised Compositional Data Types
  is an extension of Compositional Data Types with mutually recursive
  data types , and more generally GADTs . Examples of usage are bundled with the
  package in the library @examples\/Examples\/Multi@.
module Data.Comp.Multi (
    module Data.Comp.Multi.Term
  , module Data.Comp.Multi.HFunctor
  , module Data.Comp.Multi.Algebra
  , module Data.Comp.Multi.Sum
  , module Data.Comp.Multi.Annotation
  , module Data.Comp.Multi.Equality
  , module Data.Comp.Multi.Generic
    ) where

import Data.Comp.Multi.Algebra
import Data.Comp.Multi.Annotation
import Data.Comp.Multi.Equality
import Data.Comp.Multi.Generic
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Sum
import Data.Comp.Multi.Term

  $ ex1 
 The example illustrates how to use generalised compositional data types 
 to implement a small expression language , with a sub language of values , and 
 an evaluation function mapping expressions to values . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > 
 > type Sig = Op : + : Value 
 > 
 > $ ( derive [ makeHFunctor , makeHShowF ,  , smartConstructors ] 
 >           [ '' Value , '' Op ] ) 
 > 
 > class Eval f v where 
 >    evalAlg : : Alg f ( Term v ) 
 > 
 > instance ( Eval f v ,   v ) = > Eval ( f : + : g ) v where 
 >    evalAlg (   ) = evalAlg x 
 >    evalAlg ( Inr x ) = evalAlg x 
 > 
 > eval : : ( HFunctor f ,   v ) = > Term f :-> Term v 
 > eval = cata evalAlg 
 > 
 > instance ( Value : < : v ) = > Eval Value v where 
 >    evalAlg = inject 
 > 
 > instance ( Value : < : v ) = > Eval Op v where 
 >    evalAlg ( Add x y )   = iConst $ ( projC x ) + ( projC y ) 
 >    evalAlg ( Mult x y ) = iConst $ ( projC x ) * ( projC y ) 
 >    evalAlg (   )     = fst $ projP x 
 >    evalAlg ( Snd x )     = snd $ projP x 
 > 
 > projC : : ( Value : < : v ) = > Term v Int - > Int 
 > projC v = case project v of Just ( Const n ) - > n 
 > 
 > projP : : ( Value : < : v ) = > Term v ( s , t ) - > ( Term v s , Term v t ) 
 > projP v = case project v of Just ( Pair x y ) - > ( x , y ) 
 > 
 > evalEx : : Term Value Int 
 > evalEx = eval ( iFst $ iPair ( iConst 2 ) ( iConst 1 ) : : Term Sig Int ) 

The example illustrates how to use generalised compositional data types
to implement a small expression language, with a sub language of values, and
an evaluation function mapping expressions to values.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
>
> type Sig = Op :+: Value
>
> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors]
>          [''Value, ''Op])
>
> class Eval f v where
>   evalAlg :: Alg f (Term v)
>
> instance (Eval f v, Eval g v) => Eval (f :+: g) v where
>   evalAlg (Inl x) = evalAlg x
>   evalAlg (Inr x) = evalAlg x
>
> eval :: (HFunctor f, Eval f v) => Term f :-> Term v
> eval = cata evalAlg
>
> instance (Value :<: v) => Eval Value v where
>   evalAlg = inject
>
> instance (Value :<: v) => Eval Op v where
>   evalAlg (Add x y)  = iConst $ (projC x) + (projC y)
>   evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
>   evalAlg (Fst x)    = fst $ projP x
>   evalAlg (Snd x)    = snd $ projP x
>
> projC :: (Value :<: v) => Term v Int -> Int
> projC v = case project v of Just (Const n) -> n
>
> projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
> projP v = case project v of Just (Pair x y) -> (x,y)
>
> evalEx :: Term Value Int
> evalEx = eval (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
-}

  $ ex2 
 The example illustrates how to use generalised compositional data types to 
 implement a small expression language , with a sub language of values , and a 
 monadic evaluation function mapping expressions to values . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > import Control .  ( liftM ) 
 > 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > 
 > type Sig = Op : + : Value 
 > 
 > $ ( derive [ makeHFunctor , makeHTraversable , makeHFoldable , 
 >             , makeHShowF , smartConstructors ] 
 >           [ '' Value , '' Op ] ) 
 > 
 > class  f v where 
 >    evalAlgM : : AlgM Maybe f ( Term v ) 
 > 
 > instance ( EvalM f v ,   v ) = > EvalM ( f : + : g ) v where 
 >    evalAlgM (   ) = evalAlgM x 
 >    evalAlgM ( Inr x ) = evalAlgM x 
 > 
 > evalM : : ( HTraversable f ,  f v ) = > Term f l - > Maybe ( Term v l ) 
 > evalM = cataM evalAlgM 
 > 
 > instance ( Value : < : v ) = > EvalM Value v where 
 >    evalAlgM = return . inject 
 > 
 > instance ( Value : < : v ) = > EvalM Op v where 
 >    evalAlgM ( Add x y )   = do n1 < - projC x 
 >                             n2 < - projC y 
 >                             return $ iConst $ n1 + n2 
 >    evalAlgM ( Mult x y ) = do n1 < - projC x 
 >                             n2 < - projC y 
 >                             return $ iConst $ n1 * n2 
 >    evalAlgM (  v )     = liftM fst $ projP v 
 >    evalAlgM ( Snd v )     = liftM snd $ projP v 
 > 
 > projC : : ( Value : < : v ) = > Term v Int - > Maybe Int 
 > projC v = case project v of 
 >              Just ( Const n ) - > return n ; _ - > Nothing 
 > 
 > projP : : ( Value : < : v ) = > Term v ( a , b ) - > Maybe ( Term v a , Term v b ) 
 > projP v = case project v of 
 >              Just ( Pair x y ) - > return ( x , y ) ; _ - > Nothing 
 > 
 > evalMEx : : Maybe ( Term Value Int ) 
 > evalMEx = evalM ( ( iConst 1 ) ` iAdd ` 
 >                   ( iConst 2 ` iMult ` iConst 2 ) : : Term Sig Int ) 

The example illustrates how to use generalised compositional data types to
implement a small expression language, with a sub language of values, and a
monadic evaluation function mapping expressions to values.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
> import Control.Monad (liftM)
>
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
>
> type Sig = Op :+: Value
>
> $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
>           makeHEqF, makeHShowF, smartConstructors]
>          [''Value, ''Op])
>
> class EvalM f v where
>   evalAlgM :: AlgM Maybe f (Term v)
>
> instance (EvalM f v, EvalM g v) => EvalM (f :+: g) v where
>   evalAlgM (Inl x) = evalAlgM x
>   evalAlgM (Inr x) = evalAlgM x
>
> evalM :: (HTraversable f, EvalM f v) => Term f l -> Maybe (Term v l)
> evalM = cataM evalAlgM
>
> instance (Value :<: v) => EvalM Value v where
>   evalAlgM = return . inject
>
> instance (Value :<: v) => EvalM Op v where
>   evalAlgM (Add x y)  = do n1 <- projC x
>                            n2 <- projC y
>                            return $ iConst $ n1 + n2
>   evalAlgM (Mult x y) = do n1 <- projC x
>                            n2 <- projC y
>                            return $ iConst $ n1 * n2
>   evalAlgM (Fst v)    = liftM fst $ projP v
>   evalAlgM (Snd v)    = liftM snd $ projP v
>
> projC :: (Value :<: v) => Term v Int -> Maybe Int
> projC v = case project v of
>             Just (Const n) -> return n; _ -> Nothing
>
> projP :: (Value :<: v) => Term v (a,b) -> Maybe (Term v a, Term v b)
> projP v = case project v of
>             Just (Pair x y) -> return (x,y); _ -> Nothing
>
> evalMEx :: Maybe (Term Value Int)
> evalMEx = evalM ((iConst 1) `iAdd`
>                  (iConst 2 `iMult` iConst 2) :: Term Sig Int)
-}

  $ ex3 
 The example illustrates how to use generalised compositional data types 
 to implement a small expression language , and   an evaluation function mapping 
 intrinsically typed expressions to values . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > 
 > type Sig = Op : + : Value 
 > 
 > $ ( derive [ makeHFunctor , makeHShowF ,  , smartConstructors ] 
 >           [ '' Value , '' Op ] ) 
 > 
 > class EvalI f where 
 >    evalAlgI : : Alg f I 
 > 
 > instance ( EvalI f ,   ) = > EvalI ( f : + : g ) where 
 >    evalAlgI (   ) = evalAlgI x 
 >    evalAlgI ( Inr x ) = evalAlgI x 
 > 
 > evalI : : ( HFunctor f , EvalI f ) = > Term f i - > i 
 > evalI = unI . cata evalAlgI 
 > 
 > instance EvalI Value where 
 >    evalAlgI ( Const n ) = I n 
 >    evalAlgI ( Pair ( I x ) ( I y ) ) = I ( x , y ) 
 > 
 > instance EvalI Op where 
 >    evalAlgI ( Add ( I x ) ( I y ) )   = I ( x + y ) 
 >    evalAlgI ( Mult ( I x ) ( I y ) ) = I ( x * y ) 
 >    evalAlgI (  ( I ( x , _ ) ) )     = I x 
 >    evalAlgI ( Snd ( I ( _ , y ) ) )     = I y 
 > 
 > evalIEx : : Int 
 > evalIEx = evalI ( iFst $ iPair ( iConst 2 ) ( iConst 1 ) : : Term Sig Int ) 

The example illustrates how to use generalised compositional data types
to implement a small expression language, and  an evaluation function mapping
intrinsically typed expressions to values.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
>
> type Sig = Op :+: Value
>
> $(derive [makeHFunctor, makeHShowF, makeHEqF, smartConstructors]
>          [''Value, ''Op])
>
> class EvalI f where
>   evalAlgI :: Alg f I
>
> instance (EvalI f, EvalI g) => EvalI (f :+: g) where
>   evalAlgI (Inl x) = evalAlgI x
>   evalAlgI (Inr x) = evalAlgI x
>
> evalI :: (HFunctor f, EvalI f) => Term f i -> i
> evalI = unI . cata evalAlgI
>
> instance EvalI Value where
>   evalAlgI (Const n) = I n
>   evalAlgI (Pair (I x) (I y)) = I (x,y)
>
> instance EvalI Op where
>   evalAlgI (Add (I x) (I y))  = I (x + y)
>   evalAlgI (Mult (I x) (I y)) = I (x * y)
>   evalAlgI (Fst (I (x,_)))    = I x
>   evalAlgI (Snd (I (_,y)))    = I y
>
> evalIEx :: Int
> evalIEx = evalI (iFst $ iPair (iConst 2) (iConst 1) :: Term Sig Int)
-}

  $ ex4 
 The example illustrates how to compose a term homomorphism and an algebra , 
 exemplified via a desugaring term homomorphism and an evaluation algebra . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > data Sugar e l where 
 >    Neg    : : e Int    - > Sugar e Int 
 >    Swap   : : e ( s , t ) - > Sugar e ( t , s ) 
 > 
 > data Pos = Pos Int Int 
 >             deriving Show 
 > 
 > type Sig = Op : + : Value 
 > type SigP = Op : & : Pos : + : Value : & : Pos 
 > 
 > type Sig ' = Sugar : + : Op : + : Value 
 > type SigP ' = Sugar : & : Pos : + : Op : & : Pos : + : Value : & : Pos 
 > 
 > $ ( derive [ makeHFunctor , makeHTraversable , makeHFoldable , 
 >             , makeHShowF , smartConstructors ] 
 >           [ '' Value , '' Op , '' Sugar ] ) 
 > 
 > class ( HFunctor f ,   ) = >  f g where 
 >    desugHom : :    
 >    desugHom = desugHom ' .   
 >    desugHom ' : : Alg f ( Context g a ) 
 >    desugHom ' x = appCxt ( desugHom x ) 
 > 
 > instance (  f h ,   h ) = >  ( f : + : g ) h where 
 >    desugHom (   ) = desugHom x 
 >    desugHom ( Inr x ) = desugHom x 
 >    desugHom ' (   ) = desugHom ' x 
 >    desugHom ' ( Inr x ) = desugHom ' x 
 > 
 > instance ( Value : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , Value : < : v , HFunctor v ) = >   v where 
 >    desugHom ' (   )   = iConst ( -1 ) ` iMult ` x 
 >    desugHom ' ( Swap x ) = iSnd x ` iPair ` iFst x 
 > 
 > class Eval f v where 
 >    evalAlg : : Alg f ( Term v ) 
 > 
 > instance ( Eval f v ,   v ) = > Eval ( f : + : g ) v where 
 >    evalAlg (   ) = evalAlg x 
 >    evalAlg ( Inr x ) = evalAlg x 
 > 
 > instance ( Value : < : v ) = > Eval Value v where 
 >    evalAlg = inject 
 > 
 > instance ( Value : < : v ) = > Eval Op v where 
 >    evalAlg ( Add x y )   = iConst $ ( projC x ) + ( projC y ) 
 >    evalAlg ( Mult x y ) = iConst $ ( projC x ) * ( projC y ) 
 >    evalAlg (   )     = fst $ projP x 
 >    evalAlg ( Snd x )     = snd $ projP x 
 > 
 > projC : : ( Value : < : v ) = > Term v Int - > Int 
 > projC v = case project v of Just ( Const n ) - > n 
 > 
 > projP : : ( Value : < : v ) = > Term v ( s , t ) - > ( Term v s , Term v t ) 
 > projP v = case project v of Just ( Pair x y ) - > ( x , y ) 
 > 
 > eval : : Term Sig ' :-> Term Value 
 > eval = cata ( evalAlg ` compAlg ` ( desugHom : :    Sig ) ) 
 > 
 > evalEx : : Term Value ( Int , Int ) 
 > evalEx = eval $ iSwap $ iPair ( iConst 1 ) ( iConst 2 ) 

The example illustrates how to compose a term homomorphism and an algebra,
exemplified via a desugaring term homomorphism and an evaluation algebra.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
> data Sugar e l where
>   Neg   :: e Int   -> Sugar e Int
>   Swap  :: e (s,t) -> Sugar e (t,s)
>
> data Pos = Pos Int Int
>            deriving Show
>
> type Sig = Op :+: Value
> type SigP = Op :&: Pos :+: Value :&: Pos
>
> type Sig' = Sugar :+: Op :+: Value
> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
>
> $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
>           makeHEqF, makeHShowF, smartConstructors]
>          [''Value, ''Op, ''Sugar])
>
> class (HFunctor f, HFunctor g) => Desugar f g where
>   desugHom :: Hom f g
>   desugHom = desugHom' . hfmap Hole
>   desugHom' :: Alg f (Context g a)
>   desugHom' x = appCxt (desugHom x)
>
> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
>   desugHom (Inl x) = desugHom x
>   desugHom (Inr x) = desugHom x
>   desugHom' (Inl x) = desugHom' x
>   desugHom' (Inr x) = desugHom' x
>
> instance (Value :<: v, HFunctor v) => Desugar Value v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, HFunctor v) => Desugar Op v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
>   desugHom' (Neg x)  = iConst (-1) `iMult` x
>   desugHom' (Swap x) = iSnd x `iPair` iFst x
>
> class Eval f v where
>   evalAlg :: Alg f (Term v)
>
> instance (Eval f v, Eval g v) => Eval (f :+: g) v where
>   evalAlg (Inl x) = evalAlg x
>   evalAlg (Inr x) = evalAlg x
>
> instance (Value :<: v) => Eval Value v where
>   evalAlg = inject
>
> instance (Value :<: v) => Eval Op v where
>   evalAlg (Add x y)  = iConst $ (projC x) + (projC y)
>   evalAlg (Mult x y) = iConst $ (projC x) * (projC y)
>   evalAlg (Fst x)    = fst $ projP x
>   evalAlg (Snd x)    = snd $ projP x
>
> projC :: (Value :<: v) => Term v Int -> Int
> projC v = case project v of Just (Const n) -> n
>
> projP :: (Value :<: v) => Term v (s,t) -> (Term v s, Term v t)
> projP v = case project v of Just (Pair x y) -> (x,y)
>
> eval :: Term Sig' :-> Term Value
> eval = cata (evalAlg `compAlg` (desugHom :: Hom Sig' Sig))
>
> evalEx :: Term Value (Int,Int)
> evalEx = eval $ iSwap $ iPair (iConst 1) (iConst 2)
-}

  $ ex5 
 The example illustrates how to lift a term homomorphism to annotations , 
 exemplified via a desugaring term homomorphism lifted to terms annotated with 
 source position information . 

 The following language extensions are needed in order to run the example : 
 @TemplateHaskell@ , @TypeOperators@ , @MultiParamTypeClasses@ , 
 @FlexibleInstances@ , @FlexibleContexts@ , and @UndecidableInstances@ , 
 @GADTs@. Besides , GCH 7 is required . 

 > import Data . Comp . Multi 
 > import Data . Comp . Multi . Show ( ) 
 > import Data . Comp . Multi . Derive 
 > 
 > data Value e l where 
 >    Const   : :         Int - > Value e Int 
 >    Pair    : : e s - > e t - > Value e ( s , t ) 
 > data Op e l where 
 >    Add , Mult   : : e Int - > e Int    - > Op e Int 
 >    Fst         : :           e ( s , t ) - > Op e s 
 >    Snd         : :           e ( s , t ) - > Op e t 
 > data Sugar e l where 
 >    Neg    : : e Int    - > Sugar e Int 
 >    Swap   : : e ( s , t ) - > Sugar e ( t , s ) 
 > 
 > data Pos = Pos Int Int 
 >             deriving ( Show , Eq ) 
 > 
 > type Sig = Op : + : Value 
 > type SigP = Op : & : Pos : + : Value : & : Pos 
 > 
 > type Sig ' = Sugar : + : Op : + : Value 
 > type SigP ' = Sugar : & : Pos : + : Op : & : Pos : + : Value : & : Pos 
 > 
 > $ ( derive [ makeHFunctor , makeHTraversable , makeHFoldable , 
 >             , makeHShowF , smartConstructors ] 
 >           [ '' Value , '' Op , '' Sugar ] ) 
 > 
 > class ( HFunctor f ,   ) = >  f g where 
 >    desugHom : :    
 >    desugHom = desugHom ' .   
 >    desugHom ' : : Alg f ( Context g a ) 
 >    desugHom ' x = appCxt ( desugHom x ) 
 > 
 > instance (  f h ,   h ) = >  ( f : + : g ) h where 
 >    desugHom (   ) = desugHom x 
 >    desugHom ( Inr x ) = desugHom x 
 >    desugHom ' (   ) = desugHom ' x 
 >    desugHom ' ( Inr x ) = desugHom ' x 
 > 
 > instance ( Value : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , HFunctor v ) = >   v where 
 >    desugHom = simpCxt . inj 
 > 
 > instance ( Op : < : v , Value : < : v , HFunctor v ) = >   v where 
 >    desugHom ' (   )   = iConst ( -1 ) ` iMult ` x 
 >    desugHom ' ( Swap x ) = iSnd x ` iPair ` iFst x 
 > 
 > desug : : Term Sig ' :-> Term Sig 
 > desug = appHom desugHom 
 > 
 > desugEx : : Term Sig ( Int , Int ) 
 > desugEx = desug $ iSwap $ iPair ( iConst 1 ) ( iConst 2 ) 
 > 
 > desugP : : Term SigP ' :-> Term SigP 
 > desugP = appHom (   ) 
 > 
 > iSwapP : : ( DistAnn f p f ' , Sugar : < : f ) = > p - > Term f ' ( a , b ) - > Term f ' ( b , a ) 
 > iSwapP p x = Term ( injectA p $ inj $ Swap x ) 
 > 
 > iConstP : : ( DistAnn f p f ' , Value : < : f ) = > p - > Int - > Term f ' Int 
 > iConstP p x = Term ( injectA p $ inj $ Const x ) 
 > 
 > iPairP : : ( DistAnn f p f ' , Value : < : f ) = > p - > Term f ' a - > Term f ' b - > Term f ' ( a , b ) 
 > iPairP p x y = Term ( injectA p $ inj $ Pair x y ) 
 > 
 > iFstP : : ( DistAnn f p f ' , Op : < : f ) = > p - > Term f ' ( a , b ) - > Term f ' a 
 > iFstP p x = Term ( injectA p $ inj $ Fst x ) 
 > 
 > iSndP : : ( DistAnn f p f ' , Op : < : f ) = > p - > Term f ' ( a , b ) - > Term f ' b 
 >      ( injectA p $ inj $ Snd x ) 
 > 
 > desugPEx : : Term SigP ( Int , Int ) 
 >  = desugP $ iSwapP ( Pos 1 0 ) ( iPairP ( Pos 1 1 ) ( iConstP ( Pos 1 2 ) 1 ) 
 >                                                         ( iConstP ( Pos 1 3 ) 2 ) ) 

The example illustrates how to lift a term homomorphism to annotations,
exemplified via a desugaring term homomorphism lifted to terms annotated with
source position information.

The following language extensions are needed in order to run the example:
@TemplateHaskell@, @TypeOperators@, @MultiParamTypeClasses@,
@FlexibleInstances@, @FlexibleContexts@, and @UndecidableInstances@,
@GADTs@. Besides, GCH 7 is required.

> import Data.Comp.Multi
> import Data.Comp.Multi.Show ()
> import Data.Comp.Multi.Derive
>
> data Value e l where
>   Const  ::        Int -> Value e Int
>   Pair   :: e s -> e t -> Value e (s,t)
> data Op e l where
>   Add, Mult  :: e Int -> e Int   -> Op e Int
>   Fst        ::          e (s,t) -> Op e s
>   Snd        ::          e (s,t) -> Op e t
> data Sugar e l where
>   Neg   :: e Int   -> Sugar e Int
>   Swap  :: e (s,t) -> Sugar e (t,s)
>
> data Pos = Pos Int Int
>            deriving (Show, Eq)
>
> type Sig = Op :+: Value
> type SigP = Op :&: Pos :+: Value :&: Pos
>
> type Sig' = Sugar :+: Op :+: Value
> type SigP' = Sugar :&: Pos :+: Op :&: Pos :+: Value :&: Pos
>
> $(derive [makeHFunctor, makeHTraversable, makeHFoldable,
>           makeHEqF, makeHShowF, smartConstructors]
>          [''Value, ''Op, ''Sugar])
>
> class (HFunctor f, HFunctor g) => Desugar f g where
>   desugHom :: Hom f g
>   desugHom = desugHom' . hfmap Hole
>   desugHom' :: Alg f (Context g a)
>   desugHom' x = appCxt (desugHom x)
>
> instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
>   desugHom (Inl x) = desugHom x
>   desugHom (Inr x) = desugHom x
>   desugHom' (Inl x) = desugHom' x
>   desugHom' (Inr x) = desugHom' x
>
> instance (Value :<: v, HFunctor v) => Desugar Value v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, HFunctor v) => Desugar Op v where
>   desugHom = simpCxt . inj
>
> instance (Op :<: v, Value :<: v, HFunctor v) => Desugar Sugar v where
>   desugHom' (Neg x)  = iConst (-1) `iMult` x
>   desugHom' (Swap x) = iSnd x `iPair` iFst x
>
> desug :: Term Sig' :-> Term Sig
> desug = appHom desugHom
>
> desugEx :: Term Sig (Int,Int)
> desugEx = desug $ iSwap $ iPair (iConst 1) (iConst 2)
>
> desugP :: Term SigP' :-> Term SigP
> desugP = appHom (propAnn desugHom)
>
> iSwapP :: (DistAnn f p f', Sugar :<: f) => p -> Term f' (a,b) -> Term f' (b,a)
> iSwapP p x = Term (injectA p $ inj $ Swap x)
>
> iConstP :: (DistAnn f p f', Value :<: f) => p -> Int -> Term f' Int
> iConstP p x = Term (injectA p $ inj $ Const x)
>
> iPairP :: (DistAnn f p f', Value :<: f) => p -> Term f' a -> Term f' b -> Term f' (a,b)
> iPairP p x y = Term (injectA p $ inj $ Pair x y)
>
> iFstP :: (DistAnn f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' a
> iFstP p x = Term (injectA p $ inj $ Fst x)
>
> iSndP :: (DistAnn f p f', Op :<: f) => p -> Term f' (a,b) -> Term f' b
> iSndP p x = Term (injectA p $ inj $ Snd x)
>
> desugPEx :: Term SigP (Int,Int)
> desugPEx = desugP $ iSwapP (Pos 1 0) (iPairP (Pos 1 1) (iConstP (Pos 1 2) 1)
>                                                        (iConstP (Pos 1 3) 2))
-}
