Commits

Patrick Bahr committed 895599a

removed the parametric higher-order variants; cleaned up the tests and benchmarks

  • Participants
  • Parent commits b23e638
  • Branches closed_type_families

Comments (0)

Files changed (72)

File benchmark-macro/DataTypes/Mono.hs

-{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable, TemplateHaskell, FlexibleContexts #-}
+{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable, TemplateHaskell,
+  FlexibleContexts, ConstraintKinds #-}
 
 module DataTypes.Mono where
 
 
 exprAE :: Int -> Term ArithExc
 exprAE 0 = iVal' 3
-exprAE n = iVal' 1 `iAdd'` iCatch (exprAE (n-1) `iAdd'` iThrow) (iVal' 2 `iAdd'` exprAE (n-1))
+exprAE n = iVal' 1 `iAdd'` iCatch (exprAE (n-1) `iAdd'` iThrow) (iVal' 2 `iAdd'` exprAE (n-1))

File benchmark/Benchmark.hs

 import Control.DeepSeq
 import Test.QuickCheck.Arbitrary
 import Test.QuickCheck.Gen
+import Test.QuickCheck.Random
 import System.Random
 
 aExpr :: SugarExpr
 
 randStdBenchmarks :: Int -> IO Benchmark
 randStdBenchmarks s = do
-  rand <- newStdGen
+  rand <- newQCGen
   let ty = unGen arbitrary rand s
   putStr "size of the type term: "
   print $ size ty

File benchmark/DataTypes/Comp.hs

   TypeOperators,
   ScopedTypeVariables,
   TypeSynonymInstances,
-  DeriveFunctor#-}
+  DeriveFunctor,
+  ConstraintKinds #-}
 
 module DataTypes.Comp 
     ( module DataTypes.Comp,
         where run TInt n = return [(5*n,Neg iTInt),(5*n,Minus iTInt iTInt)]
               run TBool n = return [(5*n,Gt iTInt iTInt),(5*n,Or iTBool iTBool),
                                  (5*n,Impl iTBool iTBool)]
-              run TPair{} _ = return []
+              run TPair{} _ = return []

File benchmark/Functions/Comp/Desugar.hs

   UndecidableInstances,
   TypeOperators,
   ScopedTypeVariables,
-  TypeSynonymInstances #-}
+  TypeSynonymInstances,
+  ConstraintKinds #-}
 
 module Functions.Comp.Desugar where
 

File benchmark/Functions/Comp/Eval.hs

   UndecidableInstances,
   TypeOperators,
   ScopedTypeVariables,
-  TypeSynonymInstances #-}
+  TypeSynonymInstances,
+  ConstraintKinds #-}
 
 module Functions.Comp.Eval where
 
 import Functions.Comp.Desugar
 import Data.Comp
 import Data.Comp.Ops
-import Data.Comp.Thunk
+import Data.Comp.Thunk hiding (eval, eval2)
 import Data.Comp.Derive
 import Control.Monad
 import Data.Traversable
 $(derive [liftSum] [''EvalT])
 
 instance (Monad m, Traversable v, Value :<: v) => EvalT Value v m where
-    evalTAlg = inject
+    evalTAlg = injectT
 
-instance (Value :<: v, Traversable v, EqF v, Monad m) => EvalT Op v m where
+instance (Value :<: (m :+: v), Value :<: v, Traversable v, EqF v, Monad m) => EvalT Op v m where
     evalTAlg (Plus x y) = thunk $ do
                            VInt i <- whnfPr x
                            VInt j <- whnfPr y
                               ProjLeft -> x
                               ProjRight -> y
 
-instance (Value :<: v, Traversable v, Monad m) => EvalT Sugar v m where
+instance (Value :<: (m :+: v), Value :<: v, Traversable v, Monad m) => EvalT Sugar v m where
     evalTAlg (Neg x) = thunk $ do
                          VInt i <- whnfPr x
                          return $ iVInt (-i)

File benchmark/Functions/Comp/FreeVars.hs

   UndecidableInstances,
   TypeOperators,
   ScopedTypeVariables,
-  TypeSynonymInstances #-}
+  TypeSynonymInstances,
+  ConstraintKinds #-}
 
 module Functions.Comp.FreeVars where
 
 
 
 freeVarsGen :: SugarExpr -> [Int]
-freeVarsGen e =  [ j | VInt j <- subterms' e]
+freeVarsGen e =  [ j | VInt j <- subterms' e]

File benchmark/Functions/Comp/HOAS.hs

     varsAlg = foldr (+) 0
 
 vars :: (ExpFunctor f, Vars f) => Term f -> Int
-vars = cataE varsAlg
+vars = cataE varsAlg

File benchmark/Functions/Comp/Inference.hs

   UndecidableInstances,
   TypeOperators,
   ScopedTypeVariables,
-  TypeSynonymInstances #-}
+  TypeSynonymInstances,
+  ConstraintKinds#-}
 
 module Functions.Comp.Inference where
 
 desugTypeAlg2 = inferTypeAlg2  `compAlg` (desugAlg :: Hom SugarSig ExprSig)
 
 desugType2' :: SugarExpr -> BaseType
-desugType2' e = cata desugTypeAlg2 e
+desugType2' e = cata desugTypeAlg2 e

File compdata.cabal

 Name:			compdata
-Version:		0.7.0.1
+Version:		0.8
 Synopsis:            	Compositional Data Types
 Description:
 
      to families of mutually recursive data types and (more generally) GADTs.
      This extension resides in the module "Data.Comp.Multi".
   .
-  * /Parametric compositional data types/ (Workshop on Mathematically
-     Structured Functional Programming, 3-24, 2012,
-     <http://dx.doi.org/10.4204/EPTCS.76.3>). All of the above is also
-     lifted to parametric data types, which enables support for
-     parametric higher-order abstract syntax (PHOAS). This extension
-     resides in the module "Data.Comp.Param".
-  .
-  *  /Generalised parametric compositional data types/. All of the above is also
-     lifted to generalised parametric data types, which enables support for
-     typed parametric higher-order abstract syntax (PHOAS). This extension
-     resides in the module "Data.Comp.MultiParam".
-  .
   * Advanced recursion schemes derived from tree automata. These
     recursion schemes allow for a higher degree of modularity and make
     it possible to apply fusion. See /Modular Tree Automata/
     2013, <http://dx.doi.org/10.1145/2502488.2502489>).
   .
 
-  Examples of using (generalised) (parametric) compositional data types are
-  bundled with the package in the libray @examples@.
+  Examples of using (generalised) compositional data types are bundled
+  with the package in the folder @examples@.
 
 Category:            	Generics
 License:		BSD3
 
 extra-source-files:
   -- test files
-  testsuite/tests/Data_Test.hs,
-  testsuite/tests/Data/Comp_Test.hs,
-  testsuite/tests/Data/Comp/Equality_Test.hs,
-  testsuite/tests/Data/Comp/Variables_Test.hs,
-  testsuite/tests/Data/Comp/Multi_Test.hs,
-  testsuite/tests/Data/Comp/Multi/Variables_Test.hs,
-  testsuite/tests/Data/Comp/Examples_Test.hs,
-  testsuite/tests/Data/Comp/Examples/Comp.hs,
-  testsuite/tests/Data/Comp/Examples/Multi.hs,
-  testsuite/tests/Data/Comp/Examples/Param.hs,
-  testsuite/tests/Data/Comp/Examples/MultiParam.hs,
+  testsuite/tests/*.hs
+  testsuite/tests/Data/*.hs
+  testsuite/tests/Data/Comp/*.hs
+  testsuite/tests/Data/Comp/Multi/*.hs
+  testsuite/tests/Data/Comp/Examples/*.hs
   testsuite/tests/Test/Utils.hs
   -- benchmark files
-  benchmark/Test.hs
-  benchmark/Benchmark.hs
-  benchmark/DataTypes.hs
-  benchmark/Functions.hs
-  benchmark/DataTypes/Comp.hs
-  benchmark/DataTypes/Transform.hs
-  benchmark/DataTypes/Standard.hs
-  benchmark/Multi/DataTypes/Comp.hs
-  benchmark/Multi/Functions/Comp/Eval.hs
-  benchmark/Multi/Functions/Comp/Desugar.hs
-  benchmark/Transformations.hs
-  benchmark/Functions/Comp.hs
-  benchmark/Functions/Comp/Eval.hs
-  benchmark/Functions/Comp/Desugar.hs
-  benchmark/Functions/Comp/FreeVars.hs
-  benchmark/Functions/Comp/Inference.hs
-  benchmark/Functions/Standard/Eval.hs
-  benchmark/Functions/Standard/Desugar.hs
-  benchmark/Functions/Standard/FreeVars.hs
-  benchmark/Functions/Standard/Inference.hs
-  benchmark/Functions/Standard.hs
+  benchmark/*.hs
+  benchmark/DataTypes/*.hs
+  benchmark/Functions/*.hs
+  benchmark/Functions/Comp/*.hs
+  benchmark/Functions/Standard/*.hs
+  benchmark/Multi/DataTypes/*.hs
+  benchmark/Multi/Functions/Comp/*.hs
   -- example files
-  examples/Examples/Common.hs
-  examples/Examples/Eval.hs
-  examples/Examples/EvalM.hs
-  examples/Examples/Desugar.hs
-  examples/Examples/Automata/Compiler.hs,
-  examples/Examples/Multi/Common.hs
-  examples/Examples/Multi/Eval.hs
-  examples/Examples/Multi/EvalI.hs
-  examples/Examples/Multi/EvalM.hs
-  examples/Examples/Multi/Desugar.hs
-  examples/Examples/Param/Lambda.hs
-  examples/Examples/Param/Names.hs
-  examples/Examples/Param/Graph.hs
-  examples/Examples/MultiParam/Lambda.hs
-  examples/Examples/MultiParam/FOL.hs
+  examples/Examples/*.hs
+  examples/Examples/Automata/*.hs
+  examples/Examples/Multi/*.hs
 
 library
-  Exposed-Modules:      Data.Comp,
-                        Data.Comp.Annotation,
-                        Data.Comp.Sum,
-                        Data.Comp.Term,
-                        Data.Comp.Algebra,
-                        Data.Comp.Equality,
-                        Data.Comp.Ordering,
-                        Data.Comp.DeepSeq,
+  Exposed-Modules:      Data.Comp
+                        Data.Comp.Annotation
+                        Data.Comp.Sum
+                        Data.Comp.Term
+                        Data.Comp.Algebra
+                        Data.Comp.Equality
+                        Data.Comp.Ordering
+                        Data.Comp.DeepSeq
                         Data.Comp.Generic
-                        Data.Comp.TermRewriting,
-                        Data.Comp.Arbitrary,
-                        Data.Comp.Show,
-                        Data.Comp.Render,
-                        Data.Comp.Variables,
-                        Data.Comp.Decompose,
-                        Data.Comp.Unification,
-                        Data.Comp.Derive,
-                        Data.Comp.Matching,
-                        Data.Comp.Desugar,
-                        Data.Comp.Automata,
-                        Data.Comp.MacroAutomata,
-                        Data.Comp.Automata.Product,
-                        Data.Comp.Number,
-                        Data.Comp.Thunk,
-                        Data.Comp.Ops,
+                        Data.Comp.TermRewriting
+                        Data.Comp.Arbitrary
+                        Data.Comp.Show
+                        Data.Comp.Render
+                        Data.Comp.Variables
+                        Data.Comp.Decompose
+                        Data.Comp.Unification
+                        Data.Comp.Derive
+                        Data.Comp.Derive.Utils
+                        Data.Comp.Matching
+                        Data.Comp.Desugar
+                        Data.Comp.Automata
+                        Data.Comp.MacroAutomata
+                        Data.Comp.Automata.Product
+                        Data.Comp.Number
+                        Data.Comp.Thunk
+                        Data.Comp.Ops
 
-                        Data.Comp.Multi,
-                        Data.Comp.Multi.Term,
-                        Data.Comp.Multi.Sum,
-                        Data.Comp.Multi.HFunctor,
-                        Data.Comp.Multi.HFoldable,
-                        Data.Comp.Multi.HTraversable,
-                        Data.Comp.Multi.Algebra,
-                        Data.Comp.Multi.Annotation,
-                        Data.Comp.Multi.Show,
-                        Data.Comp.Multi.Equality,
-                        Data.Comp.Multi.Ordering,
-                        Data.Comp.Multi.Variables,
-                        Data.Comp.Multi.Ops,
-                        Data.Comp.Multi.Number,
+                        Data.Comp.Multi
+                        Data.Comp.Multi.Term
+                        Data.Comp.Multi.Sum
+                        Data.Comp.Multi.HFunctor
+                        Data.Comp.Multi.HFoldable
+                        Data.Comp.Multi.HTraversable
+                        Data.Comp.Multi.Algebra
+                        Data.Comp.Multi.Annotation
+                        Data.Comp.Multi.Show
+                        Data.Comp.Multi.Equality
+                        Data.Comp.Multi.Ordering
+                        Data.Comp.Multi.Variables
+                        Data.Comp.Multi.Ops
+                        Data.Comp.Multi.Number
                         Data.Comp.Multi.Derive
-                        Data.Comp.Multi.Generic,
-                        Data.Comp.Multi.Desugar,
+                        Data.Comp.Multi.Generic
+                        Data.Comp.Multi.Desugar
 
-                        Data.Comp.Param,
-                        Data.Comp.Param.Term,
-                        Data.Comp.Param.FreshM,
-                        Data.Comp.Param.Sum,
-                        Data.Comp.Param.Difunctor,
-                        Data.Comp.Param.Ditraversable,
-                        Data.Comp.Param.Algebra,
-                        Data.Comp.Param.Annotation,
-                        Data.Comp.Param.Ops
-                        Data.Comp.Param.Equality
-                        Data.Comp.Param.Ordering
-                        Data.Comp.Param.Show
-                        Data.Comp.Param.Derive,
-                        Data.Comp.Param.Desugar
-                        Data.Comp.Param.Thunk
+  Other-Modules:        Data.Comp.Derive.Equality
+                        Data.Comp.Derive.Ordering
+                        Data.Comp.Derive.Arbitrary
+                        Data.Comp.Derive.Show
+                        Data.Comp.Derive.DeepSeq
+                        Data.Comp.Derive.SmartConstructors
+                        Data.Comp.Derive.SmartAConstructors
+                        Data.Comp.Derive.Foldable
+                        Data.Comp.Derive.Traversable
+                        Data.Comp.Derive.Projections
+                        Data.Comp.Derive.HaskellStrict
+                        Data.Comp.Automata.Product.Derive
 
-                        Data.Comp.MultiParam,
-                        Data.Comp.MultiParam.Term,
-                        Data.Comp.MultiParam.FreshM,
-                        Data.Comp.MultiParam.Sum,
-                        Data.Comp.MultiParam.HDifunctor,
-                        Data.Comp.MultiParam.HDitraversable,
-                        Data.Comp.MultiParam.Algebra,
-                        Data.Comp.MultiParam.Annotation,
-                        Data.Comp.MultiParam.Ops
-                        Data.Comp.MultiParam.Equality
-                        Data.Comp.MultiParam.Ordering
-                        Data.Comp.MultiParam.Show
-                        Data.Comp.MultiParam.Derive,
-                        Data.Comp.MultiParam.Desugar
-
-  Other-Modules:        Data.Comp.Derive.Utils,
-                        Data.Comp.Derive.Equality,
-                        Data.Comp.Derive.Ordering,
-                        Data.Comp.Derive.Arbitrary,
-                        Data.Comp.Derive.Show,
-                        Data.Comp.Derive.DeepSeq,
-                        Data.Comp.Derive.SmartConstructors,
-                        Data.Comp.Derive.SmartAConstructors,
-                        Data.Comp.Derive.Foldable,
-                        Data.Comp.Derive.Traversable,
-                        Data.Comp.Derive.Projections,
-                        Data.Comp.Derive.HaskellStrict,
-                        Data.Comp.Automata.Product.Derive,
-
-                        Data.Comp.Multi.Derive.HFunctor,
-                        Data.Comp.Multi.Derive.HFoldable,
-                        Data.Comp.Multi.Derive.HTraversable,
-                        Data.Comp.Multi.Derive.Equality,
-                        Data.Comp.Multi.Derive.Ordering,
-                        Data.Comp.Multi.Derive.Show,
+                        Data.Comp.Multi.Derive.HFunctor
+                        Data.Comp.Multi.Derive.HFoldable
+                        Data.Comp.Multi.Derive.HTraversable
+                        Data.Comp.Multi.Derive.Equality
+                        Data.Comp.Multi.Derive.Ordering
+                        Data.Comp.Multi.Derive.Show
                         Data.Comp.Multi.Derive.SmartConstructors
                         Data.Comp.Multi.Derive.SmartAConstructors
-                        Data.Comp.Multi.Derive.Injections,
-                        Data.Comp.Multi.Derive.Projections,
+                        Data.Comp.Multi.Derive.Injections
+                        Data.Comp.Multi.Derive.Projections
 
-                        Data.Comp.Param.Derive.Difunctor,
-                        Data.Comp.Param.Derive.Ditraversable,
-                        Data.Comp.Param.Derive.Equality,
-                        Data.Comp.Param.Derive.Ordering,
-                        Data.Comp.Param.Derive.Show,
-                        Data.Comp.Param.Derive.SmartConstructors,
-                        Data.Comp.Param.Derive.SmartAConstructors,
-                        Data.Comp.Param.Derive.Injections,
-                        Data.Comp.Param.Derive.Projections,
-
-                        Data.Comp.MultiParam.Derive.HDifunctor,
-                        Data.Comp.MultiParam.Derive.Equality,
-                        Data.Comp.MultiParam.Derive.Ordering,
-                        Data.Comp.MultiParam.Derive.Show,
-                        Data.Comp.MultiParam.Derive.SmartConstructors,
-                        Data.Comp.MultiParam.Derive.SmartAConstructors,
-                        Data.Comp.MultiParam.Derive.Injections,
-                        Data.Comp.MultiParam.Derive.Projections
-
-  Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, th-expand-syns, transformers, tree-view
+  Build-Depends:	base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive,
+                        deepseq, th-expand-syns, transformers, tree-view
   hs-source-dirs:	src
   ghc-options:          -W
 
 Test-Suite test
   Type:                 exitcode-stdio-1.0
   Main-is:		Data_Test.hs
-  hs-source-dirs:	src testsuite/tests examples
-  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive, th-expand-syns, deepseq, transformers
+  hs-source-dirs:	testsuite/tests examples
+  Build-Depends:        compdata, base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, 
+                        HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive,
+                        th-expand-syns, deepseq, transformers
 
 Benchmark algebra
   Type:                 exitcode-stdio-1.0
   ghc-options:          -W -O2
   -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.
   cpp-options:          -DNO_RULES
-  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers
+  Build-Depends:        base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, 
+                        deepseq, criterion, random, uniplate, th-expand-syns, transformers
 
 
 source-repository head

File examples/Examples/Desugar.hs

 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
   FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances #-}
+  OverlappingInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Desugar
 --                                                     (iAConst (Pos 1 3) 2)))
 desugPEx :: Term SigP
 desugPEx = desugP $ iASwap (Pos 1 0) (iAPair (Pos 1 1) (iAConst (Pos 1 2) 1)
-                                                       (iAConst (Pos 1 3) 2))
+                                                       (iAConst (Pos 1 3) 2))

File examples/Examples/Eval.hs

 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
   FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances #-}
+  OverlappingInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.Eval
 
 -- Example: evalEx = iConst 5
 evalEx :: Term Value
-evalEx = eval (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)
+evalEx = eval (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)

File examples/Examples/EvalM.hs

 {-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
   FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances #-}
+  OverlappingInstances, ConstraintKinds #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Examples.EvalM
 
 -- Example: evalMEx = Just (iConst 5)
 evalMEx :: Maybe (Term Value)
-evalMEx = evalM (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)
+evalMEx = evalM (iConst 1 `iAdd` (iConst 2 `iMult` iConst 2) :: Term Sig)

File examples/Examples/MultiParam/FOL.hs

-{-# LANGUAGE TemplateHaskell, TypeOperators, FlexibleInstances,
-  FlexibleContexts, UndecidableInstances, GADTs, KindSignatures,
-  OverlappingInstances, TypeSynonymInstances, EmptyDataDecls #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.MultiParam.FOL
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- First-Order Logic a la Carte
---
--- This example illustrates how to implement First-Order Logic a la Carte
--- (Knowles, The Monad.Reader Issue 11, '08) using Generalised Parametric
--- Compositional Data Types.
---
--- Rather than using a fixed domain 'Term' for binders as Knowles, our encoding
--- uses a mutually recursive data structure for terms and formulae. This makes
--- terms modular too, and hence we only introduce variables when they are
--- actually needed in stage 5.
---
---------------------------------------------------------------------------------
-
-module Examples.MultiParam.FOL where
-
-import Data.Comp.MultiParam hiding (Var)
-import qualified Data.Comp.MultiParam as MP
-import Data.Comp.MultiParam.Show ()
-import Data.Comp.MultiParam.Derive
-import Data.Comp.MultiParam.FreshM (Name, withName, evalFreshM)
-import Data.List (intercalate)
-import Data.Maybe
-import Control.Monad.State
-import Control.Monad.Reader
-
--- Phantom types indicating whether a (recursive) term is a formula or a term
-data TFormula
-data TTerm
-
--- Terms
-data Const :: (* -> *) -> (* -> *) -> * -> * where
-    Const :: String -> [e TTerm] -> Const a e TTerm
-data Var :: (* -> *) -> (* -> *) -> * -> * where
-    Var :: String -> Var a e TTerm
-
--- Formulae
-data TT :: (* -> *) -> (* -> *) -> * -> * where
-    TT :: TT a e TFormula
-data FF :: (* -> *) -> (* -> *) -> * -> * where
-    FF :: FF a e TFormula
-data Atom :: (* -> *) -> (* -> *) -> * -> * where
-    Atom :: String -> [e TTerm] -> Atom a e TFormula
-data NAtom :: (* -> *) -> (* -> *) -> * -> * where
-    NAtom :: String -> [e TTerm] -> NAtom a e TFormula
-data Not :: (* -> *) -> (* -> *) -> * -> * where
-    Not :: e TFormula -> Not a e TFormula
-data Or :: (* -> *) -> (* -> *) -> * -> * where
-    Or :: e TFormula -> e TFormula -> Or a e TFormula
-data And :: (* -> *) -> (* -> *) -> * -> * where
-    And :: e TFormula -> e TFormula -> And a e TFormula
-data Impl :: (* -> *) -> (* -> *) -> * -> * where
-    Impl :: e TFormula -> e TFormula -> Impl a e TFormula
-data Exists :: (* -> *) -> (* -> *) -> * -> * where
-    Exists :: (a TTerm -> e TFormula) -> Exists a e TFormula
-data Forall :: (* -> *) -> (* -> *) -> * -> * where
-    Forall :: (a TTerm -> e TFormula) -> Forall a e TFormula
-
-$(derive [makeHDifunctor, smartConstructors]
-         [''Const, ''Var, ''TT, ''FF, ''Atom, ''NAtom,
-          ''Not, ''Or, ''And, ''Impl, ''Exists, ''Forall])
-
---------------------------------------------------------------------------------
--- (Custom) pretty printing of terms and formulae
---------------------------------------------------------------------------------
-
-instance ShowHD Const where
-  showHD (Const f t) = do ts <- mapM unK t
-                          return $ f ++ "(" ++ intercalate ", " ts ++ ")"
-
-instance ShowHD Var where
-  showHD (Var x) = return x
-
-instance ShowHD TT where
-  showHD TT = return "true"
-
-instance ShowHD FF where
-  showHD FF = return "false"
-
-instance ShowHD Atom where
-  showHD (Atom p t) = do ts <- mapM unK t
-                         return $ p ++ "(" ++ intercalate ", " ts ++ ")"
-
-instance ShowHD NAtom where
-  showHD (NAtom p t) = do ts <- mapM unK t
-                          return $ "not " ++ p ++ "(" ++ intercalate ", " ts ++ ")"
-
-instance ShowHD Not where
-  showHD (Not (K f)) = liftM (\x -> "not (" ++ x ++ ")") f
-
-instance ShowHD Or where
-  showHD (Or (K f1) (K f2)) =
-      liftM2 (\x y -> "(" ++ x ++ ") or (" ++ y ++ ")") f1 f2
-
-instance ShowHD And where
-  showHD (And (K f1) (K f2)) =
-      liftM2 (\x y -> "(" ++ x ++ ") and (" ++ y ++ ")") f1 f2
-
-instance ShowHD Impl where
-  showHD (Impl (K f1) (K f2)) =
-      liftM2 (\x y -> "(" ++ x ++ ") -> (" ++ y ++ ")") f1 f2
-
-instance ShowHD Exists where
-  showHD (Exists f) =
-      withName (\x -> do b <- unK (f x)
-                         return $ "exists " ++ show x ++ ". " ++ b)
-
-instance ShowHD Forall where
-  showHD (Forall f) =
-      withName (\x -> do b <- unK (f x)
-                         return $ "forall " ++ show x ++ ". " ++ b)
-
---------------------------------------------------------------------------------
--- Stage 0
---------------------------------------------------------------------------------
-
-type Input = Const :+:
-             TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Impl :+:
-             Exists :+: Forall
-
-foodFact :: Term Input TFormula
-foodFact = Term $
-  iExists (\p -> iAtom "Person" [p] `iAnd`
-                 iForall (\f -> iAtom "Food" [f] `iImpl`
-                                iAtom "Eats" [p,f])) `iImpl`
-  iNot (iExists $ \f -> iAtom "Food" [f] `iAnd`
-                        iNot (iExists $ \p -> iAtom "Person" [p] `iAnd`
-                                              iAtom "Eats" [p,f]))
-
---------------------------------------------------------------------------------
--- Stage 1: Eliminate Implications
---------------------------------------------------------------------------------
-
-type Stage1 = Const :+:
-              TT :+: FF :+: Atom :+: Not :+: Or :+: And :+: Exists :+: Forall
-
-class HDifunctor f => ElimImp f where
-  elimImpHom :: Hom f Stage1
-
-$(derive [liftSum] [''ElimImp])
-
-elimImp :: Term Input :-> Term Stage1
-elimImp (Term t) = Term (appHom elimImpHom t)
-
-instance (HDifunctor f, f :<: Stage1) => ElimImp f where
-  elimImpHom = simpCxt . inj
-
-instance ElimImp Impl where
-  elimImpHom (Impl f1 f2) = iNot (Hole f1) `iOr` (Hole f2)
-
-foodFact1 :: Term Stage1 TFormula
-foodFact1 = elimImp foodFact
-
---------------------------------------------------------------------------------
--- Stage 2: Move Negation Inwards
---------------------------------------------------------------------------------
-
-type Stage2 = Const :+:
-              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Exists :+: Forall
-
-class HDifunctor f => Dualize f where
-  dualizeHom :: f a (Cxt h Stage2 a b) :-> Cxt h Stage2 a b
-
-$(derive [liftSum] [''Dualize])
-
-dualize :: Trm Stage2 a :-> Trm Stage2 a
-dualize = appHom (dualizeHom . hfmap Hole)
-
-instance Dualize Const where
-  dualizeHom (Const f t) = iConst f t
-
-instance Dualize TT where
-  dualizeHom TT = iFF
-
-instance Dualize FF where
-  dualizeHom FF = iTT
-
-instance Dualize Atom where
-  dualizeHom (Atom p t) = iNAtom p t
-
-instance Dualize NAtom where
-  dualizeHom (NAtom p t) = iAtom p t
-
-instance Dualize Or where
-  dualizeHom (Or f1 f2) = f1 `iAnd` f2
-
-instance Dualize And where
-  dualizeHom (And f1 f2) = f1 `iOr` f2
-
-instance Dualize Exists where
-  dualizeHom (Exists f) = inject $ Forall f
-
-instance Dualize Forall where
-  dualizeHom (Forall f) = inject $ Exists f
-
-class PushNot f where
-  pushNotAlg :: Alg f (Trm Stage2 a)
-
-$(derive [liftSum] [''PushNot])
-
-pushNotInwards :: Term Stage1 :-> Term Stage2
-pushNotInwards t = Term (cata pushNotAlg t)
-
-instance (HDifunctor f, f :<: Stage2) => PushNot f where
-  pushNotAlg = inject . hdimap MP.Var id -- default
-
-instance PushNot Not where
-  pushNotAlg (Not f) = dualize f
-
-foodFact2 :: Term Stage2 TFormula
-foodFact2 = pushNotInwards foodFact1
-
---------------------------------------------------------------------------------
--- Stage 4: Skolemization
---------------------------------------------------------------------------------
-
-type Stage4 = Const :+:
-              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And :+: Forall
-
-type Unique = Int
-data UniqueSupply = UniqueSupply Unique UniqueSupply UniqueSupply
-
-initialUniqueSupply :: UniqueSupply
-initialUniqueSupply = genSupply 1
-    where genSupply n = UniqueSupply n (genSupply (2 * n))
-                                       (genSupply (2 * n + 1))
-
-splitUniqueSupply :: UniqueSupply -> (UniqueSupply, UniqueSupply)
-splitUniqueSupply (UniqueSupply	_ l r) = (l,r)
-
-getUnique :: UniqueSupply -> (Unique, UniqueSupply)
-getUnique (UniqueSupply n l _) = (n,l)
-
-type Supply = State UniqueSupply
-type S a = ReaderT [Trm Stage4 a TTerm] Supply
-
-evalS :: S a b -> [Trm Stage4 a TTerm] -> UniqueSupply -> b
-evalS m env = evalState (runReaderT m env)
-
-fresh :: S a Int
-fresh = do supply <- get
-           let (uniq,rest) = getUnique supply
-           put rest
-           return uniq
-
-freshes :: S a UniqueSupply
-freshes = do supply <- get
-             let (l,r) = splitUniqueSupply supply
-             put r
-             return l
-
-class Skolem f where
-  skolemAlg :: AlgM' (S a) f (Trm Stage4 a)
-
-$(derive [liftSum] [''Skolem])
-
-skolemize :: Term Stage2 :-> Term Stage4
-skolemize f = Term (evalState (runReaderT (cataM' skolemAlg f) [])
-                              initialUniqueSupply)
-
-instance Skolem Const where
-  skolemAlg (Const f t) = liftM (iConst f) $ mapM getCompose t
-
-instance Skolem TT where
-  skolemAlg TT = return iTT
-
-instance Skolem FF where
-  skolemAlg FF = return iFF
-
-instance Skolem Atom where
-  skolemAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t
-
-instance Skolem NAtom where
-  skolemAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t
-
-instance Skolem Or where
-  skolemAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2
-
-instance Skolem And where
-  skolemAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2
-
-instance Skolem Forall where
-  skolemAlg (Forall f) = do
-    supply <- freshes
-    xs <- ask
-    return $ iForall $ \x -> evalS (getCompose $ f x) (x : xs) supply
-
-instance Skolem Exists where
-  skolemAlg (Exists f) = do
-    uniq <- fresh
-    xs <- ask
-    getCompose $ f (iConst ("Skol" ++ show uniq) xs)
-
-foodFact4 :: Term Stage4 TFormula
-foodFact4 = skolemize foodFact2
-
---------------------------------------------------------------------------------
--- Stage 5: Prenex Normal Form
---------------------------------------------------------------------------------
-
-type Stage5 = Const :+: Var :+:
-              TT :+: FF :+: Atom :+: NAtom :+: Or :+: And
-
-class Prenex f where
-  prenexAlg :: AlgM' (S a) f (Trm Stage5 a)
-
-$(derive [liftSum] [''Prenex])
-
-prenex :: Term Stage4 :-> Term Stage5
-prenex f = Term (evalState (runReaderT (cataM' prenexAlg f) [])
-                           initialUniqueSupply)
-
-instance Prenex Const where
-  prenexAlg (Const f t) = liftM (iConst f) $ mapM getCompose t
-
-instance Prenex TT where
-  prenexAlg TT = return iTT
-
-instance Prenex FF where
-  prenexAlg FF = return iFF
-
-instance Prenex Atom where
-  prenexAlg (Atom p t) = liftM (iAtom p) $ mapM getCompose t
-
-instance Prenex NAtom where
-  prenexAlg (NAtom p t) = liftM (iNAtom p) $ mapM getCompose t
-
-instance Prenex Or where
-  prenexAlg (Or (Compose f1) (Compose f2)) = liftM2 iOr f1 f2
-
-instance Prenex And where
-  prenexAlg (And (Compose f1) (Compose f2)) = liftM2 iAnd f1 f2
-
-instance Prenex Forall where
-  prenexAlg (Forall f) = do uniq <- fresh
-                            getCompose $ f (iVar ('x' : show uniq))
-
-foodFact5 :: Term Stage5 TFormula
-foodFact5 = prenex foodFact4
-
---------------------------------------------------------------------------------
--- Stage 6: Conjunctive Normal Form
---------------------------------------------------------------------------------
-
-type Literal a     = Trm (Const :+: Var :+: Atom :+: NAtom) a
-newtype Clause a i = Clause {unClause :: [Literal a i]} -- implicit disjunction
-newtype CNF a i    = CNF {unCNF :: [Clause a i]}        -- implicit conjunction
-
-instance (HDifunctor f, ShowHD f) => Show (Trm f Name i) where
-  show = evalFreshM . showHD . toCxt
-
-instance Show (Clause Name i) where
-  show c = intercalate " or " $ map show $ unClause c
-
-instance Show (CNF Name i) where
-  show c = intercalate "\n" $ map show $ unCNF c
-
-class ToCNF f where
-  cnfAlg :: f (CNF a) (CNF a) i -> [Clause a i]
-
-$(derive [liftSum] [''ToCNF])
-
-cnf :: Term Stage5 :-> CNF a
-cnf = cata (CNF . cnfAlg)
-
-instance ToCNF Const where
-  cnfAlg (Const f t) =
-      [Clause [iConst f (map (head . unClause . head . unCNF) t)]]
-
-instance ToCNF Var where
-  cnfAlg (Var x) = [Clause [iVar x]]
-
-instance ToCNF TT where
-  cnfAlg TT = []
-
-instance ToCNF FF where
-  cnfAlg FF = [Clause []]
-
-instance ToCNF Atom where
-  cnfAlg (Atom p t) =
-      [Clause [iAtom p (map (head . unClause . head . unCNF) t)]]
-
-instance ToCNF NAtom where
-  cnfAlg (NAtom p t) =
-      [Clause [iNAtom p (map (head . unClause . head . unCNF) t)]]
-
-instance ToCNF And where
-  cnfAlg (And f1 f2) = unCNF f1 ++ unCNF f2
-
-instance ToCNF Or where
-  cnfAlg (Or f1 f2) =
-      [Clause (x ++ y) | Clause x <- unCNF f1, Clause y <- unCNF f2]
-
-foodFact6 :: CNF a TFormula
-foodFact6 = cnf foodFact5
-
---------------------------------------------------------------------------------
--- Stage 7: Implicative Normal Form
---------------------------------------------------------------------------------
-
-type T              = Const :+: Var :+: Atom :+: NAtom
-newtype IClause a i = IClause ([Trm T a i], -- implicit conjunction
-                               [Trm T a i]) -- implicit disjunction
-newtype INF a i     = INF [IClause a i]     -- implicit conjunction
-
-instance Show (IClause Name i) where
-  show (IClause (cs,ds)) = let cs' = intercalate " and " $ map show cs
-                               ds' = intercalate " or " $ map show ds
-                           in "(" ++ cs' ++ ") -> (" ++ ds' ++ ")"
-
-instance Show (INF Name i) where
-  show (INF fs) = intercalate "\n" $ map show fs
-
-inf :: CNF a TFormula -> INF a TFormula
-inf (CNF f) = INF $ map (toImpl . unClause) f
-    where toImpl :: [Literal a TFormula] -> IClause a TFormula
-          toImpl disj = IClause ([iAtom p t | NAtom p t <- mapMaybe proj1 disj],
-                                 [inject t | t <- mapMaybe proj2 disj])
-          proj1 :: NatM Maybe (Trm T a) (NAtom a (Trm T a))
-          proj1 = project
-          proj2 :: NatM Maybe (Trm T a) (Atom a (Trm T a))
-          proj2 = project
-
-foodFact7 :: INF a TFormula
-foodFact7 = inf foodFact6

File examples/Examples/MultiParam/Lambda.hs

-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances, Rank2Types, GADTs, KindSignatures,
-  ScopedTypeVariables, TypeFamilies #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.MultiParam.Lambda
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- Tagless (monadic) interpretation of extended lambda calculus
---
---------------------------------------------------------------------------------
-
-module Examples.MultiParam.Lambda where
-
-import Data.Comp.MultiParam
-import Data.Comp.MultiParam.Show ()
-import Data.Comp.MultiParam.Equality ()
-import Data.Comp.MultiParam.Derive
-import Control.Monad (liftM2)
-import Control.Monad.Error (MonadError, throwError)
-
-data Lam :: (* -> *) -> (* -> *) -> * -> * where
-  Lam :: (a i -> b j) -> Lam a b (i -> j)
-data App :: (* -> *) -> (* -> *) -> * -> * where
-  App :: b (i -> j) -> b i -> App a b j
-data Const :: (* -> *) -> (* -> *) -> * -> * where
-  Const :: Int -> Const a b Int
-data Plus :: (* -> *) -> (* -> *) -> * -> * where
-  Plus :: b Int -> b Int -> Plus a b Int
-data Err :: (* -> *) -> (* -> *) -> * -> * where
-  Err :: Err a b i
-type Sig = Lam :+: App :+: Const :+: Plus :+: Err
-
-$(derive [smartConstructors, makeHDifunctor, makeShowHD, makeEqHD]
-         [''Lam, ''App, ''Const, ''Plus, ''Err])
-
--- * Tagless interpretation
-class Eval f where
-  evalAlg :: f I I i -> i -- I . evalAlg :: Alg f I is the actual algebra
-
-$(derive [liftSum] [''Eval])
-
-eval :: (HDifunctor f, Eval f) => Term f i -> i
-eval = unI . cata (I . evalAlg)
-
-instance Eval Lam where
-  evalAlg (Lam f) = unI . f . I
-
-instance Eval App where
-  evalAlg (App (I f) (I x)) = f x
-
-instance Eval Const where
-  evalAlg (Const n) = n
-
-instance Eval Plus where
-  evalAlg (Plus (I x) (I y)) = x + y
-
-instance Eval Err where
-  evalAlg Err = error "error"
-
--- * Tagless monadic interpretation
-type family Sem (m :: * -> *) i
-type instance Sem m (i -> j) = Sem m i -> m (Sem m j)
-type instance Sem m Int = Int
-
-newtype M m i = M {unM :: m (Sem m i)}
-
-class Monad m => EvalM m f where
-  evalMAlg :: f (M m) (M m) i -> m (Sem m i) -- M . evalMAlg :: Alg f (M m)
-
-$(derive [liftSum] [''EvalM])
-
-evalM :: (Monad m, HDifunctor f, EvalM m f) => Term f i -> m (Sem m i)
-evalM = unM . cata (M . evalMAlg)
-
-instance Monad m => EvalM m Lam where
-  evalMAlg (Lam f) = return $ unM . f . M . return
-
-instance Monad m => EvalM m App where
-  evalMAlg (App (M mf) (M mx)) = do f <- mf; f =<< mx
-  
-instance Monad m => EvalM m Const where
-  evalMAlg (Const n) = return n
-
-instance Monad m => EvalM m Plus where
-  evalMAlg (Plus (M mx) (M my)) = liftM2 (+) mx my
-
-instance MonadError String m => EvalM m Err where
-  evalMAlg Err = throwError "error" -- 'throwError' rather than 'error'
-
-e :: Term Sig Int
-e = Term ((iLam $ \x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)) `iApp` iConst 2)
-
-v :: Either String Int
-v = evalM e
-
-e' :: Term Sig (Int -> Int)
-e' = Term iErr --(iLam id)
-
-v' :: Either String (Int -> Either String Int)
-v' = evalM e'

File examples/Examples/Param/Graph.hs

-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, TemplateHaskell,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.Param.Graph
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- Graph representation. The example is taken from (Fegaras and Sheard,
--- Revisiting Catamorphisms over Datatypes with Embedded Functions, '96).
---
---------------------------------------------------------------------------------
-
-module Examples.Param.Graph where
-
-import Data.Comp.Param
-import Data.Comp.Param.Derive
-import Data.Comp.Param.Show ()
-import Data.Comp.Param.Equality ()
-
-data N p a b = N p [b] -- Node
-data R a b = R (a -> b) -- Recursion
-data S a b = S (a -> b) b -- Sharing
-
-$(derive [makeDifunctor, makeShowD, makeEqD, makeOrdD, smartConstructors]
-         [''N, ''R, ''S])
-$(derive [makeDitraversable] [''N])
-
-type Graph p = Term (N p :+: R :+: S)
-
-class FlatG f p where
-  flatGAlg :: Alg f [p]
-
-$(derive [liftSum] [''FlatG])
-
-flatG :: (Difunctor f, FlatG f p) => Term f -> [p]
-flatG = cata flatGAlg
-
-instance FlatG (N p) p where
-  flatGAlg (N p ps) = p : concat ps
-
-instance FlatG R p where
-  flatGAlg (R f) = f []
-
-instance FlatG S p where
-  flatGAlg (S f g) = f g
-
-class SumG f where
-  sumGAlg :: Alg f Int
-
-$(derive [liftSum] [''SumG])
-
-sumG :: (Difunctor f, SumG f) => Term f -> Int
-sumG = cata sumGAlg
-
-instance SumG (N Int) where
-  sumGAlg (N p ps) = p + sum ps
-
-instance SumG R where
-  sumGAlg (R f) = f 0
-
-instance SumG S where
-  sumGAlg (S f g) = f g
-
-g :: Graph Int
-g = Term $ iR (\x -> iS (\z -> iN (0 :: Int) [z,iR $ \y -> iN (1 :: Int) [y,z]])
-                        (iN (2 :: Int) [x]))
-
-f :: [Int]
-f = flatG g
-
-n :: Int
-n = sumG g

File examples/Examples/Param/Lambda.hs

-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances, Rank2Types, GADTs #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.Param.Lambda
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- Lambda calculus examples
---
--- We define a pretty printer, a desugaring transformation, constant folding,
--- and call-by-value interpreter for an extended variant of the simply typed
--- lambda calculus.
---
---------------------------------------------------------------------------------
-
-module Examples.Param.Lambda where
-
-import Data.Comp.Param
-import Data.Comp.Param.Show ()
-import Data.Comp.Param.Equality ()
-import Data.Comp.Param.Ordering ()
-import Data.Comp.Param.Derive
-import Data.Comp.Param.Desugar
-
-data Lam a b   = Lam (a -> b)
-data App a b   = App b b
-data Const a b = Const Int
-data Plus a b  = Plus b b
-data Let a b   = Let b (a -> b)
-data Err a b   = Err
-
-type Sig       = Lam :+: App :+: Const :+: Plus :+: Let :+: Err
-type Sig'      = Lam :+: App :+: Const :+: Plus :+: Err
-
-$(derive [smartConstructors, makeDifunctor, makeShowD, makeEqD, makeOrdD]
-         [''Lam, ''App, ''Const, ''Plus, ''Let, ''Err])
-
--- * Pretty printing
-data Stream a = Cons a (Stream a)
-
-class Pretty f where
-  prettyAlg :: Alg f (Stream String -> String)
-
-$(derive [liftSum] [''Pretty])
-
-pretty :: (Difunctor f, Pretty f) => Term f -> String
-pretty t = cata prettyAlg t (nominals 1)
-    where nominals n = Cons ('x' : show n) (nominals (n + 1))
-
-instance Pretty Lam where
-  prettyAlg (Lam f) (Cons x xs) = "(\\" ++ x ++ ". " ++ f (const x) xs ++ ")"
-
-instance Pretty App where
-  prettyAlg (App e1 e2) xs = "(" ++ e1 xs ++ " " ++ e2 xs ++ ")"
-
-instance Pretty Const where
-  prettyAlg (Const n) _ = show n
-
-instance Pretty Plus where
-  prettyAlg (Plus e1 e2) xs = "(" ++ e1 xs ++ " + " ++ e2 xs ++ ")"
-
-instance Pretty Err where
-  prettyAlg Err _ = "error"
-
-instance Pretty Let where
-  prettyAlg (Let e1 e2) (Cons x xs) = "let " ++ x ++ " = " ++ e1 xs ++ " in " ++ e2 (const x) xs
-
--- * Desugaring
-instance (Difunctor f, App :<: f, Lam :<: f) => Desugar Let f where
-  desugHom' (Let e1 e2) = inject (Lam e2) `iApp` e1
-
--- * Constant folding
-class Constf f g where
-  constfAlg :: forall a. Alg f (Trm g a)
-
-$(derive [liftSum] [''Constf])
-
-constf :: (Difunctor f, Constf f g) => Term f -> Term g
-constf t = Term (cata constfAlg t)
-
-instance (Difunctor f, f :<: g) => Constf f g where
-  constfAlg = inject . dimap Var id -- default instance
-
-instance (Plus :<: f, Const :<: f) => Constf Plus f where
-  constfAlg (Plus e1 e2) = case (project e1, project e2) of
-                             (Just (Const n),Just (Const m)) -> iConst (n + m)
-                             _                               -> e1 `iPlus` e2
-
--- * Call-by-value evaluation
-data Sem m = Fun (Sem m -> m (Sem m)) | Int Int
-
-class Monad m => Eval f m where
-  evalAlg :: Alg f (m (Sem m))
-
-$(derive [liftSum] [''Eval])
-
-eval :: (Difunctor f, Eval f m) => Term f -> m (Sem m)
-eval = cata evalAlg
-
-instance Monad m => Eval Lam m where
-  evalAlg (Lam f) = return (Fun (f . return))
-
-instance Monad m => Eval App m where
-  evalAlg (App mx my) = do x <- mx
-                           case x of Fun f -> f =<< my; _ -> fail "stuck"
-
-instance Monad m => Eval Const m where
-  evalAlg (Const n) = return (Int n)
-
-instance Monad m => Eval Plus m where
-  evalAlg (Plus mx my) = do x <- mx
-                            y <- my
-                            case (x,y) of (Int n,Int m) -> return (Int (n + m))
-                                          _             -> fail "stuck"
-
-instance Monad m => Eval Err m where
-  evalAlg Err = fail "error"
-
-e :: Term Sig
-e = Term (iLet (iConst 2) (\x -> (iLam (\y -> y `iPlus` x) `iApp` iConst 3)))
-
-e' :: Term Sig'
-e' = desugar e
-
-evalEx :: Maybe (Sem Maybe)
-evalEx = eval e'

File examples/Examples/Param/Names.hs

-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances,
-  OverlappingInstances #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.Param.Names
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- From names to parametric higher-order abstract syntax and back
---
--- The example illustrates how to convert a parse tree with explicit names into
--- an AST that uses parametric higher-order abstract syntax, and back again. The
--- example shows how we can easily convert object language binders to Haskell
--- binders, without having to worry about capture avoidance.
---
---------------------------------------------------------------------------------
-
-module Examples.Param.Names where
-
-import Data.Comp.Param hiding (Var)
-import qualified Data.Comp.Param as P
-import Data.Comp.Param.Derive
-import Data.Comp.Param.Ditraversable
-import Data.Comp.Param.Show ()
-import Data.Maybe
-import qualified Data.Map as Map
-import Control.Monad.Reader
-
-data Lam a b  = Lam (a -> b)
-data App a b  = App b b
-data Lit a b  = Lit Int
-data Plus a b = Plus b b
-type Name     = String                 -- The type of names
-data NLam a b = NLam Name b
-data NVar a b = NVar Name
-type SigB     = App :+: Lit :+: Plus
-type SigN     = NLam :+: NVar :+: SigB -- The name signature
-type SigP     = Lam :+: SigB           -- The PHOAS signature
-
-$(derive [makeDifunctor, makeShowD, makeEqD, smartConstructors]
-         [''Lam, ''App, ''Lit, ''Plus, ''NLam, ''NVar])
-$(derive [makeDitraversable]
-         [''App, ''Lit, ''Plus, ''NLam, ''NVar])
-
---------------------------------------------------------------------------------
--- Names to PHOAS translation
---------------------------------------------------------------------------------
-
-type M f a = Reader (Map.Map Name (Trm f a))
-
-class N2PTrans f g where
-  n2pAlg :: Alg f (M g a (Trm g a))
-
-
--- We make the lifting to sums explicit in order to make the N2PTrans
--- work with the default instance declaration further below.
-instance (N2PTrans f1 g, N2PTrans f2 g) => N2PTrans (f1 :+: f2) g where
-    n2pAlg = caseD n2pAlg n2pAlg
-
-n2p :: (Difunctor f, N2PTrans f g) => Term f -> Term g
-n2p t = Term $ runReader (cata n2pAlg t) Map.empty
-
-instance (Lam :<: g) => N2PTrans NLam g where
-  n2pAlg (NLam x b) = do vars <- ask
-                         return $ iLam $ \y -> runReader b (Map.insert x y vars)
-
-instance (Ditraversable f, f :<: g) => N2PTrans f g where
-  n2pAlg = liftM inject . disequence . dimap (return . P.Var) id -- default
-
-instance N2PTrans NVar g where
-  n2pAlg (NVar x) = liftM fromJust (asks (Map.lookup x))
-
-en :: Term SigN
-en = Term $ iNLam "x1" $ iNLam "x2" (iNLam "x3" $ iNVar "x2") `iApp` iNVar "x1"
-
-ep :: Term SigP
-ep = n2p en
-
---------------------------------------------------------------------------------
--- PHOAS to names translation
---------------------------------------------------------------------------------
-
-type M' = Reader [Name]
-
-class P2NTrans f g where
-  p2nAlg :: Alg f (M' (Trm g a))
-
-
--- We make the lifting to sums explicit in order to make the P2NTrans
--- work with the default instance declaration further below.
-instance (P2NTrans f1 g, P2NTrans f2 g) => P2NTrans (f1 :+: f2) g where
-    p2nAlg = caseD p2nAlg p2nAlg
-
-
-p2n :: (Difunctor f, P2NTrans f g) => Term f -> Term g
-p2n t = Term $ runReader (cata p2nAlg t) ['x' : show n | n <- [1..]]
-
-instance (Ditraversable f, f :<: g) => P2NTrans f g where
-  p2nAlg = liftM inject . disequence . dimap (return . P.Var) id -- default
-
-instance (NLam :<: g, NVar :<: g) => P2NTrans Lam g where
-  p2nAlg (Lam f) = do n:names <- ask
-                      return $ iNLam n (runReader (f (return $ iNVar n)) names)
-
-ep' :: Term SigP
-ep' = Term $ iLam $ \a -> iLam (\b -> (iLam $ \_ -> b)) `iApp` a
-
-en' :: Term SigN
-en' = p2n ep'

File examples/Examples/Param/Thunk.hs

-{-# LANGUAGE TemplateHaskell, TypeOperators, MultiParamTypeClasses,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances, OverlappingInstances #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.Param.Thunk
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
---------------------------------------------------------------------------------
-
-module Examples.Param.Thunk where
-
-import Data.Comp.Param
-import Data.Comp.Param.Show ()
-import Data.Comp.Param.Derive
-import Data.Comp.Param.Thunk
-
--- Signatures for values and operators
-data Const a e = Const Int
-data Lam a e = Lam (a -> e) -- Note: not e -> e
-data App a e = App e e
-data Op a e = Add e e | Mult e e
-data Fun a e = Fun (e -> e) -- Note: not a -> e
-
--- Signature for the simple expression language
-type Sig = Const :+: Lam :+: App :+: Op
--- Signature for values. Note the use of 'FunM' rather than 'Lam' (!)
-type Value = Const :+: Fun
--- Signature for ground values.
-type GValue = Const
-
--- Derive boilerplate code using Template Haskell
-$(derive [makeDifunctor, makeEqD, makeOrdD, makeShowD, smartConstructors]
-         [''Const, ''Lam, ''App, ''Op])
-$(derive [makeDitraversable]
-         [''Const, ''App, ''Op])
-
--- Term evaluation algebra. Note that we cannot use @AlgM Maybe f (Term v)@
--- because that would force @FunM@ to have the type @e -> e@ rather than
--- @e -> m e@. The latter is needed because the input to a @Lam@ (which is
--- evaluated to a @Fun@) will determine whether or not an error should be
--- returned. Example: @(\x -> x x) 42@ will produce an error because the
--- abstraction is applied to a non-functional, whereas @(\x -> x x)(\y -> y)@
--- will not.
-class EvalT f v where
-  evalAlgT :: Alg f (TrmT Maybe v a)
-
-$(derive [liftSum] [''EvalT])
-
--- Lift the evaluation algebra to a catamorphism
-evalT :: (Difunctor f, Ditraversable v, EvalT f v) => Term f -> Maybe (Term v)
-evalT t = nfT $ Term (cata evalAlgT t)
-
--- instance (Ditraversable f Maybe Any, f :<: v) => EvalT f v where
---   evalAlgT  = strict'
-
-instance (Difunctor f, f :<: v) => EvalT f v where
-  evalAlgT  = inject'
-
-
-instance (Const :<: v) => EvalT Op v where
-  evalAlgT (Add mx my)  = thunk $ do 
-                            Const x <- whnfPr mx
-                            Const y <- whnfPr my
-                            return $ iConst $ x + y
-  evalAlgT (Mult mx my) = thunk $ do 
-                            Const x <- whnfPr mx
-                            Const y <- whnfPr my
-                            return $ iConst $ x * y
-
-instance (Fun :<: v) => EvalT App v where
-  evalAlgT (App mx my) = thunk $ do 
-                           Fun f <- whnfPr mx
-                           -- lazy
-                           return $ f my
-                           -- strict
-                           -- liftM f $ whnf' my
-
-instance (Fun :<: v) => EvalT Lam v where
-  evalAlgT (Lam f) = inject $ Fun f
-
--- |Evaluation of expressions to ground values.
-evalMG :: Term Sig -> Maybe (Term GValue)
-evalMG e = termM $ nfPr $ eval e
-  where eval :: Term Sig -> TrmT Maybe Value a
-        eval = cata evalAlgT
-
-
--- Example: evalEx = Just (iConst 12) (3 * (2 + 2) = 12)
-evalMEx :: Maybe (Term GValue)
-evalMEx = evalMG $ Term $ iLam (\x -> iLam $ \y -> y `iMult` (x `iAdd` x))
-                   `iApp` iConst 2 `iApp` iConst 3
-
--- Example: type error
-evalMEx' :: Maybe (Term GValue)
-evalMEx' = evalMG $ Term $ iLam (\x -> iLam $ \y -> x `iMult` (x `iAdd` x))
-                   `iApp` iConst 2 `iApp` (iLam (\x -> x) `iAdd` iConst 2)
-
--- Example: non-termination
-evalMExY :: Maybe (Term GValue)
-evalMExY = evalMG $ Term $ iLam (\x -> iLam $ \y -> x `iMult` (x `iAdd` x))
-                   `iApp` iConst 2 `iApp` omega
-    where omega = iLam (\x -> x `iApp` x) `iApp` iLam (\x -> x `iApp` x)

File src/Data/Comp/MultiParam.hs

---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.MultiParam
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>, Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module defines the infrastructure necessary to use
--- /Generalised Parametric Compositional Data Types/. Generalised Parametric
--- Compositional Data Types is an extension of Compositional Data Types with
--- parametric higher-order abstract syntax (PHOAS) for usage with binders, and
--- GADTs. Generalised Parametric Compositional Data Types combines Generalised
--- Compositional Data Types ("Data.Comp.Multi") and Parametric Compositional
--- Data Types ("Data.Comp.Param"). Examples of usage are bundled with the
--- package in the library @examples\/Examples\/MultiParam@.
---
---------------------------------------------------------------------------------
-module Data.Comp.MultiParam (
-    module Data.Comp.MultiParam.Term
-  , module Data.Comp.MultiParam.Algebra
-  , module Data.Comp.MultiParam.HDifunctor
-  , module Data.Comp.MultiParam.Sum
-  , module Data.Comp.MultiParam.Annotation
-  , module Data.Comp.MultiParam.Equality
-    ) where
-
-import Data.Comp.MultiParam.Term
-import Data.Comp.MultiParam.Algebra
-import Data.Comp.MultiParam.HDifunctor
-import Data.Comp.MultiParam.Sum
-import Data.Comp.MultiParam.Annotation
-import Data.Comp.MultiParam.Equality

File src/Data/Comp/MultiParam/Algebra.hs

-{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
-  FlexibleContexts, CPP, KindSignatures #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.MultiParam.Algebra
--- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module defines the notion of algebras and catamorphisms, and their
--- generalizations to e.g. monadic versions and other (co)recursion schemes.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.MultiParam.Algebra (
-      -- * Algebras & Catamorphisms
-      Alg,
-      free,
-      cata,
-      cata',
-      appCxt,
-      
-      -- * Monadic Algebras & Catamorphisms
-      AlgM,
---      algM,
-      freeM,
-      cataM,
-      AlgM',
-      Compose(..),
-      freeM',
-      cataM',
-
-      -- * Term Homomorphisms
-      CxtFun,
-      SigFun,
-      Hom,
-      appHom,
-      appHom',
-      compHom,
-      appSigFun,
-      appSigFun',
-      compSigFun,
-      hom,
-      compAlg,
-
-      -- * Monadic Term Homomorphisms
-      CxtFunM,
-      SigFunM,
-      HomM,
-      sigFunM,
-      hom',
-      appHomM,
-      appTHomM,
-      appHomM',
-      appTHomM',
-      homM,
-      appSigFunM,
-      appTSigFunM,
-      appSigFunM',
-      appTSigFunM',
-      compHomM,
-      compSigFunM,
-      compAlgM,
-      compAlgM'
-    ) where
-
-import Prelude hiding (sequence, mapM)
-import Control.Monad hiding (sequence, mapM)
-import Data.Functor.Compose -- Functor composition
-import Data.Comp.MultiParam.Term
-import Data.Comp.MultiParam.HDifunctor
-import Data.Comp.MultiParam.HDitraversable
-
-{-| This type represents an algebra over a difunctor @f@ and carrier @a@. -}
-type Alg f a = f a a :-> a
-
-{-| Construct a catamorphism for contexts over @f@ with holes of type @b@, from
-  the given algebra. -}
-free :: forall h f a b. HDifunctor f
-        => Alg f a -> (b :-> a) -> Cxt h f a b :-> a
-free f g = run
-    where run :: Cxt h f a b :-> a
-          run (In t) = f (hfmap run t)
-          run (Hole x) = g x
-          run (Var p) = p
-
-{-| Construct a catamorphism from the given algebra. -}
-cata :: forall f a. HDifunctor f => Alg f a -> Term f :-> a 
-{-# NOINLINE [1] cata #-}
-cata f (Term t) = run t
-    where run :: Trm f a :-> a
-          run (In t) = f (hfmap run t)
-          run (Var x) = x
-
-{-| A generalisation of 'cata' from terms over @f@ to contexts over @f@, where
-  the holes have the type of the algebra carrier. -}
-cata' :: HDifunctor f => Alg f a -> Cxt h f a a :-> a
-{-# INLINE cata' #-}
-cata' f = free f id
-
-{-| This function applies a whole context into another context. -}
-appCxt :: HDifunctor f => Cxt Hole f a (Cxt h f a b) :-> Cxt h f a b
-appCxt (In t) = In (hfmap appCxt t)
-appCxt (Hole x) = x
-appCxt (Var p) = Var p
-
-{-| This type represents a monadic algebra. It is similar to 'Alg' but
-  the return type is monadic. -}
-type AlgM m f a = NatM m (f a a) a
-
-{-| Construct a monadic catamorphism for contexts over @f@ with holes of type
-  @b@, from the given monadic algebra. -}
-freeM :: forall m h f a b. (HDitraversable f, Monad m)
-         => AlgM m f a -> NatM m b a -> NatM m (Cxt h f a b) a
-freeM f g = run
-    where run :: NatM m (Cxt h f a b) a
-          run (In t) = f =<< hdimapM run t
-          run (Hole x) = g x
-          run (Var p) = return p
-
-{-| Construct a monadic catamorphism from the given monadic algebra. -}
-cataM :: forall m f a. (HDitraversable f, Monad m)
-         => AlgM m f a -> NatM m (Term f) a
-{-# NOINLINE [1] cataM #-}
-cataM algm (Term t) = run t
-    where run :: NatM m (Trm f a) a
-          run (In t) = algm =<< hdimapM run t
-          run (Var x) = return x
-
-{-| This type represents a monadic algebra, but where the covariant argument is
-  also a monadic computation. -}
-type AlgM' m f a = NatM m (f a (Compose m a)) a
-
-{-| Construct a monadic catamorphism for contexts over @f@ with holes of type
-  @b@, from the given monadic algebra. -}
-freeM' :: forall m h f a b. (HDifunctor f, Monad m)
-          => AlgM' m f a -> NatM m b a -> NatM m (Cxt h f a b) a
-freeM' f g = run
-    where run :: NatM m (Cxt h f a b) a
-          run (In t) = f $ hfmap (Compose . run) t
-          run (Hole x) = g x
-          run (Var p) = return p
-
-{-| Construct a monadic catamorphism from the given monadic algebra. -}
-cataM' :: forall m f a. (HDifunctor f, Monad m)
-          => AlgM' m f a -> NatM m (Term f) a
-{-# NOINLINE [1] cataM' #-}
-cataM' algm (Term t) = run t
-    where run :: NatM m (Trm f a) a
-          run (In t) = algm $ hfmap (Compose . run) t
-          run (Var x) = return x
-
-{-| This type represents a signature function. -}
-type SigFun f g = forall (a :: * -> *) (b :: * -> *) . f a b :-> g a b
-
-{-| This type represents a context function. -}
-type CxtFun f g = forall h. SigFun (Cxt h f) (Cxt h g)
-
-{-| This type represents a term homomorphism. -}
-type Hom f g = SigFun f (Context g)
-
-{-| Apply a term homomorphism recursively to a term/context. -}
-appHom :: forall f g. (HDifunctor f, HDifunctor g) => Hom f g -> CxtFun f g
-{-# INLINE [1] appHom #-}
-appHom f = run where
-    run :: CxtFun f g
-    run (In t) = appCxt (f (hfmap run t))
-    run (Hole x) = Hole x
-    run (Var p) = Var p
-
--- | Apply a term homomorphism recursively to a term/context. This is
--- a top-down variant of 'appHom'.
-appHom' :: forall f g. (HDifunctor g)
-              => Hom f g -> CxtFun f g
-{-# INLINE [1] appHom' #-}
-appHom' f = run where
-    run :: CxtFun f g
-    run (In t) = appCxt (hfmapCxt run (f t))
-    run (Hole x) = Hole x
-    run (Var p) = Var p
-
-{-| Compose two term homomorphisms. -}
-compHom :: (HDifunctor g, HDifunctor h)
-               => Hom g h -> Hom f g -> Hom f h
-compHom f g = appHom f . g
-
-{-| Compose an algebra with a term homomorphism to get a new algebra. -}
-compAlg :: (HDifunctor f, HDifunctor g) => Alg g a -> Hom f g -> Alg f a
-compAlg alg talg = cata' alg . talg
-
-{-| This function applies a signature function to the given context. -}
-appSigFun :: forall f g. (HDifunctor f) => SigFun f g -> CxtFun f g
-appSigFun f = run where
-    run :: CxtFun f g
-    run (In t) = In (f (hfmap run t))
-    run (Hole x) = Hole x
-    run (Var p) = Var p
-
-{-| This function applies a signature function to the given context. -}
-appSigFun' :: forall f g. (HDifunctor g) => SigFun f g -> CxtFun f g
-appSigFun' f = run where
-    run :: CxtFun f g
-    run (In t) = In (hfmap run (f t))
-    run (Hole x) = Hole x
-    run (Var p) = Var p
-
-{-| This function composes two signature functions. -}
-compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
-compSigFun f g = f . g
-
-{-| Lifts the given signature function to the canonical term homomorphism. -}
-hom :: HDifunctor g => SigFun f g -> Hom f g
-hom f = simpCxt . f
-
-{-| This type represents a monadic signature function. -}
-type SigFunM m f g = forall (a :: * -> *) (b :: * -> *) . NatM m (f a b) (g a b)
-
-{-| This type represents a monadic context function. -}
-type CxtFunM m f g = forall h . SigFunM m (Cxt h f) (Cxt h g)
-
-{-| This type represents a monadic term homomorphism. -}
-type HomM m f g = SigFunM m f (Cxt Hole g)
-
-
-{-| Lift the given signature function to a monadic signature function. Note that
-  term homomorphisms are instances of signature functions. Hence this function
-  also applies to term homomorphisms. -}
-sigFunM :: Monad m => SigFun f g -> SigFunM m f g
-sigFunM f = return . f
-
-{-| Lift the give monadic signature function to a monadic term homomorphism. -}
-hom' :: (HDifunctor f, HDifunctor g, Monad m)
-            => SigFunM m f g -> HomM m f g
-hom' f = liftM  (In . hfmap Hole) . f
-
-{-| Lift the given signature function to a monadic term homomorphism. -}
-homM :: (HDifunctor g, Monad m) => SigFun f g -> HomM m f g
-homM f = sigFunM $ hom f
-
-{-| Apply a monadic term homomorphism recursively to a term/context. -}
-appHomM :: forall f g m. (HDitraversable f, Monad m, HDifunctor g)
-               => HomM m f g -> CxtFunM m f g
-{-# NOINLINE [1] appHomM #-}
-appHomM f = run
-    where run :: CxtFunM m f g
-          run (In t) = liftM appCxt (f =<< hdimapM run t)
-          run (Hole x) = return (Hole x)
-          run (Var p) = return (Var p)
-
-{-| A restricted form of |appHomM| which only works for terms. -}
-appTHomM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)
-            => HomM m f g -> Term f i -> m (Term g i)
-appTHomM f (Term t) = termM (appHomM f t)
-
--- | Apply a monadic term homomorphism recursively to a
--- term/context. This is a top-down variant of 'appHomM'.
-appHomM' :: forall f g m. (HDitraversable g, Monad m)
-            => HomM m f g -> CxtFunM m f g
-{-# NOINLINE [1] appHomM' #-}
-appHomM' f = run
-    where run :: CxtFunM m f g
-          run (In t) = liftM appCxt (hdimapMCxt run =<<  f t)
-          run (Hole x) = return (Hole x)
-          run (Var p) = return (Var p)
-
-{-| A restricted form of |appHomM'| which only works for terms. -}
-appTHomM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)
-             => HomM m f g -> Term f i -> m (Term g i)
-appTHomM' f (Term t) = termM (appHomM' f t)
-
-{-| This function applies a monadic signature function to the given context. -}
-appSigFunM :: forall m f g. (HDitraversable f, Monad m)
-              => SigFunM m f g -> CxtFunM m f g
-appSigFunM f = run
-    where run :: CxtFunM m f g
-          run (In t)   = liftM In (f =<< hdimapM run t)
-          run (Hole x) = return (Hole x)
-          run (Var p)  = return (Var p)
-
-{-| A restricted form of |appSigFunM| which only works for terms. -}
-appTSigFunM :: (HDitraversable f, Monad m, ParamFunctor m, HDifunctor g)
-               => SigFunM m f g -> Term f i -> m (Term g i)
-appTSigFunM f (Term t) = termM (appSigFunM f t)
-
--- | This function applies a monadic signature function to the given
--- context. This is a top-down variant of 'appSigFunM'.
-appSigFunM' :: forall m f g. (HDitraversable g, Monad m)
-               => SigFunM m f g -> CxtFunM m f g
-appSigFunM' f = run
-    where run :: CxtFunM m f g
-          run (In t)   = liftM In (hdimapM run =<< f t)
-          run (Hole x) = return (Hole x)
-          run (Var p)  = return (Var p)
-
-{-| A restricted form of |appSigFunM'| which only works for terms. -}
-appTSigFunM' :: (HDitraversable g, Monad m, ParamFunctor m, HDifunctor g)
-                => SigFunM m f g -> Term f i -> m (Term g i)
-appTSigFunM' f (Term t) = termM (appSigFunM' f t)
-
-{-| Compose two monadic term homomorphisms. -}
-compHomM :: (HDitraversable g, HDifunctor h, Monad m)
-                => HomM m g h -> HomM m f g -> HomM m f h
-compHomM f g = appHomM f <=< g
-
-{-| Compose a monadic algebra with a monadic term homomorphism to get a new
-  monadic algebra. -}
-compAlgM :: (HDitraversable g, Monad m) => AlgM m g a -> HomM m f g -> AlgM m f a
-compAlgM alg talg = freeM alg return <=< talg
-
-{-| Compose a monadic algebra with a term homomorphism to get a new monadic
-  algebra. -}
-compAlgM' :: (HDitraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
-compAlgM' alg talg = freeM alg return . talg
-
-{-| This function composes two monadic signature functions. -}
-compSigFunM :: Monad m => SigFunM m g h -> SigFunM m f g -> SigFunM m f h
-compSigFunM f g a = g a >>= f
-
-{-
-#ifndef NO_RULES
-{-# RULES
-  "cata/appHom" forall (a :: Alg g d) (h :: Hom f g) x.
-    cata a (appHom h x) = cata (compAlg a h) x;
-
-  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
-    appHom a (appHom h x) = appHom (compHom a h) x; #-}
-
-{-
-{-# RULES 
-  "cataM/appHomM" forall (a :: AlgM m g d) (h :: HomM m f g d) x.
-     appHomM h x >>= cataM a = cataM (compAlgM a h) x;
-
-  "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.
-     cataM a (appHom h x) = cataM (compAlgM' a h) x;
-
-  "appHomM/appHomM" forall (a :: HomM m g h b) (h :: HomM m f g b) x.
-    appHomM h x >>= appHomM a = appHomM (compHomM a h) x; #-}
-
-{-# RULES
-  "cata/build"  forall alg (g :: forall a . Alg f a -> a) .
-                cata alg (build g) = g alg #-}
--}
-#endif
--}

File src/Data/Comp/MultiParam/Annotation.hs

-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.MultiParam.Annotation
--- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved
--- License     :  BSD3
--- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module defines annotations on signatures.
---
---------------------------------------------------------------------------------
-
-module Data.Comp.MultiParam.Annotation
-    (
-     (:&:) (..),
-     (:*:) (..),
-     DistAnn (..),
-     RemA (..),
-     liftA,
-     liftA',
-     stripA,
-     propAnn,
-     propAnnM,
-     ann,
-     project'
-    ) where
-
-import qualified Data.Comp.Ops as O
-import Data.Comp.MultiParam.HDifunctor
-import Data.Comp.MultiParam.Term
-import Data.Comp.MultiParam.Sum
-import Data.Comp.MultiParam.Ops
-import Data.Comp.MultiParam.Algebra
-
-import Control.Monad
-
-{-| Transform a function with a domain constructed from a higher-order difunctor
-  to a function with a domain constructed with the same higher-order difunctor,
-  but with an additional annotation. -}
-liftA :: (RemA s s') => (s' a b :-> t) -> s a b :-> t
-liftA f v = f (remA v)
-
-{-| Transform a function with a domain constructed from a higher-order difunctor
-  to a function with a domain constructed with the same higher-order difunctor,
-  but with an additional annotation. -}
-liftA' :: (DistAnn s' p s, HDifunctor s')
-          => (s' a b :-> Cxt h s' c d) -> s a b :-> Cxt h s c d
-liftA' f v = let v' O.:&: p = projectA v
-             in ann p (f v')
-
-{-| Strip the annotations from a term over a higher-order difunctor with
-  annotations. -}
-stripA :: (RemA g f, HDifunctor g) => CxtFun g f
-stripA = appSigFun remA
-
-{-| Lift a term homomorphism over signatures @f@ and @g@ to a term homomorphism
- over the same signatures, but extended with annotations. -}
-propAnn :: (DistAnn f p f', DistAnn g p g', HDifunctor g) 
-           => Hom f g -> Hom f' g'
-propAnn hom f' = ann p (hom f)
-    where f O.:&: p = projectA f'
-
-{-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic