diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2010--2011 Patrick Bahr, Tom Hvitved
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/compdata-param.cabal b/compdata-param.cabal
new file mode 100644
--- /dev/null
+++ b/compdata-param.cabal
@@ -0,0 +1,105 @@
+Name:			compdata-param
+Version:		0.8
+Synopsis:            	Parametric Compositional Data Types
+Description:
+
+  Based on Wouter Swierstra's Functional Pearl /Data types a la carte/
+  (Journal of Functional Programming, 18(4):423-436, 2008,
+  <http://dx.doi.org/10.1017/S0956796808006758>), this package
+  provides a framework for defining recursive data types in a
+  compositional manner with support for binders. 
+  .
+  This package implemements /parametric compositional data types/
+  (Workshop on Mathematically Structured Functional Programming, 3-24,
+  2012, <http://dx.doi.org/10.4204/EPTCS.76.3>), generalising
+  compositional data types (as implemented in the /compdata/ package)
+  with support for parametric higher-order abstract syntax
+  (PHOAS).
+  .
+  Examples of using parametric compositional data types are bundled
+  with the package in the folder @examples@.
+
+Category:            	Generics
+License:		BSD3
+License-file:		LICENSE
+Author:			Patrick Bahr, Tom Hvitved
+Maintainer:		paba@di.ku.dk
+Build-Type:		Simple
+Cabal-Version:          >=1.9.2
+
+extra-source-files:
+  -- test files
+  testsuite/tests/Tests.hs
+  testsuite/tests/Data/Comp/Examples_Test.hs
+  testsuite/tests/Data/Comp/Examples/*.hs
+  -- example files
+  examples/Examples/*.hs
+  examples/Examples/Multi/*.hs
+
+
+library
+  Exposed-Modules:      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
+
+                        Data.Comp.Param.Multi
+                        Data.Comp.Param.Multi.Term
+                        Data.Comp.Param.Multi.FreshM
+                        Data.Comp.Param.Multi.Sum
+                        Data.Comp.Param.Multi.HDifunctor
+                        Data.Comp.Param.Multi.HDitraversable
+                        Data.Comp.Param.Multi.Algebra
+                        Data.Comp.Param.Multi.Annotation
+                        Data.Comp.Param.Multi.Ops
+                        Data.Comp.Param.Multi.Equality
+                        Data.Comp.Param.Multi.Ordering
+                        Data.Comp.Param.Multi.Show
+                        Data.Comp.Param.Multi.Derive,
+                        Data.Comp.Param.Multi.Desugar
+
+  Other-Modules:        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.Param.Multi.Derive.HDifunctor
+                        Data.Comp.Param.Multi.Derive.Equality
+                        Data.Comp.Param.Multi.Derive.Ordering
+                        Data.Comp.Param.Multi.Derive.Show
+                        Data.Comp.Param.Multi.Derive.SmartConstructors
+                        Data.Comp.Param.Multi.Derive.SmartAConstructors
+                        Data.Comp.Param.Multi.Derive.Injections
+                        Data.Comp.Param.Multi.Derive.Projections
+
+  Build-Depends:	base == 4.*, template-haskell, mtl, transformers, compdata == 0.8.*
+  hs-source-dirs:	src
+  ghc-options:          -W
+
+
+Test-Suite test
+  Type:                 exitcode-stdio-1.0
+  Main-is:		Tests.hs
+  hs-source-dirs:	testsuite/tests examples
+  Build-Depends:        base == 4.*, template-haskell, mtl, transformers, compdata == 0.8.*, HUnit,
+                        test-framework, test-framework-hunit, containers, compdata-param
+
+source-repository head
+  type:     hg
+  location: https://bitbucket.org/paba/compdata-param
diff --git a/examples/Examples/Graph.hs b/examples/Examples/Graph.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Graph.hs
@@ -0,0 +1,77 @@
+{-# 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.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
diff --git a/examples/Examples/Lambda.hs b/examples/Examples/Lambda.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Lambda.hs
@@ -0,0 +1,131 @@
+{-# 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.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'
diff --git a/examples/Examples/Multi/FOL.hs b/examples/Examples/Multi/FOL.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Multi/FOL.hs
@@ -0,0 +1,436 @@
+{-# 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.Multi.FOL where
+
+import Data.Comp.Param.Multi hiding (Var)
+import qualified Data.Comp.Param.Multi as MP
+import Data.Comp.Param.Multi.Show ()
+import Data.Comp.Param.Multi.Derive
+import Data.Comp.Param.Multi.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
diff --git a/examples/Examples/Multi/Lambda.hs b/examples/Examples/Multi/Lambda.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Multi/Lambda.hs
@@ -0,0 +1,106 @@
+{-# 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.Multi.Lambda where
+
+import Data.Comp.Param.Multi
+import Data.Comp.Param.Multi.Show ()
+import Data.Comp.Param.Multi.Equality ()
+import Data.Comp.Param.Multi.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'
diff --git a/examples/Examples/Names.hs b/examples/Examples/Names.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Names.hs
@@ -0,0 +1,113 @@
+{-# 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.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'
diff --git a/examples/Examples/Thunk.hs b/examples/Examples/Thunk.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Thunk.hs
@@ -0,0 +1,106 @@
+{-# 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.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)
diff --git a/src/Data/Comp/Param.hs b/src/Data/Comp/Param.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param.hs
@@ -0,0 +1,32 @@
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param
+-- 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
+-- /Parametric Compositional Data Types/. Parametric Compositional Data Types 
+-- is an extension of Compositional Data Types with parametric
+-- higher-order abstract syntax (PHOAS) for usage with binders. Examples of
+-- usage are bundled with the package in the library
+-- @examples\/Examples\/Param@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param (
+    module Data.Comp.Param.Term
+  , module Data.Comp.Param.Algebra
+  , module Data.Comp.Param.Difunctor
+  , module Data.Comp.Param.Sum
+  , module Data.Comp.Param.Annotation
+  , module Data.Comp.Param.Equality
+    ) where
+
+import Data.Comp.Param.Term
+import Data.Comp.Param.Algebra
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.Sum
+import Data.Comp.Param.Annotation
+import Data.Comp.Param.Equality
diff --git a/src/Data/Comp/Param/Algebra.hs b/src/Data/Comp/Param/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Algebra.hs
@@ -0,0 +1,962 @@
+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
+  FlexibleContexts, CPP #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.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.Param.Algebra (
+      -- * Algebras & Catamorphisms
+      Alg,
+      free,
+      cata,
+      cata',
+      appCxt,
+      
+      -- * Monadic Algebras & Catamorphisms
+      AlgM,
+      algM,
+      freeM,
+      cataM,
+      cataM',
+
+      -- * Term Homomorphisms
+      CxtFun,
+      SigFun,
+      Hom,
+      appHom,
+      appHom',
+      compHom,
+      appSigFun,
+      appSigFun',
+      compSigFun,
+      compHomSigFun,
+      compSigFunHom,
+      hom,
+      compAlg,
+      compAlgSigFun,
+
+      -- * Monadic Term Homomorphisms
+      CxtFunM,
+      SigFunM,
+      HomM,
+      SigFunMD,
+      HomMD,
+      sigFunM,
+      appHomM,
+      appTHomM,
+      appHomM',
+      appTHomM',
+      homM,
+      homMD,
+      appSigFunM,
+      appTSigFunM,
+      appSigFunM',
+      appTSigFunM',
+      appSigFunMD,
+      appTSigFunMD,
+      compHomM,
+      compHomM',
+      compSigFunM,
+      compSigFunHomM,
+      compSigFunHomM',
+      compAlgSigFunM,
+      compAlgSigFunM',
+      compAlgM,
+      compAlgM',
+
+      -- * Coalgebras & Anamorphisms
+      Coalg,
+      ana,
+      CoalgM,
+      anaM,
+
+      -- * R-Algebras & Paramorphisms
+      RAlg,
+      para,
+      RAlgM,
+      paraM,
+
+      -- * R-Coalgebras & Apomorphisms
+      RCoalg,
+      apo,
+      RCoalgM,
+      apoM,
+
+      -- * CV-Algebras & Histomorphisms
+      CVAlg,
+      histo,
+      CVAlgM,
+      histoM,
+
+      -- * CV-Coalgebras & Futumorphisms
+      CVCoalg,
+      futu,
+      CVCoalg',
+      futu',
+      CVCoalgM,
+      futuM
+    ) where
+
+import Prelude hiding (sequence, mapM)
+import Control.Monad hiding (sequence, mapM)
+import Data.Comp.Param.Term
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.Ditraversable
+
+{-| 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. Difunctor 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 (difmap run t)
+          run (Hole x) = g x
+          run (Var p) = p
+
+{-| Construct a catamorphism from the given algebra. -}
+cata :: forall f a. Difunctor 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 (difmap 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' :: Difunctor 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 :: Difunctor f => Context f a (Cxt h f a b) -> Cxt h f a b
+appCxt (In t) = In (difmap 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 = f a a -> m a
+
+{-| Convert a monadic algebra into an ordinary algebra with a monadic
+  carrier. -}
+algM :: (Ditraversable f, Monad m) => AlgM m f a -> Alg f (m a)
+algM f x = disequence (dimap return id x) >>= f
+
+{-| 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. (Ditraversable f, Monad m)
+         => AlgM m f a -> (b -> m a) -> Cxt h f a b -> m a
+freeM f g = run
+    where run :: Cxt h f a b -> m a
+          run (In t) = f =<< dimapM 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. (Ditraversable f, Monad m) => AlgM m f a -> Term f -> m a
+{-# NOINLINE [1] cataM #-}
+cataM algm (Term t) = run t
+    where run :: Trm f a  -> m a
+          run (In t) = algm =<< dimapM run t
+          run (Var x) = return x
+
+{-| A generalisation of 'cataM' from terms over @f@ to contexts over @f@, where
+  the holes have the type of the monadic algebra carrier. -}
+cataM' :: forall m h f a. (Ditraversable f, Monad m)
+          => AlgM m f a -> Cxt h f a (m a) -> m a
+{-# NOINLINE [1] cataM' #-}
+cataM' f = freeM f id
+
+{-| This type represents a context function. -}
+type CxtFun f g = forall h a b. Cxt h f a b -> Cxt h g a b
+
+
+{-| This type represents a signature function. -}
+type SigFun f g = forall a b. f a b -> g a b
+
+{-| 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. (Difunctor f, Difunctor g) => Hom f g -> CxtFun f g
+{-# NOINLINE [1] appHom #-}
+appHom f = run where
+    run :: CxtFun f g
+    run (In t) = appCxt (f (difmap run t))
+    run (Hole x) = Hole x
+    run (Var p) = Var p
+
+{-| Apply a term homomorphism recursively to a term/context. -}
+appHom' :: forall f g. (Difunctor g) => Hom f g -> CxtFun f g
+{-# NOINLINE [1] appHom' #-}
+appHom' f = run where
+    run :: CxtFun f g
+    run (In t) = appCxt (fmapCxt run (f t))
+    run (Hole x) = Hole x
+    run (Var p) = Var p
+
+fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b'
+fmapCxt f = run
+    where run (In t) = In $ difmap run t
+          run (Var a) = Var a
+          run (Hole b)  = Hole $ f b
+
+{-| Compose two term homomorphisms. -}
+compHom :: (Difunctor g, Difunctor 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 :: (Difunctor f, Difunctor g) => Alg g a -> Hom f g -> Alg f a
+compAlg alg talg = cata' alg . talg
+
+compAlgSigFun  :: Alg g a -> SigFun f g -> Alg f a
+compAlgSigFun alg sig = alg . sig
+
+
+{-| This function applies a signature function to the given context. -}
+appSigFun :: forall f g. (Difunctor f) => SigFun f g -> CxtFun f g
+{-# NOINLINE [1] appSigFun #-}
+appSigFun f = run
+    where run (In t) = In $ f $ difmap run t
+          run (Var x) = Var x
+          run (Hole x) = Hole x
+-- implementation via term homomorphisms
+--  appSigFun f = appHom $ hom f
+
+
+-- | This function applies a signature function to the given
+-- context. This is a top-bottom variant of 'appSigFun'.
+appSigFun' :: forall f g. (Difunctor g) => SigFun f g -> CxtFun f g
+{-# NOINLINE [1] appSigFun' #-}
+appSigFun' f = run
+    where run (In t) = In $ difmap run $ f t
+          run (Var x) = Var x
+          run (Hole x) = Hole x
+
+{-| This function composes two signature functions. -}
+compSigFun :: SigFun g h -> SigFun f g -> SigFun f h
+compSigFun f g = f . g
+
+{-| This function composes a term homomorphism and a signature function. -}
+compHomSigFun :: Hom g h -> SigFun f g -> Hom f h
+compHomSigFun f g = f . g
+
+{-| This function composes a term homomorphism and a signature function. -}
+compSigFunHom :: (Difunctor g) => SigFun g h -> Hom f g -> Hom f h
+compSigFunHom f g = appSigFun f . g
+
+
+{-| Lifts the given signature function to the canonical term homomorphism. -}
+hom :: Difunctor 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. f a b -> m (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 signature function. It is similar to
+  'SigFunM' but has monadic values also in the domain. -}
+type SigFunMD m f g = forall a b. f a (m b) -> m (g a b)
+
+{-| This type represents a monadic term homomorphism. -}
+type HomM m f g = SigFunM m f (Context g)
+
+{-| This type represents a monadic term homomorphism. It is similar to
+  'HomM' but has monadic values also in the domain. -}
+type HomMD m f g = SigFunMD m f (Context 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 given signature function to a monadic term homomorphism. -}
+homM :: (Difunctor g, Monad m) => SigFunM m f g -> HomM m f g
+homM f = liftM simpCxt . f
+
+-- | Apply a monadic term homomorphism recursively to a
+-- term/context. The monad is sequenced bottom-up.
+appHomM :: forall f g m. (Ditraversable f, Difunctor 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 . f =<< dimapM 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 :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)
+            => HomM m f g -> Term f -> m (Term g)
+appTHomM f (Term t) = termM (appHomM f t)
+
+
+-- | Apply a monadic term homomorphism recursively to a
+-- term/context. The monad is sequence top-down.
+appHomM' :: forall f g m. (Ditraversable g, Monad m)
+            => HomM m f g -> CxtFunM m f g
+appHomM' f = run
+    where run :: CxtFunM m f g
+          run (In t)  = liftM appCxt . dimapMCxt run =<< f t
+          run (Var p) = return (Var p)
+          run (Hole x) = return (Hole x)
+
+dimapMCxt :: (Ditraversable f, Monad m)
+             => (b -> m b') -> Cxt h f a b -> m (Cxt h f a b')
+dimapMCxt f = run
+              where run (In t) = liftM In $ dimapM run t
+                    run (Var a)  = return $ Var a
+                    run (Hole b) = liftM Hole (f b)
+
+{-| A restricted form of |appHomM'| which only works for terms. -}
+appTHomM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g)
+             => HomM m f g -> Term f -> m (Term g)
+appTHomM' f (Term t) = termM (appHomM' f t)
+            
+
+{-| This function constructs the unique monadic homomorphism from the
+  initial term algebra to the given term algebra. -}
+homMD :: forall f g m. (Difunctor f, Difunctor g, Monad m)
+         => HomMD m f g -> CxtFunM m f g
+homMD f = run 
+    where run :: CxtFunM m f g
+          run (In t) = liftM appCxt (f (difmap run t))
+          run (Hole x) = return (Hole x)
+          run (Var p) = return (Var p)
+
+{-| This function applies a monadic signature function to the given context. -}
+appSigFunM :: forall m f g. (Ditraversable 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 =<< dimapM run t
+          run (Var x) = return $ Var x
+          run (Hole x) = return $ Hole x
+-- implementation via term homomorphisms
+--  appSigFunM f = appHomM $ hom' f
+
+{-| A restricted form of |appSigFunM| which only works for terms. -}
+appTSigFunM :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)
+               => SigFunM m f g -> Term f -> m (Term g)
+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. (Ditraversable 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 . dimapM run =<< f t
+          run (Var x) = return $ Var x
+          run (Hole x) = return $ Hole x
+
+{-| A restricted form of |appSigFunM'| which only works for terms. -}
+appTSigFunM' :: (Ditraversable g, ParamFunctor m, Monad m, Difunctor g)
+                => SigFunM m f g -> Term f -> m (Term g)
+appTSigFunM' f (Term t) = termM (appSigFunM' f t)
+
+{-| This function applies a signature function to the given context. -}
+appSigFunMD :: forall f g m. (Ditraversable f, Difunctor g, Monad m)
+               => SigFunMD m f g -> CxtFunM m f g
+appSigFunMD f = run 
+    where run :: CxtFunM m f g
+          run (In t) = liftM In (f (difmap run t))
+          run (Hole x) = return (Hole x)
+          run (Var p) = return (Var p)
+
+{-| A restricted form of |appSigFunMD| which only works for terms. -}
+appTSigFunMD :: (Ditraversable f, ParamFunctor m, Monad m, Difunctor g)
+                => SigFunMD m f g -> Term f -> m (Term g)
+appTSigFunMD f (Term t) = termM (appSigFunMD f t)
+
+{-| Compose two monadic term homomorphisms. -}
+compHomM :: (Ditraversable g, Difunctor h, Monad m)
+            => HomM m g h -> HomM m f g -> HomM m f h
+compHomM f g = appHomM f <=< g
+
+{-| Compose two monadic term homomorphisms. -}
+compHomM' :: (Ditraversable h, Monad m) => HomM m g h -> HomM m f g -> HomM m f h
+compHomM' f g = appHomM' f <=< g
+
+{-{-| Compose two monadic term homomorphisms. -}
+compHomM_ :: (Difunctor h, Difunctor g, Monad m)
+                => Hom g h -> HomM m f g -> HomM m f h
+compHomM_ f g = liftM (appHom f) . g
+
+{-| Compose two monadic term homomorphisms. -}
+compHomSigFunM :: Monad m => HomM m g h -> SigFunM m f g -> HomM m f h
+compHomSigFunM f g = f <=< g-}
+
+{-| Compose two monadic term homomorphisms. -}
+compSigFunHomM :: (Ditraversable g, Monad m)
+                  => SigFunM m g h -> HomM m f g -> HomM m f h
+compSigFunHomM f g = appSigFunM f <=< g
+
+{-| Compose two monadic term homomorphisms. -}
+compSigFunHomM' :: (Ditraversable h, Monad m)
+                   => SigFunM m g h -> HomM m f g -> HomM m f h
+compSigFunHomM' f g = appSigFunM' f <=< g
+
+{-| Compose a monadic algebra with a monadic term homomorphism to get a new
+  monadic algebra. -}
+compAlgM :: (Ditraversable 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' :: (Ditraversable g, Monad m) => AlgM m g a -> Hom f g -> AlgM m f a
+compAlgM' alg talg = freeM alg return . talg
+
+{-| Compose a monadic algebra with a monadic signature function to get a new
+  monadic algebra. -}
+compAlgSigFunM :: Monad m => AlgM m g a -> SigFunM m f g -> AlgM m f a
+compAlgSigFunM alg talg = alg <=< talg
+
+
+{-| Compose a monadic algebra with a signature function to get a new monadic
+  algebra. -}
+compAlgSigFunM' :: AlgM m g a -> SigFun f g -> AlgM m f a
+compAlgSigFunM' alg talg = alg . 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 = f <=< g
+
+
+----------------
+-- Coalgebras --
+----------------
+
+{-| This type represents a coalgebra over a difunctor @f@ and carrier @a@. The
+  list of @(a,b)@s represent the parameters that may occur in the constructed
+  value. The first component represents the seed of the parameter,
+  and the second component is the (polymorphic) parameter itself. If @f@ is
+  itself a binder, then the parameters bound by @f@ can be passed to the
+  covariant argument, thereby making them available to sub terms. -}
+type Coalg f a = forall b. a -> [(a,b)] -> Either b (f b (a,[(a,b)]))
+
+{-| Construct an anamorphism from the given coalgebra. -}
+ana :: Difunctor f => Coalg f a -> a -> Term f
+ana f x = Term $ anaAux f x
+    where anaAux :: Difunctor f => Coalg f a -> a -> (forall a. Trm f a)
+          anaAux f x = run (x,[])
+              where run (a,bs) = case f a bs of
+                                   Left p -> Var p
+                                   Right t -> In $ difmap run t
+
+{-| This type represents a monadic coalgebra over a difunctor @f@ and carrier
+  @a@. -}
+type CoalgM m f a = forall b. a -> [(a,b)] -> m (Either b (f b (a,[(a,b)])))
+
+{-| Construct a monadic anamorphism from the given monadic coalgebra. -}
+anaM :: forall a m f. (Ditraversable f, Monad m)
+     => CoalgM m f a -> a -> forall a. m (Trm f a)
+anaM f x = run (x,[])
+    where run (a,bs) = do c <- f a bs
+                          case c of
+                            Left p -> return $ Var p
+                            Right t -> liftM In $ dimapM run t
+
+
+--------------------------------
+-- R-Algebras & Paramorphisms --
+--------------------------------
+
+{-| This type represents an r-algebra over a difunctor @f@ and carrier @a@. -}
+type RAlg f a = f a (Trm f a, a) -> a
+
+{-| Construct a paramorphism from the given r-algebra. -}
+para :: forall f a. Difunctor f => RAlg f a -> Term f -> a
+para f (Term t) = run t
+    where run :: Trm f a -> a
+          run (In t) = f $ difmap (\x -> (x, run x)) t
+          run (Var x) = x
+
+{-| This type represents a monadic r-algebra over a difunctor @f@ and carrier
+  @a@. -}
+type RAlgM m f a = f a (Trm f a, a) -> m a
+{-| Construct a monadic paramorphism from the given monadic r-algebra. -}
+paraM :: forall m f a. (Ditraversable f, Monad m) => RAlgM m f a -> Term f -> m a
+paraM f (Term t) = run t
+    where run :: Trm f a -> m a
+          run (In t) = f =<< dimapM (\x -> run x >>= \y -> return (x, y)) t
+          run (Var x) = return x
+
+
+--------------------------------
+-- R-Coalgebras & Apomorphisms --
+--------------------------------
+
+{-| This type represents an r-coalgebra over a difunctor @f@ and carrier @a@. -}
+type RCoalg f a = forall b. a -> [(a,b)] -> Either b (f b (Either (Trm f b) (a,[(a,b)])))
+
+{-| Construct an apomorphism from the given r-coalgebra. -}
+apo :: Difunctor f => RCoalg f a -> a -> Term f
+apo f x = Term (apoAux f x)
+    where apoAux :: Difunctor f => RCoalg f a -> a -> (forall a. Trm f a)
+          apoAux coa x = run (x,[])
+              where -- run :: (a,[(a,b)]) -> Trm f b
+                run (a,bs) = case coa a bs of
+                               Left x -> Var x
+                               Right t -> In $ difmap run' t
+                -- run' :: Either (Trm f b) (a,[(a,b)]) -> Trm f b
+                run' (Left t) = t
+                run' (Right x) = run x
+
+
+
+{-| This type represents a monadic r-coalgebra over a functor @f@ and carrier
+  @a@. -}
+type RCoalgM m f a = forall b. a -> [(a,b)] -> m (Either b (f b (Either (Trm f b) (a,[(a,b)]))))
+
+{-| Construct a monadic apomorphism from the given monadic r-coalgebra. -}
+apoM :: forall f m a. (Ditraversable f, Monad m)
+        => RCoalgM m f a -> a -> forall a. m (Trm f a)
+apoM coa x = run (x,[]) 
+    where run (a,bs) = do
+            res <- coa a bs
+            case res of
+              Left x -> return $ Var x
+              Right t -> liftM In $ dimapM run' t
+          run' (Left t) = return t
+          run' (Right x) = run x
+
+
+----------------------------------
+-- CV-Algebras & Histomorphisms --
+----------------------------------
+
+{-| This type represents a cv-algebra over a difunctor @f@ and carrier @a@. -}
+type CVAlg f a f' = f a (Trm f' a) -> a
+
+-- | This function applies 'projectA' at the tip of the term.
+projectTip  :: DistAnn f a f' => Trm f' a -> a
+projectTip (In v) = snd $ projectA v
+projectTip (Var p) = p
+
+{-| Construct a histomorphism from the given cv-algebra. -}
+histo :: forall f f' a. (Difunctor f, DistAnn f a f')
+         => CVAlg f a f' -> Term f -> a
+histo alg = projectTip . cata run
+    where run :: Alg f (Trm f' a)
+          run v = In $ injectA (alg v') v'
+              where v' = dimap Var id v
+
+{-| This type represents a monadic cv-algebra over a functor @f@ and carrier
+  @a@. -}
+type CVAlgM m f a f' = f a (Trm f' a) -> m a
+
+{-| Construct a monadic histomorphism from the given monadic cv-algebra. -}
+histoM :: forall f f' m a. (Ditraversable f, Monad m, DistAnn f a f')
+          => CVAlgM m f a f' -> Term f -> m a
+histoM alg (Term t) = liftM projectTip (run t)
+    where run :: Trm f a -> m (Trm f' a)
+          run (In t) = do t' <- dimapM run t
+                          r <- alg t'
+                          return $ In $ injectA r t'
+          run (Var p) = return $ Var p
+
+
+-----------------------------------
+-- CV-Coalgebras & Futumorphisms --
+-----------------------------------
+
+{-| This type represents a cv-coalgebra over a difunctor @f@ and carrier @a@.
+  The list of @(a,b)@s represent the parameters that may occur in the
+  constructed value. The first component represents the seed of the parameter,
+  and the second component is the (polymorphic) parameter itself. If @f@ is
+  itself a binder, then the parameters bound by @f@ can be passed to the
+  covariant argument, thereby making them available to sub terms. -}
+type CVCoalg f a = forall b. a -> [(a,b)]
+                 -> Either b (f b (Context f b (a,[(a,b)])))
+
+{-| Construct a futumorphism from the given cv-coalgebra. -}
+futu :: Difunctor f => CVCoalg f a -> a -> Term f
+futu f x = Term (futuAux f x)
+    where futuAux :: Difunctor f => CVCoalg f a -> a -> (forall a. Trm f a)
+          futuAux coa x = run (x,[])
+              where run (a,bs) = case coa a bs of
+                                   Left p -> Var p
+                                   Right t -> In $ difmap run' t
+                    run' (In t) = In $ difmap run' t
+                    run' (Hole x) = run x
+                    run' (Var p) = Var p
+
+{-| This type represents a monadic cv-coalgebra over a difunctor @f@ and carrier
+  @a@. -}
+type CVCoalgM m f a = forall b. a -> [(a,b)]
+                    -> m (Either b (f b (Context f b (a,[(a,b)]))))
+
+{-| Construct a monadic futumorphism from the given monadic cv-coalgebra. -}
+futuM :: forall f a m. (Ditraversable f, Monad m) =>
+         CVCoalgM m f a -> a -> forall a. m (Trm f a)
+futuM coa x = run (x,[])
+    where run (a,bs) = do c <- coa a bs
+                          case c of 
+                            Left p -> return $ Var p
+                            Right t -> liftM In $ dimapM run' t
+          run' (In t) = liftM In $ dimapM run' t
+          run' (Hole x) = run x
+          run' (Var p) = return $ Var p
+
+{-| This type represents a generalised cv-coalgebra over a difunctor @f@ and
+  carrier @a@. -}
+type CVCoalg' f a = forall b. a -> [(a,b)] -> Context f b (a,[(a,b)])
+
+{-| Construct a futumorphism from the given generalised cv-coalgebra. -}
+futu' :: Difunctor f => CVCoalg' f a -> a -> Term f
+futu' f x = Term (futuAux' f x)
+    where futuAux' :: Difunctor f => CVCoalg' f a -> a -> (forall a. Trm f a)
+          futuAux' coa x = run (x,[])
+              where run (a,bs) = run' $ coa a bs
+                    run' (In t) = In $ difmap run' t
+                    run' (Hole x) = run x
+                    run' (Var p) = Var p
+
+{--------------------------------------------
+-- functions only used for rewrite rules --
+-------------------------------------------
+
+appAlgHom :: forall f g d. Difunctor g => Alg g d -> Hom f g -> Term f -> d
+{-# NOINLINE [1] appAlgHom #-}
+appAlgHom alg hom (Term t) = run t where
+    run :: Trm f d -> d
+    run (In t) = run' $ hom t
+    run (Var a) = a
+    run' :: Context g d (Trm f d) -> d
+    run' (In t) = alg $ fmap run' t
+    run' (Var a) = a
+    run' (Hole x) = run x
+
+
+-- | This function applies a signature function after a term homomorphism.
+appSigFunHom :: forall f g h. (Difunctor g)
+                => SigFun g h -> Hom f g -> CxtFun f h
+{-# NOINLINE [1] appSigFunHom #-}
+appSigFunHom f g = run where
+    run :: CxtFun f h
+    run (In t) = run' $ g t
+    run (Var a) = Var a
+    run (Hole h) = Hole h
+    run' :: Context g a (Cxt h' f a b) -> Cxt h' h a b
+    run' (In t) = In $ f $ fmap run' t
+    run' (Var a) = Var a
+    run' (Hole h) = run h
+
+appAlgHomM :: forall m g f d. Ditraversable g
+              => AlgM m g d -> HomM m f g -> Term f -> m d
+appAlgHomM alg hom (Term t) = run t where
+    run :: Trm f d -> m d
+    run (In t) = run' =<< hom t
+    run (Var a) = return a
+    run' :: Context g d (Trm f d) -> m d
+    run' (In t) = alg =<< dimapM run' t
+    run' (Var a) = return a
+    run' (Hole x) = run x
+
+appHomHomM :: forall m f g h. (Ditraversable g, Difunctor h)
+              => HomM m g h -> HomM m f g -> CxtFunM m f h
+appHomHomM f g = run where
+--    run :: CxtFunM m f h
+    run (In t) = run' =<< g t
+    run (Var a) = return $ Var a
+    run (Hole h) = return $ Hole h
+--    run' :: Context g Any (Cxt h' f Any b) -> m (Cxt h' h Any b)
+    run' (In t) = liftM appCxt $ f =<< dimapM run' t
+    run' (Var a) = return $ Var a
+    run' (Hole h) = run h
+
+appSigFunHomM :: forall m f g h. Ditraversable g
+                 => SigFunM m g h -> HomM m f g -> CxtFunM m f h
+appSigFunHomM f g = run where
+--    run :: CxtFunM m f h
+    run (In t) = run' =<< g t
+    run (Var a) = return $ Var a
+    run (Hole h) = return $ Hole h
+--    run' :: Context g Any (Cxt h' f Any b) -> m (Cxt h' h Any b)
+    run' (In t) = liftM In $ f =<< dimapM run' t
+    run' (Var a) = return $ Var a
+    run' (Hole h) = run h
+
+
+-------------------
+-- rewrite rules --
+-------------------
+
+#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;
+
+  "cata/appHom'" forall (a :: Alg g d) (h :: Hom f g) x.
+    cata a (appHom' h x) = appAlgHom a h x;
+
+  "cata/appSigFun" forall (a :: Alg g d) (h :: SigFun f g) x.
+    cata a (appSigFun h x) = cata (compAlgSigFun a h) x;
+
+  "cata/appSigFun'" forall (a :: Alg g d) (h :: SigFun f g) x.
+    cata a (appSigFun' h x) = appAlgHom a (hom h) x;
+
+  "cata/appSigFunHom" forall (f :: Alg f3 d) (g :: SigFun f2 f3)
+                                      (h :: Hom f1 f2) x.
+    cata f (appSigFunHom g h x) = appAlgHom (compAlgSigFun f g) h x;
+
+  "appAlgHom/appHom" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.
+    appAlgHom a h (appHom f x) = cata (compAlg a (compHom h f)) x;
+
+  "appAlgHom/appHom'" forall (a :: Alg h d) (f :: Hom f g) (h :: Hom g h) x.
+    appAlgHom a h (appHom' f x) = appAlgHom a (compHom h f) x;
+
+  "appAlgHom/appSigFun" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.
+    appAlgHom a h (appSigFun f x) = cata (compAlg a (compHomSigFun h f)) x;
+
+  "appAlgHom/appSigFun'" forall (a :: Alg h d) (f :: SigFun f g) (h :: Hom g h) x.
+    appAlgHom a h (appSigFun' f x) = appAlgHom a (compHomSigFun h f) x;
+
+  "appAlgHom/appSigFunHom" forall (a :: Alg i d) (f :: Hom f g) (g :: SigFun g h)
+                                          (h :: Hom h i) x.
+    appAlgHom a h (appSigFunHom g f x)
+      = appAlgHom a (compHom (compHomSigFun h g) f) x;
+
+  "appHom/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
+    appHom a (appHom h x) = appHom (compHom 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;
+
+  "appHom'/appHom" forall (a :: Hom g h) (h :: Hom f g) x.
+    appHom' a (appHom h x) = appHom (compHom 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;
+    
+  "appSigFun/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
+    appSigFun f (appSigFun g x) = appSigFun (compSigFun f g) x;
+
+  "appSigFun'/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.
+    appSigFun' f (appSigFun' g x) = appSigFun' (compSigFun f g) x;
+
+  "appSigFun/appSigFun'" forall (f :: SigFun g h) (g :: SigFun f g) x.
+    appSigFun f (appSigFun' g x) = appSigFunHom f (hom g) x;
+
+  "appSigFun'/appSigFun" forall (f :: SigFun g h) (g :: SigFun f g) x.
+    appSigFun' f (appSigFun g x) = appSigFun (compSigFun f g) x;
+
+  "appHom/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
+    appHom f (appSigFun g x) = appHom (compHomSigFun f g) x;
+
+  "appHom/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.
+    appHom f (appSigFun' g x) =  appHom' (compHomSigFun f g) x;
+
+  "appHom'/appSigFun'" forall (f :: Hom g h) (g :: SigFun f g) x.
+    appHom' f (appSigFun' g x) =  appHom' (compHomSigFun f g) x;
+
+  "appHom'/appSigFun" forall (f :: Hom g h) (g :: SigFun f g) x.
+    appHom' f (appSigFun g x) = appHom (compHomSigFun f g) x;
+    
+  "appSigFun/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
+    appSigFun f (appHom g x) = appSigFunHom f g x;
+
+  "appSigFun'/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.
+    appSigFun' f (appHom' g x) = appHom' (compSigFunHom f g) x;
+
+  "appSigFun/appHom'" forall (f :: SigFun g h) (g :: Hom f g) x.
+    appSigFun f (appHom' g x) = appSigFunHom f g x;
+
+  "appSigFun'/appHom" forall (f :: SigFun g h) (g :: Hom f g) x.
+    appSigFun' f (appHom g x) = appHom (compSigFunHom f g) x;
+    
+  "appSigFunHom/appSigFun" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
+                                      (h :: SigFun f1 f2) x.
+    appSigFunHom f g (appSigFun h x)
+    = appSigFunHom f (compHomSigFun g h) x;
+
+  "appSigFunHom/appSigFun'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
+                                      (h :: SigFun f1 f2) x.
+    appSigFunHom f g (appSigFun' h x)
+    = appSigFunHom f (compHomSigFun g h) x;
+
+  "appSigFunHom/appHom" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
+                                      (h :: Hom f1 f2) x.
+    appSigFunHom f g (appHom h x)
+    = appSigFunHom f (compHom g h) x;
+
+  "appSigFunHom/appHom'" forall (f :: SigFun f3 f4) (g :: Hom f2 f3)
+                                      (h :: Hom f1 f2) x.
+    appSigFunHom f g (appHom' h x)
+    = appSigFunHom f (compHom g h) x;
+
+  "appSigFun/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)
+                                      (h :: Hom f1 f2) x.
+    appSigFun f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;
+
+  "appSigFun'/appSigFunHom" forall (f :: SigFun f3 f4) (g :: SigFun f2 f3)
+                                      (h :: Hom f1 f2) x.
+    appSigFun' f (appSigFunHom g h x) = appSigFunHom (compSigFun f g) h x;
+
+  "appHom/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)
+                                      (h :: Hom f1 f2) x.
+    appHom f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;
+
+  "appHom'/appSigFunHom" forall (f :: Hom f3 f4) (g :: SigFun f2 f3)
+                                      (h :: Hom f1 f2) x.
+    appHom' f (appSigFunHom g h x) = appHom' (compHom (compHomSigFun f g) h) x;
+
+  "appSigFunHom/appSigFunHom" forall (f1 :: SigFun f4 f5) (f2 :: Hom f3 f4)
+                                             (f3 :: SigFun f2 f3) (f4 :: Hom f1 f2) x.
+    appSigFunHom f1 f2 (appSigFunHom f3 f4 x)
+      = appSigFunHom f1 (compHom (compHomSigFun f2 f3) f4) x; #-}
+
+{-# RULES 
+  "cataM/appHomM" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
+     appHomM h x >>= cataM a =  appAlgHomM a h x;
+
+  "cataM/appHomM'" forall (a :: AlgM Maybe g d) (h :: HomM Maybe f g) x.
+     appHomM' h x >>= cataM a = appAlgHomM a h x;
+
+  "cataM/appSigFunM" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.
+     appSigFunM h x >>= cataM a = appAlgHomM a (homM h) x;
+
+  "cataM/appSigFunM'" forall (a :: AlgM Maybe g d) (h :: SigFunM Maybe f g) x.
+     appSigFunM' h x >>= cataM a = appAlgHomM a (homM h) x;
+
+  "cataM/appHom" forall (a :: AlgM m g d) (h :: Hom f g) x.
+     cataM a (appHom h x) = appAlgHomM a (sigFunM h) x;
+
+  "cataM/appHom'" forall (a :: AlgM m g d) (h :: Hom f g) x.
+     cataM a (appHom' h x) = appAlgHomM a (sigFunM h) x;
+
+  "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.
+     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;
+
+  "cataM/appSigFun'" forall (a :: AlgM m g d) (h :: SigFun f g) x.
+     cataM a (appSigFun' h x) = appAlgHomM a (sigFunM $ hom h) x;
+
+  "cataM/appSigFun" forall (a :: AlgM m g d) (h :: SigFun f g) x.
+     cataM a (appSigFun h x) = appAlgHomM a (sigFunM $ hom h) x;
+
+  "cataM/appSigFunHom" forall (a :: AlgM m h d) (g :: SigFun g h) (f :: Hom f g) x.
+     cataM a (appSigFunHom g f x) = appAlgHomM a (sigFunM $ compSigFunHom g f) x;
+
+  "appHomM/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM h x >>= appHomM a = appHomM (compHomM a h) x;
+
+  "appHomM/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM h x >>= appHomM a = appHomM (compHomSigFunM a h) x;
+
+  "appHomM/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM' h x >>= appHomM a = appHomHomM a h x;
+
+  "appHomM/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM' h x >>= appHomM a = appHomHomM a (homM h) x;
+
+  "appHomM'/appHomM" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM h x >>= appHomM' a = appHomM' (compHomM' a h) x;
+
+  "appHomM'/appSigFunM" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;
+
+  "appHomM'/appHomM'" forall (a :: HomM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM' h x >>= appHomM' a = appHomM' (compHomM' a h) x;
+
+  "appHomM'/appSigFunM'" forall (a :: HomM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM' h x >>= appHomM' a = appHomM' (compHomSigFunM a h) x;
+
+  "appHomM/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.
+     appHomM a (appHom h x) = appHomHomM a (sigFunM h) x;
+
+  "appHomM/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.
+     appHomM a (appSigFun h x) = appHomHomM a (sigFunM $ hom h) x;
+
+  "appHomM'/appHom" forall (a :: HomM m g h) (h :: Hom f g) x.
+     appHomM' a (appHom h x) = appHomM' (compHomM' a (sigFunM h)) x;
+
+  "appHomM'/appSigFun" forall (a :: HomM m g h) (h :: SigFun f g) x.
+     appHomM' a (appSigFun h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;
+
+  "appHomM/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.
+     appHomM a (appHom' h x) = appHomHomM a (sigFunM h) x;
+
+  "appHomM/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.
+     appHomM a (appSigFun' h x) = appHomHomM a (sigFunM $ hom h) x;
+
+  "appHomM'/appHom'" forall (a :: HomM m g h) (h :: Hom f g) x.
+     appHomM' a (appHom' h x) = appHomM' (compHomM' a (sigFunM h)) x;
+
+  "appHomM'/appSigFun'" forall (a :: HomM m g h) (h :: SigFun f g) x.
+     appHomM' a (appSigFun' h x) = appHomM' (compHomSigFunM a (sigFunM h)) x;
+
+  "appSigFunM/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM h x >>= appSigFunM a = appSigFunHomM a h x;
+
+  "appSigFunHomM/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM h x >>= appSigFunM a = appSigFunM (compSigFunM a h) x;
+
+  "appSigFunM/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM' h x >>= appSigFunM a = appSigFunHomM a h x;
+
+  "appSigFunM/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM' h x >>= appSigFunM a = appSigFunHomM a (homM h) x;
+
+  "appSigFunM'/appHomM" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;
+
+  "appSigFunM'/appSigFunM" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;
+
+  "appSigFunM'/appHomM'" forall (a :: SigFunM Maybe g h) (h :: HomM Maybe f g) x.
+     appHomM' h x >>= appSigFunM' a = appHomM' (compSigFunHomM' a h) x;
+
+  "appSigFunM'/appSigFunM'" forall (a :: SigFunM Maybe g h) (h :: SigFunM Maybe f g) x.
+     appSigFunM' h x >>= appSigFunM' a = appSigFunM' (compSigFunM a h) x;
+
+  "appSigFunM/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.
+     appSigFunM a (appHom h x) = appSigFunHomM a (sigFunM h) x;
+
+  "appSigFunM/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
+     appSigFunM a (appSigFun h x) = appSigFunHomM a (sigFunM $ hom h) x;
+
+  "appSigFunM'/appHom" forall (a :: SigFunM m g h) (h :: Hom f g) x.
+     appSigFunM' a (appHom h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;
+
+  "appSigFunM'/appSigFun" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
+     appSigFunM' a (appSigFun h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;
+
+  "appSigFunM/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.
+     appSigFunM a (appHom' h x) = appSigFunHomM a (sigFunM h) x;
+
+  "appSigFunM/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
+     appSigFunM a (appSigFun' h x) = appSigFunHomM a (sigFunM $ hom h) x;
+
+  "appSigFunM'/appHom'" forall (a :: SigFunM m g h) (h :: Hom f g) x.
+     appSigFunM' a (appHom' h x) = appHomM' (compSigFunHomM' a (sigFunM h)) x;
+
+  "appSigFunM'/appSigFun'" forall (a :: SigFunM m g h) (h :: SigFun f g) x.
+     appSigFunM' a (appSigFun' h x) = appSigFunM' (compSigFunM a (sigFunM h)) x;
+
+
+  "appHom/appHomM" forall (a :: Hom g h) (h :: HomM m f g) x.
+     appHomM h x >>= (return . appHom a) = appHomM (compHomM_ a h) x; #-}
+#endif
+-}
diff --git a/src/Data/Comp/Param/Annotation.hs b/src/Data/Comp/Param/Annotation.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Annotation.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.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.Param.Annotation
+    (
+     (:&:) (..),
+     (:*:) (..),
+     DistAnn (..),
+     RemA (..),
+     liftA,
+     liftA',
+     stripA,
+     propAnn,
+     propAnnM,
+     ann,
+     project'
+    ) where
+
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.Term
+import Data.Comp.Param.Sum
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Algebra
+
+import Control.Monad
+
+{-| Transform a function with a domain constructed from a functor to a function
+ with a domain constructed with the same functor, 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 functor to a function
+  with a domain constructed with the same functor, but with an additional
+  annotation. -}
+liftA' :: (DistAnn s' p s, Difunctor s')
+          => (s' a b -> Cxt h s' c d) -> s a b -> Cxt h s c d
+liftA' f v = let (v',p) = projectA v
+             in ann p (f v')
+
+{-| Strip the annotations from a term over a functor with annotations. -}
+stripA :: (RemA g f, Difunctor 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', Difunctor g) 
+        => Hom f g -> Hom f' g'
+propAnn hom f' = ann p (hom f)
+    where (f,p) = projectA f'
+
+{-| Lift a monadic term homomorphism over signatures @f@ and @g@ to a monadic
+  term homomorphism over the same signatures, but extended with annotations. -}
+propAnnM :: (DistAnn f p f', DistAnn g p g', Difunctor g, Monad m) 
+         => HomM m f g -> HomM m f' g'
+propAnnM hom f' = liftM (ann p) (hom f)
+    where (f,p) = projectA f'
+
+{-| Annotate each node of a term with a constant value. -}
+ann :: (DistAnn f p g, Difunctor f)  => p -> CxtFun f g
+ann c = appSigFun (injectA c)
+
+{-| This function is similar to 'project' but applies to signatures
+with an annotation which is then ignored. -}
+project' :: (RemA f f', s :<: f') => Cxt h f a b -> Maybe (s a (Cxt h f a b))
+project' (In x) = proj $ remA x
+project' _ = Nothing
diff --git a/src/Data/Comp/Param/Derive.hs b/src/Data/Comp/Param/Derive.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module contains functionality for automatically deriving boilerplate
+-- code using Template Haskell. Examples include instances of 'Difunctor',
+-- 'Difoldable', and 'Ditraversable'.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive
+    (
+     derive,
+     -- |Derive boilerplate instances for parametric signatures, i.e.
+     -- signatures for parametric compositional data types.
+
+     -- ** EqD
+     module Data.Comp.Param.Derive.Equality,
+     -- ** OrdD
+     module Data.Comp.Param.Derive.Ordering,
+     -- ** ShowD
+     module Data.Comp.Param.Derive.Show,
+     -- ** Difunctor
+     module Data.Comp.Param.Derive.Difunctor,
+     -- ** Ditraversable
+     module Data.Comp.Param.Derive.Ditraversable,
+     -- ** Smart Constructors
+     module Data.Comp.Param.Derive.SmartConstructors,
+     -- ** Smart Constructors w/ Annotations
+     module Data.Comp.Param.Derive.SmartAConstructors,
+     -- ** Lifting to Sums
+     liftSum
+    ) where
+
+import Data.Comp.Derive.Utils (derive, liftSumGen)
+import Data.Comp.Param.Derive.Equality
+import Data.Comp.Param.Derive.Ordering
+import Data.Comp.Param.Derive.Show
+import Data.Comp.Param.Derive.Difunctor
+import Data.Comp.Param.Derive.Ditraversable
+import Data.Comp.Param.Derive.SmartConstructors
+import Data.Comp.Param.Derive.SmartAConstructors
+import Data.Comp.Param.Ops ((:+:), caseD)
+
+import Language.Haskell.TH
+
+{-| Given the name of a type class, where the first parameter is a difunctor,
+  lift it to sums of difunctors. Example: @class ShowD f where ...@ is lifted
+  as @instance (ShowD f, ShowD g) => ShowD (f :+: g) where ... @. -}
+liftSum :: Name -> Q [Dec]
+liftSum = liftSumGen 'caseD ''(:+:)
diff --git a/src/Data/Comp/Param/Derive/Difunctor.hs b/src/Data/Comp/Param/Derive/Difunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Difunctor.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Functor
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @Difunctor@.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive.Difunctor
+    (
+     Difunctor,
+     makeDifunctor
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Difunctor
+import Language.Haskell.TH
+
+{-| Derive an instance of 'Difunctor' for a type constructor of any parametric
+  kind taking at least two arguments. -}
+makeDifunctor :: Name -> Q [Dec]
+makeDifunctor fname = do
+  -- Comments below apply to the example where name = T, args = [a,b,c], and
+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type
+  -- declaration: T a b c = X c | Y a c | Z (b -> c)
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  -- coArg = c (covariant difunctor argument)
+  let coArg :: Name = tyVarBndrName $ last args
+  -- conArg = b (contravariant difunctor argument)
+  let conArg :: Name = tyVarBndrName $ last $ init args
+  -- argNames = [a]
+  let argNames = map (VarT . tyVarBndrName) (init $ init args)
+  -- compType = T a
+  let complType = foldl AppT (ConT name) argNames
+  -- classType = Difunctor (T a)
+  let classType = AppT (ConT ''Difunctor) complType
+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  dimapDecl <- funD 'dimap (map (dimapClause conArg coArg) constrs')
+  return [InstanceD [] classType [dimapDecl]]
+      where dimapClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            dimapClause conArg coArg (constr, args) = do
+              fn <- newName "_f"
+              gn <- newName "_g"
+              varNs <- newNames (length args) "x"
+              let f = varE fn
+              let g = varE gn
+              let fp = VarP fn
+              let gp = VarP gn
+              -- Pattern for the constructor
+              let pat = ConP constr $ map VarP varNs
+              body <- dimapArgs conArg coArg f g (zip varNs args) (conE constr)
+              return $ Clause [fp, gp, pat] (NormalB body) []
+            dimapArgs :: Name -> Name -> ExpQ -> ExpQ
+                      -> [(Name, Type)] -> ExpQ -> ExpQ
+            dimapArgs _ _ _ _ [] acc =
+                acc
+            dimapArgs conArg coArg f g ((x,tp):tps) acc =
+                dimapArgs conArg coArg f g tps
+                          (acc `appE` (dimapArg conArg coArg tp f g `appE` varE x))
+            -- Given the name of the difunctor variables, a type, and the two
+            -- arguments to dimap, return the expression that should be applied
+            -- to the parameter of the given type.
+            -- Example: dimapArg a b (a -> b) f g yields the expression
+            -- [|\x -> g . x . f|]
+            dimapArg :: Name -> Name -> Type -> ExpQ -> ExpQ -> ExpQ
+            dimapArg conArg coArg tp f g
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) = [| id |]
+                | otherwise =
+                    case tp of
+                      VarT a | a == conArg -> f
+                             | a == coArg -> g
+                      AppT (AppT ArrowT tp1) tp2 -> do
+                          xn <- newName "x"
+                          let ftp1 = dimapArg conArg coArg tp1 f g
+                          let ftp2 = dimapArg conArg coArg tp2 f g
+                          lamE [varP xn]
+                               (infixE (Just ftp2)
+                                       [|(.)|]
+                                       (Just $ infixE (Just $ varE xn)
+                                                      [|(.)|]
+                                                      (Just ftp1)))
+                      SigT tp' _ ->
+                          dimapArg conArg coArg tp' f g
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| dimap $f $g |]
+                          else
+                              [| fmap $g |]
diff --git a/src/Data/Comp/Param/Derive/Ditraversable.hs b/src/Data/Comp/Param/Derive/Ditraversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Ditraversable.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Ditraversable
+-- Copyright   :  (c) 2010-2011 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @Ditraversable@.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive.Ditraversable
+    (
+     Ditraversable,
+     makeDitraversable
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Ditraversable
+import Data.Traversable (mapM)
+import Language.Haskell.TH
+import Data.Maybe
+import Control.Monad hiding (mapM)
+import Prelude hiding (mapM)
+
+iter 0 _ e = e
+iter n f e = iter (n-1) f (f `appE` e)
+
+iter' n f e = run n f e
+    where run 0 _ e = e
+          run m f e = let f' = iter (m-1) [|fmap|] f
+                        in run (m-1) f (f' `appE` e)
+
+{-| Derive an instance of 'Traversable' for a type constructor of any
+  first-order kind taking at least one argument. -}
+makeDitraversable :: Name -> Q [Dec]
+makeDitraversable fname = do
+  TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname
+  let fArg = VarT . tyVarBndrName $ last args
+      aArg = VarT . tyVarBndrName $ last (init args)
+      funTy = foldl AppT ArrowT [aArg,fArg]
+      argNames = map (VarT . tyVarBndrName) (init $ init args)
+      complType = foldl AppT (ConT name) argNames
+      classType = foldl1 AppT [ConT ''Ditraversable, complType]
+  normConstrs <- mapM normalConExp constrs
+  constrs' <- mapM (mkPatAndVars . isFarg fArg funTy) normConstrs
+  mapMDecl <- funD 'dimapM (map mapMClause constrs')
+  sequenceDecl <- funD 'disequence (map sequenceClause constrs')
+  return [InstanceD [] classType [mapMDecl,sequenceDecl]]
+      where isFarg fArg funTy (constr, args) =
+                (constr, map (\t -> (t `containsType'` fArg, t `containsType'` funTy)) args)
+            checksAarg aArg (_,args) = any (`containsType` aArg) args
+            filterVar _ _ nonFarg ([],[]) x  = nonFarg x
+            filterVar farg _ _ ([depth],[]) x = farg depth x
+            filterVar _ aarg _ ([_],[depth]) x = aarg depth x
+            filterVar _ _ _ _ _ = error "functor variable occurring twice in argument type"
+            filterVars args varNs farg aarg nonFarg = zipWith (filterVar farg aarg nonFarg) args varNs
+            mkCPat constr varNs = ConP constr $ map mkPat varNs
+            mkPat = VarP
+            mkPatAndVars (constr, args) =
+                do varNs <- newNames (length args) "x"
+                   return (conE constr, mkCPat constr varNs,
+                           any (not . null . fst) args || any (not . null . snd) args, map varE varNs,
+                           catMaybes $ filterVars args varNs (\x y -> Just (False,x,y)) (\x y -> Just (True, x, y)) (const Nothing))
+
+            -- Note: the monadic versions are not defined
+            -- applicatively, as this results in a considerable
+            -- performance penalty (by factor 2)!
+            mapMClause (con, pat,hasFargs,allVars, fvars) =
+                do fn <- newName "f"
+                   let f = varE fn
+                       fp = if hasFargs then VarP fn else WildP
+                       conAp = foldl appE con allVars
+                       addDi False _ x = x
+                       addDi True d x = [|dimapM $(f)|]
+                       conBind (fun,d,x) y = [| $(iter d [|mapM|] (addDi fun d f)) $(varE x)  >>= $(lamE [varP x] y)|]
+                   body <- foldr conBind [|return $conAp|] fvars
+                   return $ Clause [fp, pat] (NormalB body) []
+            sequenceClause (con, pat,hasFargs,allVars, fvars) =
+                do let conAp = foldl appE con allVars
+                       varE' False _ x = varE x
+                       varE' True d x = appE (iter d [|fmap|] [|disequence|]) (varE x)
+                       conBind (fun,d, x) y = [| $(iter' d [|sequence|] (varE' fun d x))  >>= $(lamE [varP x] y)|]
+                   body <- foldr conBind [|return $conAp|] fvars
+                   return $ Clause [pat] (NormalB body) []
diff --git a/src/Data/Comp/Param/Derive/Equality.hs b/src/Data/Comp/Param/Derive/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Equality.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
+  ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Equality
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @EqD@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Derive.Equality
+    (
+     EqD(..),
+     makeEqD
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.FreshM hiding (Name)
+import Data.Comp.Param.Equality
+import Control.Monad
+import Language.Haskell.TH hiding (Cxt, match)
+
+{-| Derive an instance of 'EqD' for a type constructor of any parametric
+  kind taking at least two arguments. -}
+makeEqD :: Name -> Q [Dec]
+makeEqD fname = do
+  -- Comments below apply to the example where name = T, args = [a,b,c], and
+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type
+  -- declaration: T a b c = X c | Y a c | Z (b -> c)
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  -- coArg = c (covariant difunctor argument)
+  let coArg :: Name = tyVarBndrName $ last args
+  -- conArg = b (contravariant difunctor argument)
+  let conArg :: Name = tyVarBndrName $ last $ init args
+  -- argNames = [a]
+  let argNames = map (VarT . tyVarBndrName) (init $ init args)
+  -- compType = T a
+  let complType = foldl AppT (ConT name) argNames
+  -- classType = Difunctor (T a)
+  let classType = AppT (ConT ''EqD) complType
+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  let defC = if length constrs < 2 then
+                 []
+             else
+                 [clause [wildP,wildP] (normalB [|return False|]) []]
+  eqDDecl <- funD 'eqD (map (eqDClause conArg coArg) constrs' ++ defC)
+  let context = map (\arg -> ClassP ''Eq [arg]) argNames
+  return [InstanceD context classType [eqDDecl]]
+      where eqDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            eqDClause conArg coArg (constr, args) = do
+              varXs <- newNames (length args) "x"
+              varYs <- newNames (length args) "y"
+              -- Patterns for the constructors
+              let patx = ConP constr $ map VarP varXs
+              let paty = ConP constr $ map VarP varYs
+              body <- eqDBody conArg coArg (zip3 varXs varYs args)
+              return $ Clause [patx,paty] (NormalB body) []
+            eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ
+            eqDBody conArg coArg x =
+                [|liftM and (sequence $(listE $ map (eqDB conArg coArg) x))|]
+            eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ
+            eqDB conArg coArg (x, y, tp)
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) =
+                    [| return $ $(varE x) == $(varE y) |]
+                | otherwise =
+                    case tp of
+                      VarT a
+                          | a == coArg -> [| peq $(varE x) $(varE y) |]
+                      AppT (AppT ArrowT (VarT a)) _
+                          | a == conArg ->
+                              [| withName (\v -> peq ($(varE x) v) ($(varE y) v)) |]
+                      SigT tp' _ ->
+                          eqDB conArg coArg (x, y, tp')
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| eqD $(varE x) $(varE y) |]
+                          else
+                              [| peq $(varE x) $(varE y) |]
diff --git a/src/Data/Comp/Param/Derive/Injections.hs b/src/Data/Comp/Param/Derive/Injections.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Injections.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Injections
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Derive functions for signature injections.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive.Injections
+    (
+     injn,
+     injectn,
+     deepInjectn
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.Term
+import Data.Comp.Param.Algebra (CxtFun, appSigFun)
+import Data.Comp.Param.Ops ((:+:)(..), (:<:)(..))
+
+injn :: Int -> Q [Dec]
+injn n = do
+  let i = mkName $ "inj" ++ show n
+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
+  let gvar = mkName "g"
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let xvar = mkName "x"
+  let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]
+  sequence $ sigD i (genSig fvars gvar avar bvar) : d
+    where genSig fvars gvar avar bvar = do
+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
+                            (map varT fvars)
+            let tp' = arrowT `appT` (tp `appT` varT avar `appT` varT bvar)
+                             `appT` (varT gvar `appT` varT avar `appT`
+                                     varT bvar)
+            forallT (map PlainTV $ gvar : avar : bvar : fvars)
+                    (sequence cxt) tp'
+          genDecl x n = [| case $(varE x) of
+                             Inl x -> $(varE $ mkName "inj") x
+                             Inr x -> $(varE $ mkName $ "inj" ++
+                                        if n > 2 then show (n - 1) else "") x |]
+injectn :: Int -> Q [Dec]
+injectn n = do
+  let i = mkName ("inject" ++ show n)
+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
+  let gvar = mkName "g"
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let d = [funD i [clause [] (normalB $ genDecl n) []]]
+  sequence $ sigD i (genSig fvars gvar avar bvar) : d
+    where genSig fvars gvar avar bvar = do
+            let hvar = mkName "h"
+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
+                            (map varT fvars)
+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar
+                                 `appT` varT avar `appT` varT bvar
+            let tp'' = arrowT `appT` (tp `appT` varT avar `appT` tp') `appT` tp'
+            forallT (map PlainTV $ hvar : gvar : avar : bvar : fvars)
+                    (sequence cxt) tp''
+          genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]
+
+deepInjectn :: Int -> Q [Dec]
+deepInjectn n = do
+  let i = mkName ("deepInject" ++ show n)
+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
+  let gvar = mkName "g"
+  let d = [funD i [clause [] (normalB $ genDecl n) []]]
+  sequence $ sigD i (genSig fvars gvar) : d
+    where genSig fvars gvar = do
+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
+                            (map varT fvars)
+            let cxt' = classP ''Difunctor [tp]
+            let tp' = conT ''CxtFun `appT` tp `appT` varT gvar
+            forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'
+          genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
diff --git a/src/Data/Comp/Param/Derive/Ordering.hs b/src/Data/Comp/Param/Derive/Ordering.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Ordering.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
+  ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Ordering
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @OrdD@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Derive.Ordering
+    (
+     OrdD(..),
+     makeOrdD
+    ) where
+
+import Data.Comp.Param.FreshM hiding (Name)
+import Data.Comp.Param.Ordering
+import Data.Comp.Derive.Utils
+import Language.Haskell.TH hiding (Cxt)
+import Control.Monad (liftM)
+
+{-| Derive an instance of 'OrdD' for a type constructor of any parametric
+  kind taking at least two arguments. -}
+makeOrdD :: Name -> Q [Dec]
+makeOrdD fname = do
+  -- Comments below apply to the example where name = T, args = [a,b,c], and
+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type
+  -- declaration: T a b c = X c | Y a c | Z (b -> c)
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  -- coArg = c (covariant difunctor argument)
+  let coArg :: Name = tyVarBndrName $ last args
+  -- conArg = b (contravariant difunctor argument)
+  let conArg :: Name = tyVarBndrName $ last $ init args
+  -- argNames = [a]
+  let argNames = map (VarT . tyVarBndrName) (init $ init args)
+  -- compType = T a
+  let complType = foldl AppT (ConT name) argNames
+  -- classType = Difunctor (T a)
+  let classType = AppT (ConT ''OrdD) complType
+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  compareDDecl <- funD 'compareD (compareDClauses conArg coArg constrs')
+  let context = map (\arg -> ClassP ''Ord [arg]) argNames
+  return [InstanceD context classType [compareDDecl]]
+      where compareDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]
+            compareDClauses _ _ [] = []
+            compareDClauses conArg coArg constrs = 
+                let constrs' = constrs `zip` [1..]
+                    constPairs = [(x,y)| x<-constrs', y <- constrs']
+                in map (genClause conArg coArg) constPairs
+            genClause conArg coArg ((c,n),(d,m))
+                | n == m = genEqClause conArg coArg c
+                | n < m = genLtClause c d
+                | otherwise = genGtClause c d
+            genEqClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            genEqClause conArg coArg (constr, args) = do 
+              varXs <- newNames (length args) "x"
+              varYs <- newNames (length args) "y"
+              let patX = ConP constr $ map VarP varXs
+              let patY = ConP constr $ map VarP varYs
+              body <- eqDBody conArg coArg (zip3 varXs varYs args)
+              return $ Clause [patX, patY] (NormalB body) []
+            eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ
+            eqDBody conArg coArg x =
+                [|liftM compList (sequence $(listE $ map (eqDB conArg coArg) x))|]
+            eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ
+            eqDB conArg coArg (x, y, tp)
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) =
+                    [| return $ compare $(varE x) $(varE y) |]
+                | otherwise =
+                    case tp of
+                      VarT a
+                          | a == coArg -> [| pcompare $(varE x) $(varE y) |]
+                      AppT (AppT ArrowT (VarT a)) _
+                          | a == conArg ->
+                              [| withName (\v -> pcompare ($(varE x) v) ($(varE y) v)) |]
+                      SigT tp' _ ->
+                          eqDB conArg coArg (x, y, tp')
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| compareD $(varE x) $(varE y) |]
+                          else
+                              [| pcompare $(varE x) $(varE y) |]
+            genLtClause (c, _) (d, _) =
+                clause [recP c [], recP d []] (normalB [| return LT |]) []
+            genGtClause (c, _) (d, _) =
+                clause [recP c [], recP d []] (normalB [| return GT |]) []
diff --git a/src/Data/Comp/Param/Derive/Projections.hs b/src/Data/Comp/Param/Derive/Projections.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Projections.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE TemplateHaskell, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Projections
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Derive functions for signature projections.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive.Projections
+    (
+     projn,
+     projectn,
+     deepProjectn
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Control.Monad (liftM)
+import Data.Comp.Param.Ditraversable (Ditraversable)
+import Data.Comp.Param.Term
+import Data.Comp.Param.Algebra (appTSigFunM')
+import Data.Comp.Param.Ops ((:+:)(..), (:<:)(..))
+
+projn :: Int -> Q [Dec]
+projn n = do
+  let p = mkName $ "proj" ++ show n
+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let xvar = mkName "x"
+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar bvar) []]]
+  sequence $ (sigD p $ genSig gvars avar bvar) : d
+    where genSig gvars avar bvar = do
+            let fvar = mkName "f"
+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
+                            (map varT gvars)
+            let tp' = arrowT `appT` (varT fvar `appT` varT avar `appT`
+                                     varT bvar)
+                             `appT` (conT ''Maybe `appT`
+                                     (tp `appT` varT avar `appT` varT bvar))
+            forallT (map PlainTV $ fvar : avar : bvar : gvars)
+                    (sequence cxt) tp'
+          genDecl x [g] a b =
+            [| liftM inj (proj $(varE x)
+                          :: Maybe ($(varT g `appT` varT a `appT` varT b))) |]
+          genDecl x (g:gs) a b =
+            [| case (proj $(varE x)
+                         :: Maybe ($(varT g `appT` varT a `appT` varT b))) of
+                 Just y -> Just $ inj y
+                 _ -> $(genDecl x gs a b) |]
+          genDecl _ _ _ _ = error "genDecl called with empty list"
+
+projectn :: Int -> Q [Dec]
+projectn n = do
+  let p = mkName ("project" ++ show n)
+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let xvar = mkName "x"
+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]
+  sequence $ (sigD p $ genSig gvars avar bvar) : d
+    where genSig gvars avar bvar = do
+            let fvar = mkName "f"
+            let hvar = mkName "h"
+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
+                            (map varT gvars)
+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar
+                                 `appT` varT avar `appT` varT bvar
+            let tp'' = arrowT `appT` tp'
+                              `appT` (conT ''Maybe `appT`
+                                      (tp `appT` varT avar `appT` tp'))
+            forallT (map PlainTV $ hvar : fvar : avar : bvar : gvars)
+                    (sequence cxt) tp''
+          genDecl x n = [| case $(varE x) of
+                             Hole _ -> Nothing
+                             Var _ -> Nothing
+                             In t -> $(varE $ mkName $ "proj" ++ show n) t |]
+
+deepProjectn :: Int -> Q [Dec]
+deepProjectn n = do
+  let p = mkName ("deepProject" ++ show n)
+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
+  let d = [funD p [clause [] (normalB $ genDecl n) []]]
+  sequence $ (sigD p $ genSig gvars) : d
+    where genSig gvars = do
+            let fvar = mkName "f"
+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
+                            (map varT gvars)
+            let cxt' = classP ''Ditraversable [tp]
+            let tp' = arrowT `appT` (conT ''Term `appT` varT fvar)
+                             `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp))
+            forallT (map PlainTV $ fvar : gvars) (sequence $ cxt' : cxt) tp'
+          genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
diff --git a/src/Data/Comp/Param/Derive/Show.hs b/src/Data/Comp/Param/Derive/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/Show.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
+  ScopedTypeVariables, UndecidableInstances #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.Show
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @ShowD@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Derive.Show
+    (
+     ShowD(..),
+     makeShowD
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.FreshM hiding (Name)
+import qualified Data.Comp.Param.FreshM as FreshM
+import Control.Monad
+import Language.Haskell.TH hiding (Cxt, match)
+import qualified Data.Traversable as T
+
+{-| Signature printing. An instance @ShowD f@ gives rise to an instance
+  @Show (Term f)@. -}
+class ShowD f where
+    showD :: f FreshM.Name (FreshM String) -> FreshM String
+
+newtype Dummy = Dummy String
+
+instance Show Dummy where
+  show (Dummy s) = s
+
+{-| Derive an instance of 'ShowD' for a type constructor of any parametric
+  kind taking at least two arguments. -}
+makeShowD :: Name -> Q [Dec]
+makeShowD fname = do
+  -- Comments below apply to the example where name = T, args = [a,b,c], and
+  -- constrs = [(X,[c]), (Y,[a,c]), (Z,[b -> c])], i.e. the data type
+  -- declaration: T a b c = X c | Y a c | Z (b -> c)
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  -- coArg = c (covariant difunctor argument)
+  let coArg :: Name = tyVarBndrName $ last args
+  -- conArg = b (contravariant difunctor argument)
+  let conArg :: Name = tyVarBndrName $ last $ init args
+  -- argNames = [a]
+  let argNames = map (VarT . tyVarBndrName) (init $ init args)
+  -- compType = T a
+  let complType = foldl AppT (ConT name) argNames
+  -- classType = Difunctor (T a)
+  let classType = AppT (ConT ''ShowD) complType
+  -- constrs' = [(X,[c]), (Y,[a,c]), (Z,[b -> c])]
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  showDDecl <- funD 'showD (map (showDClause conArg coArg) constrs')
+  let context = map (\arg -> ClassP ''Show [arg]) argNames
+  return [InstanceD context classType [showDDecl]]
+      where showDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            showDClause conArg coArg (constr, args) = do
+              varXs <- newNames (length args) "x"
+              -- Pattern for the constructor
+              let patx = ConP constr $ map VarP varXs
+              body <- showDBody (nameBase constr) conArg coArg (zip varXs args)
+              return $ Clause [patx] (NormalB body) []
+            showDBody :: String -> Name -> Name -> [(Name, Type)] -> ExpQ
+            showDBody constr conArg coArg x =
+                [|liftM (unwords . (constr :) .
+                         map (\x -> if elem ' ' x then "(" ++ x ++ ")" else x))
+                        (sequence $(listE $ map (showDB conArg coArg) x))|]
+            showDB :: Name -> Name -> (Name, Type) -> ExpQ
+            showDB conArg coArg (x, tp)
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) =
+                    [| return $ show $(varE x) |]
+                | otherwise =
+                    case tp of
+                      VarT a
+                          | a == coArg -> [| $(varE x) |]
+                      AppT (AppT ArrowT (VarT a)) _
+                          | a == conArg ->
+                              [| withName (\v -> do body <- $(varE x) v;
+                                                    return $ "\\" ++ show v ++ " -> " ++ body) |]
+                      SigT tp' _ ->
+                          showDB conArg coArg (x, tp')
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| showD $(varE x) |]
+                          else
+                              [| liftM show $ T.mapM (liftM Dummy) $(varE x) |]
diff --git a/src/Data/Comp/Param/Derive/SmartAConstructors.hs b/src/Data/Comp/Param/Derive/SmartAConstructors.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/SmartAConstructors.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.SmartAConstructors
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive smart constructors with annotations for difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive.SmartAConstructors 
+    (
+     smartAConstructors
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Term
+import Data.Comp.Param.Difunctor
+
+import Control.Monad
+
+{-| Derive smart constructors with annotations for a difunctor. The smart
+ constructors are similar to the ordinary constructors, but a
+ 'injectA . dimap Var id' is automatically inserted. -}
+smartAConstructors :: Name -> Q [Dec]
+smartAConstructors fname = do
+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
+    let cons = map abstractConType constrs
+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
+        where genSmartConstr targs tname (name, args) = do
+                let bname = nameBase name
+                genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args
+              genSmartConstr' targs tname sname name args = do
+                varNs <- newNames args "x"
+                varPr <- newName "_p"
+                let pats = map varP (varPr : varNs)
+                    vars = map varE varNs
+                    val = appE [|injectA $(varE varPr)|] $
+                          appE [|inj . dimap Var id|] $ foldl appE (conE name) vars
+                    function = [funD sname [clause pats (normalB [|In $val|]) []]]
+                sequence function
diff --git a/src/Data/Comp/Param/Derive/SmartConstructors.hs b/src/Data/Comp/Param/Derive/SmartConstructors.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Derive/SmartConstructors.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Derive.SmartConstructors
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive smart constructors for difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Derive.SmartConstructors 
+    (
+     smartConstructors
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Sum
+import Data.Comp.Param.Term
+import Data.Comp.Param.Difunctor
+import Control.Monad
+
+{-| Derive smart constructors for a difunctor. The smart constructors are
+ similar to the ordinary constructors, but a 'inject . dimap Var id' is
+ automatically inserted. -}
+smartConstructors :: Name -> Q [Dec]
+smartConstructors fname = do
+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
+    let cons = map abstractConType constrs
+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
+        where genSmartConstr targs tname (name, args) = do
+                let bname = nameBase name
+                genSmartConstr' targs tname (mkName $ 'i' : bname) name args
+              genSmartConstr' targs tname sname name args = do
+                varNs <- newNames args "x"
+                let pats = map varP varNs
+                    vars = map varE varNs
+                    val = foldl appE (conE name) vars
+                    sig = genSig targs tname sname args
+                    function = [funD sname [clause pats (normalB [|inject (dimap Var id $val)|]) []]]
+                sequence $ sig ++ function
+              genSig targs tname sname 0 = (:[]) $ do
+                hvar <- newName "h"
+                fvar <- newName "f"
+                avar <- newName "a"
+                bvar <- newName "b"
+                let targs' = init $ init targs
+                    vars = hvar:fvar:avar:bvar:targs'
+                    h = varT hvar
+                    f = varT fvar
+                    a = varT avar
+                    b = varT bvar
+                    ftype = foldl appT (conT tname) (map varT targs')
+                    constr = classP ''(:<:) [ftype, f]
+                    typ = foldl appT (conT ''Cxt) [h, f, a, b]
+                    typeSig = forallT (map PlainTV vars) (sequence [constr]) typ
+                sigD sname typeSig
+              genSig _ _ _ _ = []
diff --git a/src/Data/Comp/Param/Desugar.hs b/src/Data/Comp/Param/Desugar.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Desugar.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,
+  UndecidableInstances, OverlappingInstances, Rank2Types, TypeOperators #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Desugar
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This modules defines the 'Desugar' type class for desugaring of terms.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Desugar where
+
+import Data.Comp.Param
+
+
+-- |The desugaring term homomorphism.
+class (Difunctor f, Difunctor g) => Desugar f g where
+    desugHom :: Hom f g
+    desugHom = desugHom' . fmap Hole
+    desugHom' :: f a (Cxt h g a b) -> Cxt h g a b
+    desugHom' x = appCxt (desugHom x)
+
+-- We make the lifting to sums explicit in order to make the Desugar
+-- class work with the default instance declaration further below.
+instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
+    desugHom = caseD desugHom desugHom
+
+-- |Desugar a term.
+desugar :: Desugar f g => Term f -> Term g
+{-# INLINE desugar #-}
+desugar (Term t) = Term (appHom desugHom t)
+
+-- |Lift desugaring to annotated terms.
+desugarA :: (Difunctor f', Difunctor g', DistAnn f p f', DistAnn g p g',
+             Desugar f g) => Term f' -> Term g'
+desugarA (Term t) = Term (appHom (propAnn desugHom) t)
+
+-- |Default desugaring instance.
+instance (Difunctor f, Difunctor g, f :<: g) => Desugar f g where
+    desugHom = simpCxt . inj
diff --git a/src/Data/Comp/Param/Difunctor.hs b/src/Data/Comp/Param/Difunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Difunctor.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Difunctor
+-- 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 difunctors (Meijer, Hutton, FPCA '95), i.e. binary type
+-- constructors that are contravariant in the first argument and covariant in
+-- the second argument.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Difunctor
+    (
+      difmap,
+     Difunctor(..)
+    ) where
+
+-- | This class represents difunctors, i.e. binary type constructors that are
+-- contravariant in the first argument and covariant in the second argument.
+class Difunctor f where
+    dimap :: (a -> b) -> (c -> d) -> f b c -> f a d
+
+{-| The canonical example of a difunctor. -}
+instance Difunctor (->) where
+    dimap f g h = g . h . f
+
+difmap :: Difunctor f => (a -> b) -> f c a -> f c b
+difmap = dimap id
+
+instance Difunctor f => Functor (f a) where
+    fmap = difmap
diff --git a/src/Data/Comp/Param/Ditraversable.hs b/src/Data/Comp/Param/Ditraversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Ditraversable.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Ditraversable
+-- 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 traversable difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Ditraversable
+    (
+     Ditraversable(..)
+    ) where
+
+import Data.Comp.Param.Difunctor
+
+{-| Difunctors representing data structures that can be traversed from left to
+  right. -}
+class Difunctor f => Ditraversable f where
+    dimapM :: Monad m => (b -> m c) -> f a b -> m (f a c)
+    dimapM f = disequence . fmap f
+    disequence :: Monad m => f a (m b) -> m (f a b)
+    disequence = dimapM id
diff --git a/src/Data/Comp/Param/Equality.hs b/src/Data/Comp/Param/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Equality.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
+  UndecidableInstances, IncoherentInstances, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Equality
+-- 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 equality for signatures, which lifts to equality for
+-- terms.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Equality
+    (
+     PEq(..),
+     EqD(..)
+    ) where
+
+import Data.Comp.Param.Term
+import Data.Comp.Param.Sum
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.FreshM
+import Control.Monad (liftM)
+
+-- |Equality on parametric values. The equality test is performed inside the
+-- 'FreshM' monad for generating fresh identifiers.
+class PEq a where
+    peq :: a -> a -> FreshM Bool
+
+instance PEq a => PEq [a] where
+    peq l1 l2
+        | length l1 /= length l2 = return False
+        | otherwise = liftM or $ mapM (uncurry peq) $ zip l1 l2
+
+instance Eq a => PEq a where
+    peq x y = return $ x == y
+
+{-| Signature equality. An instance @EqD f@ gives rise to an instance
+  @Eq (Term f)@. The equality test is performed inside the 'FreshM' monad for
+  generating fresh identifiers. -}
+class EqD f where
+    eqD :: PEq a => f Name a -> f Name a -> FreshM Bool
+
+{-| 'EqD' is propagated through sums. -}
+instance (EqD f, EqD g) => EqD (f :+: g) where
+    eqD (Inl x) (Inl y) = eqD x y
+    eqD (Inr x) (Inr y) = eqD x y
+    eqD _ _ = return False
+
+{-| From an 'EqD' difunctor an 'Eq' instance of the corresponding term type can
+  be derived. -}
+instance EqD f => EqD (Cxt h f) where
+    eqD (In e1) (In e2) = eqD e1 e2
+    eqD (Hole h1) (Hole h2) = peq h1 h2
+    eqD (Var p1) (Var p2) = peq p1 p2
+    eqD _ _ = return False
+
+instance (EqD f, PEq a) => PEq (Cxt h f Name a) where
+    peq = eqD
+
+{-| Equality on terms. -}
+instance (Difunctor f, EqD f) => Eq (Term f) where
+    (==) (Term x) (Term y) = evalFreshM $ eqD x y
diff --git a/src/Data/Comp/Param/FreshM.hs b/src/Data/Comp/Param/FreshM.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/FreshM.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.FreshM
+-- 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 a monad for generating fresh, abstract names, useful
+-- e.g. for defining equality on terms.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.FreshM
+    (
+     FreshM,
+     Name,
+     withName,
+     evalFreshM
+    ) where
+
+import Control.Monad.Reader
+import Control.Applicative
+
+-- |Monad for generating fresh (abstract) names.
+newtype FreshM a = FreshM{unFreshM :: Reader Int a}
+    deriving (Monad, Applicative,Functor)
+
+-- |Abstract notion of a name (the constructor is hidden).
+newtype Name = Name Int
+    deriving Eq
+
+instance Show Name where
+    show (Name x) = names !! x
+        where baseNames = ['a'..'z']
+              names = map (:[]) baseNames ++ names' 1
+              names' n = map (: show n) baseNames ++ names' (n + 1)
+
+instance Ord Name where
+    compare (Name x) (Name y) = compare x y
+
+-- |Run the given computation with the next available name.
+withName :: (Name -> FreshM a) -> FreshM a
+withName m = do name <- FreshM (asks Name)
+                FreshM $ local ((+) 1) $ unFreshM $ m name
+
+-- |Evaluate a computation that uses fresh names.
+evalFreshM :: FreshM a -> a
+evalFreshM (FreshM m) = runReader m 0
diff --git a/src/Data/Comp/Param/Multi.hs b/src/Data/Comp/Param/Multi.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi.hs
@@ -0,0 +1,34 @@
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi
+-- 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\/Param.Multi@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi (
+    module Data.Comp.Param.Multi.Term
+  , module Data.Comp.Param.Multi.Algebra
+  , module Data.Comp.Param.Multi.HDifunctor
+  , module Data.Comp.Param.Multi.Sum
+  , module Data.Comp.Param.Multi.Annotation
+  , module Data.Comp.Param.Multi.Equality
+    ) where
+
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Algebra
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.Sum
+import Data.Comp.Param.Multi.Annotation
+import Data.Comp.Param.Multi.Equality
diff --git a/src/Data/Comp/Param/Multi/Algebra.hs b/src/Data/Comp/Param/Multi/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Algebra.hs
@@ -0,0 +1,346 @@
+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
+  FlexibleContexts, CPP, KindSignatures #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.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.Param.Multi.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.Param.Multi.Term
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.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
+-}
diff --git a/src/Data/Comp/Param/Multi/Annotation.hs b/src/Data/Comp/Param/Multi/Annotation.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Annotation.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.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.Param.Multi.Annotation
+    (
+     (:&:) (..),
+     (:*:) (..),
+     DistAnn (..),
+     RemA (..),
+     liftA,
+     liftA',
+     stripA,
+     propAnn,
+     propAnnM,
+     ann,
+     project'
+    ) where
+
+import qualified Data.Comp.Ops as O
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Sum
+import Data.Comp.Param.Multi.Ops
+import Data.Comp.Param.Multi.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
+  term homomorphism over the same signatures, but extended with annotations. -}
+propAnnM :: (DistAnn f p f', DistAnn g p g', HDifunctor g, Monad m)
+         => HomM m f g -> HomM m f' g'
+propAnnM hom f' = liftM (ann p) (hom f)
+    where f O.:&: p = projectA f'
+
+{-| Annotate each node of a term with a constant value. -}
+ann :: (DistAnn f p g, HDifunctor f) => p -> CxtFun f g
+ann c = appSigFun (injectA c)
+
+{-| This function is similar to 'project' but applies to signatures
+  with an annotation which is then ignored. -}
+project' :: (RemA f f', s :<: f') => Cxt h f a b i -> Maybe (s a (Cxt h f a b) i)
+project' (In x) = proj $ remA x
+project' _ = Nothing
diff --git a/src/Data/Comp/Param/Multi/Derive.hs b/src/Data/Comp/Param/Multi/Derive.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module contains functionality for automatically deriving boilerplate
+-- code using Template Haskell. Examples include instances of 'HDifunctor',
+-- 'ShowHD', and 'EqHD'.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Derive
+    (
+     derive,
+     -- |Derive boilerplate instances for parametric signatures, i.e.
+     -- signatures for parametric compositional data types.
+
+     -- ** EqHD
+     module Data.Comp.Param.Multi.Derive.Equality,
+     -- ** OrdHD
+     module Data.Comp.Param.Multi.Derive.Ordering,
+     -- ** ShowHD
+     module Data.Comp.Param.Multi.Derive.Show,
+     -- ** HDifunctor
+     module Data.Comp.Param.Multi.Derive.HDifunctor,
+     -- ** Smart Constructors
+     module Data.Comp.Param.Multi.Derive.SmartConstructors,
+     -- ** Smart Constructors w/ Annotations
+     module Data.Comp.Param.Multi.Derive.SmartAConstructors,
+     -- ** Lifting to Sums
+     liftSum
+    ) where
+
+import Data.Comp.Derive.Utils (derive, liftSumGen)
+import Data.Comp.Param.Multi.Derive.Equality
+import Data.Comp.Param.Multi.Derive.Ordering
+import Data.Comp.Param.Multi.Derive.Show
+import Data.Comp.Param.Multi.Derive.HDifunctor
+import Data.Comp.Param.Multi.Derive.SmartConstructors
+import Data.Comp.Param.Multi.Derive.SmartAConstructors
+import Data.Comp.Param.Multi.Ops ((:+:), caseHD)
+
+import Language.Haskell.TH
+
+{-| Given the name of a type class, where the first parameter is a higher-order
+  difunctor, lift it to sums of higher-order difunctors. Example:
+  @class ShowHD f where ...@ is lifted as
+  @instance (ShowHD f, ShowHD g) => ShowHD (f :+: g) where ... @. -}
+liftSum :: Name -> Q [Dec]
+liftSum = liftSumGen 'caseHD ''(:+:)
diff --git a/src/Data/Comp/Param/Multi/Derive/Equality.hs b/src/Data/Comp/Param/Multi/Derive/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/Equality.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
+  ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.Equality
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @EqHD@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.Derive.Equality
+    (
+     EqHD(..),
+     makeEqHD
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Multi.FreshM hiding (Name)
+import Data.Comp.Param.Multi.Equality
+import Control.Monad
+import Language.Haskell.TH hiding (Cxt, match)
+
+{-| Derive an instance of 'EqHD' for a type constructor of any parametric
+  kind taking at least three arguments. -}
+makeEqHD :: Name -> Q [Dec]
+makeEqHD fname = do
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  let args' = init args
+  -- covariant argument
+  let coArg :: Name = tyVarBndrName $ last args'
+  -- contravariant argument
+  let conArg :: Name = tyVarBndrName $ last $ init args'
+  let argNames = map (VarT . tyVarBndrName) (init $ init args')
+  let complType = foldl AppT (ConT name) argNames
+  let classType = AppT (ConT ''EqHD) complType
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  let defC = if length constrs < 2 then
+                 []
+             else
+                 [clause [wildP,wildP] (normalB [|return False|]) []]
+  eqHDDecl <- funD 'eqHD (map (eqHDClause conArg coArg) constrs' ++ defC)
+  let context = map (\arg -> ClassP ''Eq [arg]) argNames
+  return [InstanceD context classType [eqHDDecl]]
+      where eqHDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            eqHDClause conArg coArg (constr, args) = do
+              varXs <- newNames (length args) "x"
+              varYs <- newNames (length args) "y"
+              -- Patterns for the constructors
+              let patx = ConP constr $ map VarP varXs
+              let paty = ConP constr $ map VarP varYs
+              body <- eqHDBody conArg coArg (zip3 varXs varYs args)
+              return $ Clause [patx,paty] (NormalB body) []
+            eqHDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ
+            eqHDBody conArg coArg x =
+                [|liftM and (sequence $(listE $ map (eqHDB conArg coArg) x))|]
+            eqHDB :: Name -> Name -> (Name, Name, Type) -> ExpQ
+            eqHDB conArg coArg (x, y, tp)
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) =
+                    [| return $ $(varE x) == $(varE y) |]
+                | otherwise =
+                    case tp of
+                      AppT (VarT a) _ 
+                          | a == coArg -> [| peq $(varE x) $(varE y) |]
+                      AppT (AppT ArrowT (AppT (VarT a) _)) _
+                          | a == conArg ->
+                              [| withName (\v -> peq ($(varE x) $ nameCoerce v)                                                      ($(varE y) $ nameCoerce v)) |]
+                      SigT tp' _ ->
+                          eqHDB conArg coArg (x, y, tp')
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| eqHD $(varE x) $(varE y) |]
+                          else
+                              [| peq $(varE x) $(varE y) |]
diff --git a/src/Data/Comp/Param/Multi/Derive/HDifunctor.hs b/src/Data/Comp/Param/Multi/Derive/HDifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/HDifunctor.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.HDifunctor
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @HDifunctor@.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Derive.HDifunctor
+    (
+     HDifunctor,
+     makeHDifunctor
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Multi.HDifunctor
+import Language.Haskell.TH
+
+{-| Derive an instance of 'HDifunctor' for a type constructor of any parametric
+  kind taking at least three arguments. -}
+makeHDifunctor :: Name -> Q [Dec]
+makeHDifunctor fname = do
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  let args' = init args
+  -- covariant argument
+  let coArg :: Name = tyVarBndrName $ last args'
+  -- contravariant argument
+  let conArg :: Name = tyVarBndrName $ last $ init args'
+  let argNames = map (VarT . tyVarBndrName) (init $ init args')
+  let complType = foldl AppT (ConT name) argNames
+  let classType = AppT (ConT ''HDifunctor) complType
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  hdimapDecl <- funD 'hdimap (map (hdimapClause conArg coArg) constrs')
+  return [InstanceD [] classType [hdimapDecl]]
+      where hdimapClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            hdimapClause conArg coArg (constr, args) = do
+              fn <- newName "_f"
+              gn <- newName "_g"
+              varNs <- newNames (length args) "x"
+              let f = varE fn
+              let g = varE gn
+              let fp = VarP fn
+              let gp = VarP gn
+              -- Pattern for the constructor
+              let pat = ConP constr $ map VarP varNs
+              body <- hdimapArgs conArg coArg f g (zip varNs args) (conE constr)
+              return $ Clause [fp, gp, pat] (NormalB body) []
+            hdimapArgs :: Name -> Name -> ExpQ -> ExpQ
+                      -> [(Name, Type)] -> ExpQ -> ExpQ
+            hdimapArgs _ _ _ _ [] acc =
+                acc
+            hdimapArgs conArg coArg f g ((x,tp):tps) acc =
+                hdimapArgs conArg coArg f g tps
+                          (acc `appE` (hdimapArg conArg coArg tp f g `appE` varE x))
+            hdimapArg :: Name -> Name -> Type -> ExpQ -> ExpQ -> ExpQ
+            hdimapArg conArg coArg tp f g
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) = [| id |]
+                | otherwise =
+                    case tp of
+                      AppT (VarT a) _ | a == conArg -> f
+                                      | a == coArg -> g
+                      AppT (AppT ArrowT tp1) tp2 -> do
+                          xn <- newName "x"
+                          let ftp1 = hdimapArg conArg coArg tp1 f g
+                          let ftp2 = hdimapArg conArg coArg tp2 f g
+                          lamE [varP xn]
+                               (infixE (Just ftp2)
+                                       [|(.)|]
+                                       (Just $ infixE (Just $ varE xn)
+                                                      [|(.)|]
+                                                      (Just ftp1)))
+                      SigT tp' _ ->
+                          hdimapArg conArg coArg tp' f g
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| hdimap $f $g |]
+                          else
+                              [| fmap $g |]
diff --git a/src/Data/Comp/Param/Multi/Derive/Injections.hs b/src/Data/Comp/Param/Multi/Derive/Injections.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/Injections.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.Injections
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Derive functions for signature injections.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Derive.Injections
+    (
+     injn,
+     injectn,
+     deepInjectn
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Algebra (CxtFun, appSigFun)
+import Data.Comp.Param.Multi.Ops ((:+:)(..), (:<:)(..))
+
+injn :: Int -> Q [Dec]
+injn n = do
+  let i = mkName $ "inj" ++ show n
+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
+  let gvar = mkName "g"
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let ivar = mkName "i"
+  let xvar = mkName "x"
+  let d = [funD i [clause [varP xvar] (normalB $ genDecl xvar n) []]]
+  sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d
+    where genSig fvars gvar avar bvar ivar = do
+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
+                            (map varT fvars)
+            let tp' = arrowT `appT` (tp `appT` varT avar `appT`
+                                     varT bvar `appT` varT ivar)
+                             `appT` (varT gvar `appT` varT avar `appT`
+                                     varT bvar `appT` varT ivar)
+            forallT (map PlainTV $ gvar : avar : bvar : ivar : fvars)
+                    (sequence cxt) tp'
+          genDecl x n = [| case $(varE x) of
+                             Inl x -> $(varE $ mkName "inj") x
+                             Inr x -> $(varE $ mkName $ "inj" ++
+                                        if n > 2 then show (n - 1) else "") x |]
+injectn :: Int -> Q [Dec]
+injectn n = do
+  let i = mkName ("inject" ++ show n)
+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
+  let gvar = mkName "g"
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let ivar = mkName "i"
+  let d = [funD i [clause [] (normalB $ genDecl n) []]]
+  sequence $ sigD i (genSig fvars gvar avar bvar ivar) : d
+    where genSig fvars gvar avar bvar ivar = do
+            let hvar = mkName "h"
+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
+                            (map varT fvars)
+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT gvar
+                                 `appT` varT avar `appT` varT bvar
+            let tp'' = arrowT `appT` (tp `appT` varT avar `appT`
+                                      tp' `appT` varT ivar)
+                              `appT` (tp' `appT` varT ivar)
+            forallT (map PlainTV $ hvar : gvar : avar : bvar : ivar : fvars)
+                    (sequence cxt) tp''
+          genDecl n = [| In . $(varE $ mkName $ "inj" ++ show n) |]
+
+deepInjectn :: Int -> Q [Dec]
+deepInjectn n = do
+  let i = mkName ("deepInject" ++ show n)
+  let fvars = map (\n -> mkName $ 'f' : show n) [1..n]
+  let gvar = mkName "g"
+  let d = [funD i [clause [] (normalB $ genDecl n) []]]
+  sequence $ sigD i (genSig fvars gvar) : d
+    where genSig fvars gvar = do
+            let cxt = map (\f -> classP ''(:<:) [varT f, varT gvar]) fvars
+            let tp = foldl1 (\a f -> conT ''(:+:) `appT` f `appT` a)
+                            (map varT fvars)
+            let cxt' = classP ''HDifunctor [tp]
+            let tp' = conT ''CxtFun `appT` tp `appT` varT gvar
+            forallT (map PlainTV $ gvar : fvars) (sequence $ cxt' : cxt) tp'
+          genDecl n = [| appSigFun $(varE $ mkName $ "inj" ++ show n) |]
diff --git a/src/Data/Comp/Param/Multi/Derive/Ordering.hs b/src/Data/Comp/Param/Multi/Derive/Ordering.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/Ordering.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
+  ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.Ordering
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @OrdHD@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.Derive.Ordering
+    (
+     OrdHD(..),
+     makeOrdHD
+    ) where
+
+import Data.Comp.Param.Multi.FreshM hiding (Name)
+import Data.Comp.Param.Multi.Ordering
+import Data.Comp.Derive.Utils
+import Data.Maybe
+import Data.List
+import Language.Haskell.TH hiding (Cxt)
+import Control.Monad (liftM)
+
+compList :: [Ordering] -> Ordering
+compList = fromMaybe EQ . find (/= EQ)
+
+{-| Derive an instance of 'OrdHD' for a type constructor of any parametric
+  kind taking at least three arguments. -}
+makeOrdHD :: Name -> Q [Dec]
+makeOrdHD fname = do
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  let args' = init args
+  -- covariant argument
+  let coArg :: Name = tyVarBndrName $ last args'
+  -- contravariant argument
+  let conArg :: Name = tyVarBndrName $ last $ init args'
+  let argNames = map (VarT . tyVarBndrName) (init $ init args')
+  let complType = foldl AppT (ConT name) argNames
+  let classType = AppT (ConT ''OrdHD) complType
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  compareHDDecl <- funD 'compareHD (compareHDClauses conArg coArg constrs')
+  let context = map (\arg -> ClassP ''Ord [arg]) argNames
+  return [InstanceD context classType [compareHDDecl]]
+      where compareHDClauses :: Name -> Name -> [(Name,[Type])] -> [ClauseQ]
+            compareHDClauses _ _ [] = []
+            compareHDClauses conArg coArg constrs = 
+                let constrs' = constrs `zip` [1..]
+                    constPairs = [(x,y)| x<-constrs', y <- constrs']
+                in map (genClause conArg coArg) constPairs
+            genClause conArg coArg ((c,n),(d,m))
+                | n == m = genEqClause conArg coArg c
+                | n < m = genLtClause c d
+                | otherwise = genGtClause c d
+            genEqClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            genEqClause conArg coArg (constr, args) = do 
+              varXs <- newNames (length args) "x"
+              varYs <- newNames (length args) "y"
+              let patX = ConP constr $ map VarP varXs
+              let patY = ConP constr $ map VarP varYs
+              body <- eqDBody conArg coArg (zip3 varXs varYs args)
+              return $ Clause [patX, patY] (NormalB body) []
+            eqDBody :: Name -> Name -> [(Name, Name, Type)] -> ExpQ
+            eqDBody conArg coArg x =
+                [|liftM compList (sequence $(listE $ map (eqDB conArg coArg) x))|]
+            eqDB :: Name -> Name -> (Name, Name, Type) -> ExpQ
+            eqDB conArg coArg (x, y, tp)
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) =
+                    [| return $ compare $(varE x) $(varE y) |]
+                | otherwise =
+                    case tp of
+                      AppT (VarT a) _ 
+                          | a == coArg -> [| pcompare $(varE x) $(varE y) |]
+                      AppT (AppT ArrowT (AppT (VarT a) _)) _
+                          | a == conArg ->
+                              [| withName (\v -> pcompare ($(varE x) $ nameCoerce v)
+                                                          ($(varE y) $ nameCoerce v)) |]
+                      SigT tp' _ ->
+                          eqDB conArg coArg (x, y, tp')
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| compareHD $(varE x) $(varE y) |]
+                          else
+                              [| pcompare $(varE x) $(varE y) |]
+            genLtClause (c, _) (d, _) =
+                clause [recP c [], recP d []] (normalB [| return LT |]) []
+            genGtClause (c, _) (d, _) =
+                clause [recP c [], recP d []] (normalB [| return GT |]) []
diff --git a/src/Data/Comp/Param/Multi/Derive/Projections.hs b/src/Data/Comp/Param/Multi/Derive/Projections.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/Projections.hs
@@ -0,0 +1,108 @@
+{-# LANGUAGE TemplateHaskell, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.Projections
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Derive functions for signature projections.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Derive.Projections
+    (
+     projn,
+     projectn,
+     deepProjectn
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Control.Monad (liftM)
+import Data.Comp.Param.Multi.HDitraversable (HDitraversable)
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Algebra (appTSigFunM')
+import Data.Comp.Param.Multi.Ops ((:+:)(..), (:<:)(..))
+
+projn :: Int -> Q [Dec]
+projn n = do
+  let p = mkName $ "proj" ++ show n
+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let ivar = mkName "i"
+  let xvar = mkName "x"
+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar gvars avar bvar ivar) []]]
+  sequence $ (sigD p $ genSig gvars avar bvar ivar) : d
+    where genSig gvars avar bvar ivar = do
+            let fvar = mkName "f"
+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
+                            (map varT gvars)
+            let tp' = arrowT `appT` (varT fvar `appT` varT avar `appT`
+                                     varT bvar `appT` varT ivar)
+                             `appT` (conT ''Maybe `appT`
+                                     (tp `appT` varT avar `appT`
+                                      varT bvar `appT` varT ivar))
+            forallT (map PlainTV $ fvar : avar : bvar : ivar : gvars)
+                    (sequence cxt) tp'
+          genDecl x [g] a b i =
+            [| liftM inj (proj $(varE x)
+                          :: Maybe ($(varT g `appT` varT a `appT`
+                                      varT b `appT` varT i))) |]
+          genDecl x (g:gs) a b i =
+            [| case (proj $(varE x)
+                         :: Maybe ($(varT g `appT` varT a `appT`
+                                     varT b `appT` varT i))) of
+                 Just y -> Just $ inj y
+                 _ -> $(genDecl x gs a b i) |]
+          genDecl _ _ _ _ _ = error "genDecl called with empty list"
+
+projectn :: Int -> Q [Dec]
+projectn n = do
+  let p = mkName ("project" ++ show n)
+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
+  let avar = mkName "a"
+  let bvar = mkName "b"
+  let ivar = mkName "i"
+  let xvar = mkName "x"
+  let d = [funD p [clause [varP xvar] (normalB $ genDecl xvar n) []]]
+  sequence $ (sigD p $ genSig gvars avar bvar ivar) : d
+    where genSig gvars avar bvar ivar = do
+            let fvar = mkName "f"
+            let hvar = mkName "h"
+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
+                            (map varT gvars)
+            let tp' = conT ''Cxt `appT` varT hvar `appT` varT fvar
+                                 `appT` varT avar `appT` varT bvar
+            let tp'' = arrowT `appT` (tp' `appT` varT ivar)
+                              `appT` (conT ''Maybe `appT`
+                                      (tp `appT` varT avar `appT` tp' `appT`
+                                       varT ivar))
+            forallT (map PlainTV $ hvar : fvar : avar : bvar : ivar : gvars)
+                    (sequence cxt) tp''
+          genDecl x n = [| case $(varE x) of
+                             Hole _ -> Nothing
+                             Var _ -> Nothing
+                             In t -> $(varE $ mkName $ "proj" ++ show n) t |]
+
+deepProjectn :: Int -> Q [Dec]
+deepProjectn n = do
+  let p = mkName ("deepProject" ++ show n)
+  let gvars = map (\n -> mkName $ 'g' : show n) [1..n]
+  let d = [funD p [clause [] (normalB $ genDecl n) []]]
+  sequence $ (sigD p $ genSig gvars) : d
+    where genSig gvars = do
+            let fvar = mkName "f"
+            let ivar = mkName "i"
+            let cxt = map (\g -> classP ''(:<:) [varT g, varT fvar]) gvars
+            let tp = foldl1 (\a g -> conT ''(:+:) `appT` g `appT` a)
+                            (map varT gvars)
+            let cxt' = classP ''HDitraversable [tp]
+            let tp' = arrowT `appT` (conT ''Term `appT` varT fvar `appT` varT ivar)
+                             `appT` (conT ''Maybe `appT` (conT ''Term `appT` tp `appT` varT ivar))
+            forallT (map PlainTV $ fvar : ivar : gvars) (sequence $ cxt' : cxt) tp'
+          genDecl n = [| appTSigFunM' $(varE $ mkName $ "proj" ++ show n) |]
diff --git a/src/Data/Comp/Param/Multi/Derive/Show.hs b/src/Data/Comp/Param/Multi/Derive/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/Show.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE TemplateHaskell, FlexibleInstances, IncoherentInstances,
+  ScopedTypeVariables, UndecidableInstances, KindSignatures #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.Show
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive instances of @ShowHD@.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.Derive.Show
+    (
+     ShowHD(..),
+     makeShowHD
+    ) where
+
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Multi.FreshM hiding (Name)
+import qualified Data.Comp.Param.Multi.FreshM as FreshM
+import Data.Comp.Param.Multi.HDifunctor
+import Control.Monad
+import Language.Haskell.TH hiding (Cxt, match)
+import qualified Data.Traversable as T
+
+{-| Signature printing. An instance @ShowHD f@ gives rise to an instance
+  @Show (Term f i)@. -}
+class ShowHD f where
+    showHD :: f FreshM.Name (K (FreshM String)) i -> FreshM String
+
+newtype Dummy = Dummy String
+
+instance Show Dummy where
+  show (Dummy s) = s
+
+{-| Derive an instance of 'ShowHD' for a type constructor of any parametric
+  kind taking at least three arguments. -}
+makeShowHD :: Name -> Q [Dec]
+makeShowHD fname = do
+  TyConI (DataD _ name args constrs _) <- abstractNewtypeQ $ reify fname
+  let args' = init args
+  -- covariant argument
+  let coArg :: Name = tyVarBndrName $ last args'
+  -- contravariant argument
+  let conArg :: Name = tyVarBndrName $ last $ init args'
+  let argNames = map (VarT . tyVarBndrName) (init $ init args')
+  let complType = foldl AppT (ConT name) argNames
+  let classType = AppT (ConT ''ShowHD) complType
+  constrs' :: [(Name,[Type])] <- mapM normalConExp constrs
+  showHDDecl <- funD 'showHD (map (showHDClause conArg coArg) constrs')
+  let context = map (\arg -> ClassP ''Show [arg]) argNames
+  return [InstanceD context classType [showHDDecl]]
+      where showHDClause :: Name -> Name -> (Name,[Type]) -> ClauseQ
+            showHDClause conArg coArg (constr, args) = do
+              varXs <- newNames (length args) "x"
+              -- Pattern for the constructor
+              let patx = ConP constr $ map VarP varXs
+              body <- showHDBody (nameBase constr) conArg coArg (zip varXs args)
+              return $ Clause [patx] (NormalB body) []
+            showHDBody :: String -> Name -> Name -> [(Name, Type)] -> ExpQ
+            showHDBody constr conArg coArg x =
+                [|liftM (unwords . (constr :) .
+                         map (\x -> if elem ' ' x then "(" ++ x ++ ")" else x))
+                        (sequence $(listE $ map (showHDB conArg coArg) x))|]
+            showHDB :: Name -> Name -> (Name, Type) -> ExpQ
+            showHDB conArg coArg (x, tp)
+                | not (containsType tp (VarT conArg)) &&
+                  not (containsType tp (VarT coArg)) =
+                    [| return $ show $(varE x) |]
+                | otherwise =
+                    case tp of
+                      AppT (VarT a) _ 
+                          | a == coArg -> [| unK $(varE x) |]
+                      AppT (AppT ArrowT (AppT (VarT a) _)) _
+                          | a == conArg ->
+                              [| withName (\v -> do body <- (unK . $(varE x)) v
+                                                    return $ "\\" ++ show v ++ " -> " ++ body) |]
+                      SigT tp' _ ->
+                          showHDB conArg coArg (x, tp')
+                      _ ->
+                          if containsType tp (VarT conArg) then
+                              [| showHD $(varE x) |]
+                          else
+                              [| liftM show $ T.mapM (liftM Dummy . unK) $(varE x) |]
diff --git a/src/Data/Comp/Param/Multi/Derive/SmartAConstructors.hs b/src/Data/Comp/Param/Multi/Derive/SmartAConstructors.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/SmartAConstructors.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.SmartAConstructors
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive smart constructors with annotations for higher-order
+-- difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Derive.SmartAConstructors 
+    (
+     smartAConstructors
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Multi.Ops
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.HDifunctor
+
+import Control.Monad
+
+{-| Derive smart constructors with annotations for a higher-order difunctor. The
+ smart constructors are similar to the ordinary constructors, but a
+ 'injectA . hdimap Var id' is automatically inserted. -}
+smartAConstructors :: Name -> Q [Dec]
+smartAConstructors fname = do
+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
+    let cons = map abstractConType constrs
+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
+        where genSmartConstr targs tname (name, args) = do
+                let bname = nameBase name
+                genSmartConstr' targs tname (mkName $ "iA" ++ bname) name args
+              genSmartConstr' targs tname sname name args = do
+                varNs <- newNames args "x"
+                varPr <- newName "_p"
+                let pats = map varP (varPr : varNs)
+                    vars = map varE varNs
+                    val = appE [|injectA $(varE varPr)|] $
+                          appE [|inj . hdimap Var id|] $ foldl appE (conE name) vars
+                    function = [funD sname [clause pats (normalB [|In $val|]) []]]
+                sequence function
diff --git a/src/Data/Comp/Param/Multi/Derive/SmartConstructors.hs b/src/Data/Comp/Param/Multi/Derive/SmartConstructors.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Derive/SmartConstructors.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Derive.SmartConstructors
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Automatically derive smart constructors for higher-order difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Derive.SmartConstructors 
+    (
+     smartConstructors
+    ) where
+
+import Language.Haskell.TH hiding (Cxt)
+import Data.Comp.Derive.Utils
+import Data.Comp.Param.Multi.Sum
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.HDifunctor
+import Control.Arrow ((&&&))
+import Control.Monad
+
+{-| Derive smart constructors for a higher-order difunctor. The smart
+ constructors are similar to the ordinary constructors, but a
+ 'inject . hdimap Var id' is automatically inserted. -}
+smartConstructors :: Name -> Q [Dec]
+smartConstructors fname = do
+    TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
+    let iVar = tyVarBndrName $ last targs
+    let cons = map (abstractConType &&& iTp iVar) constrs
+    liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons
+        where iTp iVar (ForallC _ cxt _) =
+                  -- Check if the GADT phantom type is constrained
+                  case [y | EqualP x y <- cxt, x == VarT iVar] of
+                    [] -> Nothing
+                    tp:_ -> Just tp
+              iTp _ _ = Nothing
+              genSmartConstr targs tname ((name, args), miTp) = do
+                let bname = nameBase name
+                genSmartConstr' targs tname (mkName $ 'i' : bname) name args miTp
+              genSmartConstr' targs tname sname name args miTp = do
+                varNs <- newNames args "x"
+                let pats = map varP varNs
+                    vars = map varE varNs
+                    val = foldl appE (conE name) vars
+                    sig = genSig targs tname sname args miTp
+                    function = [funD sname [clause pats (normalB [|inject (hdimap Var id $val)|]) []]]
+                sequence $ sig ++ function
+              genSig targs tname sname 0 miTp = (:[]) $ do
+                hvar <- newName "h"
+                fvar <- newName "f"
+                avar <- newName "a"
+                bvar <- newName "b"
+                ivar <- newName "i"
+                let targs' = init $ init $ init targs
+                    vars = hvar:fvar:avar:bvar:maybe [ivar] (const []) miTp++targs'
+                    h = varT hvar
+                    f = varT fvar
+                    a = varT avar
+                    b = varT bvar
+                    i = varT ivar
+                    ftype = foldl appT (conT tname) (map varT targs')
+                    constr = classP ''(:<:) [ftype, f]
+                    typ = foldl appT (conT ''Cxt) [h, f, a, b,maybe i return miTp]
+                    typeSig = forallT (map PlainTV vars) (sequence [constr]) typ
+                sigD sname typeSig
+              genSig _ _ _ _ _ = []
diff --git a/src/Data/Comp/Param/Multi/Desugar.hs b/src/Data/Comp/Param/Multi/Desugar.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Desugar.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TemplateHaskell, MultiParamTypeClasses, FlexibleInstances,
+  UndecidableInstances, OverlappingInstances, TypeOperators, Rank2Types #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Desugar
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This modules defines the 'Desugar' type class for desugaring of terms.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Desugar where
+
+import Data.Comp.Param.Multi
+
+-- |The desugaring term homomorphism.
+class (HDifunctor f, HDifunctor g) => Desugar f g where
+    desugHom :: Hom f g
+    desugHom = desugHom' . hfmap Hole
+    desugHom' :: f a (Cxt h g a b) :-> Cxt h g a b
+    desugHom' x = appCxt (desugHom x)
+
+-- We make the lifting to sums explicit in order to make the Desugar
+-- class work with the default instance declaration further below.
+instance (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
+    desugHom = caseHD desugHom desugHom
+
+
+-- |Desugar a term.
+desugar :: Desugar f g => Term f :-> Term g
+desugar (Term t) = Term (appHom desugHom t)
+
+-- |Lift desugaring to annotated terms.
+desugarA :: (HDifunctor f', HDifunctor g', DistAnn f p f', DistAnn g p g',
+             Desugar f g) => Term f' :-> Term g'
+desugarA (Term t) = Term (appHom (propAnn desugHom) t)
+
+-- |Default desugaring instance.
+instance (HDifunctor f, HDifunctor g, f :<: g) => Desugar f g where
+    desugHom = simpCxt . inj
diff --git a/src/Data/Comp/Param/Multi/Equality.hs b/src/Data/Comp/Param/Multi/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Equality.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
+  UndecidableInstances, IncoherentInstances, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Equality
+-- 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 equality for signatures, which lifts to equality for
+-- terms.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.Equality
+    (
+     PEq(..),
+     EqHD(..)
+    ) where
+
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Sum
+import Data.Comp.Param.Multi.Ops
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.FreshM
+
+-- |Equality on parametric values. The equality test is performed inside the
+-- 'FreshM' monad for generating fresh identifiers.
+class PEq a where
+    peq :: a i -> a j -> FreshM Bool
+
+instance Eq a => PEq (K a) where
+    peq (K x) (K y) = return $ x == y
+
+{-| Signature equality. An instance @EqHD f@ gives rise to an instance
+  @Eq (Term f i)@. The equality test is performed inside the 'FreshM' monad for
+  generating fresh identifiers. -}
+class EqHD f where
+    eqHD :: PEq a => f Name a i -> f Name a j -> FreshM Bool
+
+{-| 'EqHD' is propagated through sums. -}
+instance (EqHD f, EqHD g) => EqHD (f :+: g) where
+    eqHD (Inl x) (Inl y) = eqHD x y
+    eqHD (Inr x) (Inr y) = eqHD x y
+    eqHD _ _ = return False
+
+instance PEq Name where
+   peq x y = return $ nameCoerce x == y
+
+{-| From an 'EqHD' difunctor an 'Eq' instance of the corresponding term type can
+  be derived. -}
+instance EqHD f => EqHD (Cxt h f) where
+    eqHD (In e1) (In e2) = eqHD e1 e2
+    eqHD (Hole h1) (Hole h2) = peq h1 h2
+    eqHD (Var p1) (Var p2) = peq p1 p2
+    eqHD _ _ = return False
+
+instance (EqHD f, PEq a) => PEq (Cxt h f Name a) where
+    peq = eqHD
+
+{-| Equality on terms. -}
+instance (HDifunctor f, EqHD f) => Eq (Term f i) where
+    (==) (Term x) (Term y) = evalFreshM $ eqHD x y
diff --git a/src/Data/Comp/Param/Multi/FreshM.hs b/src/Data/Comp/Param/Multi/FreshM.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/FreshM.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.FreshM
+-- 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 a monad for generating fresh, abstract names, useful
+-- e.g. for defining equality on terms.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.FreshM
+    (
+     FreshM,
+     Name,
+     withName,
+     nameCoerce,
+     evalFreshM
+    ) where
+
+import Control.Monad.Reader
+import Control.Applicative
+
+-- |Monad for generating fresh (abstract) names.
+newtype FreshM a = FreshM{unFreshM :: Reader Int a}
+    deriving (Monad, Functor, Applicative)
+
+-- |Abstract notion of a name (the constructor is hidden).
+newtype Name i = Name Int
+    deriving Eq
+
+instance Show (Name i) where
+    show (Name x) = names !! x
+        where baseNames = ['a'..'z']
+              names = map (:[]) baseNames ++ names' 1
+              names' n = map (: show n) baseNames ++ names' (n + 1)
+
+instance Ord (Name i) where
+    compare (Name x) (Name y) = compare x y
+
+-- |Change the type tag of a name.
+nameCoerce :: Name i -> Name j
+nameCoerce (Name x) = Name x
+
+-- |Run the given computation with the next available name.
+withName :: (Name i -> FreshM a) -> FreshM a
+withName m = do name <- FreshM (asks Name)
+                FreshM $ local ((+) 1) $ unFreshM $ m name
+
+-- |Evaluate a computation that uses fresh names.
+evalFreshM :: FreshM a -> a
+evalFreshM (FreshM m) = runReader m 0
diff --git a/src/Data/Comp/Param/Multi/HDifunctor.hs b/src/Data/Comp/Param/Multi/HDifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/HDifunctor.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, Rank2Types,
+  TypeOperators, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.HDifunctor
+-- 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 higher-order difunctors, a hybrid between higher-order
+-- functors (Johann, Ghani, POPL '08), and difunctors (Meijer, Hutton, FPCA
+-- '95). Higher-order difunctors are used to define signatures for
+-- compositional parametric generalised data types.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.HDifunctor
+    (
+     HDifunctor (..),
+     HFunctor (..),
+     I (..),
+     K (..),
+     E (..),
+     A (..),
+     (:->),
+     NatM
+    ) where
+
+import Data.Comp.Multi.HFunctor
+
+-- | This class represents higher-order difunctors.
+class HDifunctor f where
+    hdimap :: (a :-> b) -> (c :-> d) -> f b c :-> f a d
+
+-- |A higher-order difunctor gives rise to a higher-order functor when
+-- restricted to a particular contravariant argument.
+instance HDifunctor f => HFunctor (f a) where
+    hfmap = hdimap id
diff --git a/src/Data/Comp/Param/Multi/HDitraversable.hs b/src/Data/Comp/Param/Multi/HDitraversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/HDitraversable.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE Rank2Types, FlexibleInstances, MultiParamTypeClasses,
+  FlexibleContexts, OverlappingInstances, TypeOperators, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.HDitraversable
+-- 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 traversable higher-order difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.HDitraversable
+    (
+     HDitraversable (..),
+     HTraversable (..)
+    ) where
+
+import Prelude hiding (mapM, sequence, foldr)
+import Data.Comp.Multi.HTraversable
+import Data.Comp.Param.Multi.HDifunctor
+
+{-| HDifunctors representing data structures that can be traversed from left to
+  right. -}
+class HDifunctor f => HDitraversable f where
+    hdimapM :: Monad m => NatM m b c -> NatM m (f a b) (f a c)
diff --git a/src/Data/Comp/Param/Multi/Ops.hs b/src/Data/Comp/Param/Multi/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Ops.hs
@@ -0,0 +1,126 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies,
+  FlexibleInstances, UndecidableInstances, IncoherentInstances,
+  KindSignatures, RankNTypes #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Ops
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides operators on higher-order difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Ops where
+
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.HDitraversable
+import qualified Data.Comp.Ops as O
+import Control.Monad (liftM)
+
+
+-- Sums
+infixr 6 :+:
+
+-- |Formal sum of signatures (difunctors).
+data (f :+: g) (a :: * -> *) (b :: * -> *) i = Inl (f a b i)
+                                             | Inr (g a b i)
+
+{-| Utility function to case on a higher-order difunctor sum, without exposing
+  the internal representation of sums. -}
+caseHD :: (f a b i -> c) -> (g a b i -> c) -> (f :+: g) a b i -> c
+caseHD f g x = case x of
+                 Inl x -> f x
+                 Inr x -> g x
+
+instance (HDifunctor f, HDifunctor g) => HDifunctor (f :+: g) where
+    hdimap f g (Inl e) = Inl (hdimap f g e)
+    hdimap f g (Inr e) = Inr (hdimap f g e)
+
+instance (HDitraversable f, HDitraversable g) => HDitraversable (f :+: g) where
+    hdimapM f (Inl e) = Inl `liftM` hdimapM f e
+    hdimapM f (Inr e) = Inr `liftM` hdimapM f e
+
+-- | Signature containment relation for automatic injections. The left-hand must
+-- be an atomic signature, where as the right-hand side must have a list-like
+-- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,
+-- non-examples include @f :+: g :<: f :+: (g :+: h)@ and
+-- @f :<: (f :+: g) :+: h@.
+class (sub :: (* -> *) -> (* -> *) -> * -> *) :<: sup where
+    inj :: sub a b :-> sup a b
+    proj :: NatM Maybe (sup a b) (sub a b)
+
+instance (:<:) f f where
+    inj = id
+    proj = Just
+
+instance (:<:) f (f :+: g) where
+    inj = Inl
+    proj (Inl x) = Just x
+    proj (Inr _) = Nothing
+
+instance (f :<: g) => (:<:) f (h :+: g) where
+    inj = Inr . inj
+    proj (Inr x) = proj x
+    proj (Inl _) = Nothing
+
+
+-- Products
+infixr 8 :*:
+
+-- |Formal product of signatures (higher-order difunctors).
+data (f :*: g) a b = f a b :*: g a b
+
+ffst :: (f :*: g) a b -> f a b
+ffst (x :*: _) = x
+
+fsnd :: (f :*: g) a b -> g a b 
+fsnd (_ :*: x) = x
+
+
+-- Constant Products
+infixr 7 :&:
+
+{-| This data type adds a constant product to a signature. -}
+data (f :&: p) (a :: * -> *) (b :: * -> *) i = f a b i :&: p
+
+instance HDifunctor f => HDifunctor (f :&: p) where
+    hdimap f g (v :&: c) = hdimap f g v :&: c
+
+instance HDitraversable f => HDitraversable (f :&: p) where
+    hdimapM f (v :&: c) = liftM (:&: c) (hdimapM f v)
+
+{-| This class defines how to distribute an annotation over a sum of
+  signatures. -}
+class DistAnn (s :: (* -> *) -> (* -> *) -> * -> *) p s' | s' -> s, s' -> p where
+    {-| Inject an annotation over a signature. -}
+    injectA :: p -> s a b :-> s' a b
+    {-| Project an annotation from a signature. -}
+    projectA :: s' a b :-> (s a b O.:&: p)
+
+class RemA (s :: (* -> *) -> (* -> *) -> * -> *) s' | s -> s' where
+    {-| Remove annotations from a signature. -}
+    remA :: s a b :-> s' a b
+
+instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where
+    remA (Inl (v :&: _)) = Inl v
+    remA (Inr v) = Inr $ remA v
+
+instance RemA (f :&: p) f where
+    remA (v :&: _) = v
+
+instance DistAnn f p (f :&: p) where
+    injectA c v = v :&: c
+
+    projectA (v :&: p) = v O.:&: p
+
+instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where
+    injectA c (Inl v) = Inl (v :&: c)
+    injectA c (Inr v) = Inr $ injectA c v
+
+    projectA (Inl (v :&: p)) = Inl v O.:&: p
+    projectA (Inr v) = let (v' O.:&: p) = projectA v
+                       in Inr v' O.:&: p
diff --git a/src/Data/Comp/Param/Multi/Ordering.hs b/src/Data/Comp/Param/Multi/Ordering.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Ordering.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
+  UndecidableInstances, IncoherentInstances, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Ordering
+-- 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 ordering of signatures, which lifts to ordering of
+-- terms and contexts.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.Ordering
+    (
+     POrd(..),
+     OrdHD(..)
+    ) where
+
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Sum
+import Data.Comp.Param.Multi.Ops
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.FreshM
+import Data.Comp.Param.Multi.Equality
+
+-- |Ordering of parametric values.
+class PEq a => POrd a where
+    pcompare :: a i -> a j -> FreshM Ordering
+
+instance Ord a => POrd (K a) where
+    pcompare (K x) (K y) = return $ compare x y
+
+{-| Signature ordering. An instance @OrdHD f@ gives rise to an instance
+  @Ord (Term f)@. -}
+class EqHD f => OrdHD f where
+    compareHD :: POrd a => f Name a i -> f Name a j -> FreshM Ordering
+
+{-| 'OrdHD' is propagated through sums. -}
+instance (OrdHD f, OrdHD g) => OrdHD (f :+: g) where
+    compareHD (Inl x) (Inl y) = compareHD x y
+    compareHD (Inl _) (Inr _) = return LT
+    compareHD (Inr x) (Inr y) = compareHD x y
+    compareHD (Inr _) (Inl _) = return GT
+
+{-| From an 'OrdHD' difunctor an 'Ord' instance of the corresponding term type
+  can be derived. -}
+instance OrdHD f => OrdHD (Cxt h f) where
+    compareHD (In e1) (In e2) = compareHD e1 e2
+    compareHD (Hole h1) (Hole h2) = pcompare h1 h2
+    compareHD (Var p1) (Var p2) = pcompare p1 p2
+    compareHD (In _) _ = return LT
+    compareHD (Hole _) (In _) = return GT
+    compareHD (Hole _) (Var _) = return LT
+    compareHD (Var _) _ = return GT
+
+instance POrd Name where
+    pcompare x y = return $ compare (nameCoerce x) y
+
+instance (OrdHD f, POrd a) => POrd (Cxt h f Name a) where
+    pcompare = compareHD
+
+{-| Ordering of terms. -}
+instance (HDifunctor f, OrdHD f) => Ord (Term f i) where
+    compare (Term x) (Term y) = evalFreshM $ compareHD x y
diff --git a/src/Data/Comp/Param/Multi/Show.hs b/src/Data/Comp/Param/Multi/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Show.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TypeOperators, FlexibleInstances, TypeSynonymInstances,
+  IncoherentInstances, UndecidableInstances, TemplateHaskell, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Show
+-- 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 showing of signatures, which lifts to showing of terms.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Multi.Show
+    (
+     ShowHD(..)
+    ) where
+
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.Ops
+import Data.Comp.Param.Multi.Derive
+import Data.Comp.Param.Multi.FreshM
+
+-- Lift ShowHD to sums
+$(derive [liftSum] [''ShowHD])
+
+{-| From an 'ShowHD' higher-order difunctor an 'ShowHD' instance of the
+  corresponding term type can be derived. -}
+instance (HDifunctor f, ShowHD f) => ShowHD (Cxt h f) where
+    showHD (In t) = showHD $ hfmap (K . showHD) t
+    showHD (Hole h) = unK h
+    showHD (Var p) = return $ show p
+
+{-| Printing of terms. -}
+instance (HDifunctor f, ShowHD f) => Show (Term f i) where
+    show = evalFreshM . showHD . toCxt . unTerm
+
+instance (ShowHD f, Show p) => ShowHD (f :&: p) where
+    showHD (x :&: p) = do sx <- showHD x
+                          return $ sx ++ " :&: " ++ show p
diff --git a/src/Data/Comp/Param/Multi/Sum.hs b/src/Data/Comp/Param/Multi/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Sum.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,
+  FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
+  ScopedTypeVariables, TemplateHaskell #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Sum
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides the infrastructure to extend signatures.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Sum
+    (
+     (:<:),
+     (:+:),
+     caseHD,
+
+     -- * Projections for Signatures and Terms
+     proj,
+     proj2,
+     proj3,
+     proj4,
+     proj5,
+     proj6,
+     proj7,
+     proj8,
+     proj9,
+     proj10,
+     project,
+     project2,
+     project3,
+     project4,
+     project5,
+     project6,
+     project7,
+     project8,
+     project9,
+     project10,
+     deepProject,
+     deepProject2,
+     deepProject3,
+     deepProject4,
+     deepProject5,
+     deepProject6,
+     deepProject7,
+     deepProject8,
+     deepProject9,
+     deepProject10,
+
+     -- * Injections for Signatures and Terms
+     inj,
+     inj2,
+     inj3,
+     inj4,
+     inj5,
+     inj6,
+     inj7,
+     inj8,
+     inj9,
+     inj10,
+     inject,
+     inject2,
+     inject3,
+     inject4,
+     inject5,
+     inject6,
+     inject7,
+     inject8,
+     inject9,
+     inject10,
+     deepInject,
+     deepInject2,
+     deepInject3,
+     deepInject4,
+     deepInject5,
+     deepInject6,
+     deepInject7,
+     deepInject8,
+     deepInject9,
+     deepInject10,
+
+     injectCxt,
+     liftCxt
+    ) where
+
+import Prelude hiding (sequence)
+import Control.Monad hiding (sequence)
+import Data.Comp.Param.Multi.Term
+import Data.Comp.Param.Multi.Algebra
+import Data.Comp.Param.Multi.Ops
+import Data.Comp.Param.Multi.Derive.Projections
+import Data.Comp.Param.Multi.Derive.Injections
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.HDitraversable
+
+$(liftM concat $ mapM projn [2..10])
+
+-- |Project the outermost layer of a term to a sub signature. If the signature
+-- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.
+project :: (g :<: f) => NatM Maybe (Cxt h f a b) (g a (Cxt h f a b))
+project (In t)   = proj t
+project (Hole _) = Nothing
+project (Var _)  = Nothing
+
+$(liftM concat $ mapM projectn [2..10])
+
+-- | Tries to coerce a term/context to a term/context over a sub-signature. If
+-- the signature @g@ is compound of /n/ atomic signatures, use
+-- @deepProject@/n/ instead.
+deepProject :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i)
+{-# INLINE deepProject #-}
+deepProject = appTSigFunM' proj
+
+$(liftM concat $ mapM deepProjectn [2..10])
+{-# INLINE deepProject2 #-}
+{-# INLINE deepProject3 #-}
+{-# INLINE deepProject4 #-}
+{-# INLINE deepProject5 #-}
+{-# INLINE deepProject6 #-}
+{-# INLINE deepProject7 #-}
+{-# INLINE deepProject8 #-}
+{-# INLINE deepProject9 #-}
+{-# INLINE deepProject10 #-}
+
+$(liftM concat $ mapM injn [2..10])
+
+-- |Inject a term where the outermost layer is a sub signature. If the signature
+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.
+inject :: (g :<: f) => g a (Cxt h f a b) :-> Cxt h f a b
+inject = In . inj
+
+$(liftM concat $ mapM injectn [2..10])
+
+-- |Inject a term over a sub signature to a term over larger signature. If the
+-- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/
+-- instead.
+deepInject :: (HDifunctor g, g :<: f) => CxtFun g f
+{-# INLINE deepInject #-}
+deepInject = appSigFun inj
+
+$(liftM concat $ mapM deepInjectn [2..10])
+{-# INLINE deepInject2 #-}
+{-# INLINE deepInject3 #-}
+{-# INLINE deepInject4 #-}
+{-# INLINE deepInject5 #-}
+{-# INLINE deepInject6 #-}
+{-# INLINE deepInject7 #-}
+{-# INLINE deepInject8 #-}
+{-# INLINE deepInject9 #-}
+{-# INLINE deepInject10 #-}
+
+{-| This function injects a whole context into another context. -}
+injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b
+injectCxt (In t) = inject $ hfmap injectCxt t
+injectCxt (Hole x) = x
+injectCxt (Var p) = Var p
+
+{-| This function lifts the given functor to a context. -}
+liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b
+liftCxt g = simpCxt $ inj g
+
+instance (Show (f a b i), Show (g a b i)) => Show ((f :+: g) a b i) where
+    show (Inl v) = show v
+    show (Inr v) = show v
+
+instance (Ord (f a b i), Ord (g a b i)) => Ord ((f :+: g) a b i) where
+    compare (Inl _) (Inr _) = LT
+    compare (Inr _) (Inl _) = GT
+    compare (Inl x) (Inl y) = compare x y
+    compare (Inr x) (Inr y) = compare x y
+
+instance (Eq (f a b i), Eq (g a b i)) => Eq ((f :+: g) a b i) where
+    (Inl x) == (Inl y) = x == y
+    (Inr x) == (Inr y) = x == y                   
+    _ == _ = False
diff --git a/src/Data/Comp/Param/Multi/Term.hs b/src/Data/Comp/Param/Multi/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Multi/Term.hs
@@ -0,0 +1,126 @@
+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,
+  MultiParamTypeClasses, TypeOperators, ScopedTypeVariables #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Multi.Term
+-- 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 central notion of /generalised parametrised terms/
+-- and their generalisation to generalised parametrised contexts.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Multi.Term
+    (
+     Cxt(..),
+     Hole,
+     NoHole,
+     Term(..),
+     Trm,
+     Context,
+     simpCxt,
+     toCxt,
+     hfmapCxt,
+     hdimapMCxt,
+     ParamFunctor (..)
+    ) where
+
+import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
+import Data.Comp.Param.Multi.HDifunctor
+import Data.Comp.Param.Multi.HDitraversable
+import Control.Monad 
+import Unsafe.Coerce
+import Data.Maybe (fromJust)
+
+{-| This data type represents contexts over a signature. Contexts are terms
+  containing zero or more holes, and zero or more parameters. The first
+  parameter is a phantom type indicating whether the context has holes. The
+  second paramater is the signature of the context, in the form of a
+  "Data.Comp.Param.Multi.HDifunctor". The third parameter is the type of
+  parameters, the fourth parameter is the type of holes, and the fifth
+  parameter is the GADT type. -}
+data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where
+            In :: f a (Cxt h f a b) i -> Cxt h f a b i
+            Hole :: b i -> Cxt Hole f a b i
+            Var :: a i -> Cxt h f a b i
+
+{-| Phantom type used to define 'Context'. -}
+data Hole
+
+{-| Phantom type used to define 'Term'. -}
+data NoHole
+
+{-| A context may contain holes. -}
+type Context = Cxt Hole
+
+{-| \"Preterms\" |-}
+type Trm f a = Cxt NoHole f a (K ())
+
+{-| A term is a context with no holes, where all occurrences of the
+  contravariant parameter is fully parametric. -}
+newtype Term f i = Term{unTerm :: forall a. Trm f a i}
+
+{-| Convert a difunctorial value into a context. -}
+simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b
+{-# INLINE simpCxt #-}
+simpCxt = In . hfmap Hole
+
+toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b
+{-# INLINE toCxt #-}
+toCxt = unsafeCoerce
+
+-- | This is an instance of 'hfmap' for 'Cxt'.
+hfmapCxt :: forall h f a b b'. HDifunctor f
+         => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'
+hfmapCxt f = run
+    where run :: Cxt h f a b :-> Cxt h f a b'
+          run (In t)   = In $ hfmap run t
+          run (Var a)  = Var a
+          run (Hole b) = Hole $ f b
+
+-- | This is an instance of 'hdimapM' for 'Cxt'.
+hdimapMCxt :: forall h f a b b' m . (HDitraversable f, Monad m)
+          => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')
+hdimapMCxt f = run
+    where run :: NatM m (Cxt h f a b) (Cxt h f a b')
+          run (In t)   = liftM In $ hdimapM run t
+          run (Var a)  = return $ Var a
+          run (Hole b) = liftM Hole (f b)
+          
+          
+          
+{-| Monads for which embedded @Trm@ values, which are parametric at top level,
+  can be made into monadic @Term@ values, i.e. \"pushing the parametricity
+  inwards\". -}
+class ParamFunctor m where
+    termM :: (forall a. m (Trm f a i)) -> m (Term f i)
+
+coerceTermM :: ParamFunctor m => (forall a. m (Trm f a i)) -> m (Term f i)
+{-# INLINE coerceTermM #-}
+coerceTermM t = unsafeCoerce t
+
+{-# RULES
+    "termM/coerce'" termM = coerceTermM
+ #-}
+
+instance ParamFunctor Maybe where
+    {-# NOINLINE [1] termM #-}
+    termM Nothing = Nothing
+    termM x       = Just (Term $ fromJust x)
+
+instance ParamFunctor (Either a) where
+    {-# NOINLINE [1] termM #-}
+    termM (Left x) = Left x
+    termM x        = Right (Term $ fromRight x)
+                             where fromRight :: Either a b -> b
+                                   fromRight (Right x) = x
+                                   fromRight _ = error "fromRight: Left"
+
+instance ParamFunctor [] where
+    {-# NOINLINE [1] termM #-}
+    termM [] = []
+    termM l  = Term (head l) : termM (tail l)
diff --git a/src/Data/Comp/Param/Ops.hs b/src/Data/Comp/Param/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Ops.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies,
+  FlexibleInstances, UndecidableInstances, IncoherentInstances #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Ops
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides operators on difunctors.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Ops where
+
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.Ditraversable
+import Control.Monad (liftM)
+
+
+-- Sums
+infixr 6 :+:
+
+-- |Formal sum of signatures (difunctors).
+data (f :+: g) a b = Inl (f a b)
+                   | Inr (g a b)
+
+{-| Utility function to case on a difunctor sum, without exposing the internal
+  representation of sums. -}
+caseD :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
+caseD f g x = case x of
+                Inl x -> f x
+                Inr x -> g x
+
+instance (Difunctor f, Difunctor g) => Difunctor (f :+: g) where
+    dimap f g (Inl e) = Inl (dimap f g e)
+    dimap f g (Inr e) = Inr (dimap f g e)
+
+instance (Ditraversable f, Ditraversable g) => Ditraversable (f :+: g) where
+    dimapM f (Inl e) = Inl `liftM` dimapM f e
+    dimapM f (Inr e) = Inr `liftM` dimapM f e
+    disequence (Inl e) = Inl `liftM` disequence e
+    disequence (Inr e) = Inr `liftM` disequence e
+
+-- | Signature containment relation for automatic injections. The left-hand must
+-- be an atomic signature, where as the right-hand side must have a list-like
+-- structure. Examples include @f :<: f :+: g@ and @g :<: f :+: (g :+: h)@,
+-- non-examples include @f :+: g :<: f :+: (g :+: h)@ and
+-- @f :<: (f :+: g) :+: h@.
+class sub :<: sup where
+  inj :: sub a b -> sup a b
+  proj :: sup a b -> Maybe (sub a b)
+
+instance (:<:) f f where
+    inj = id
+    proj = Just
+
+instance (:<:) f (f :+: g) where
+    inj = Inl
+    proj (Inl x) = Just x
+    proj (Inr _) = Nothing
+
+instance (f :<: g) => (:<:) f (h :+: g) where
+    inj = Inr . inj
+    proj (Inr x) = proj x
+    proj (Inl _) = Nothing
+
+
+-- Products
+infixr 8 :*:
+
+-- |Formal product of signatures (difunctors).
+data (f :*: g) a b = f a b :*: g a b
+
+ffst :: (f :*: g) a b -> f a b
+ffst (x :*: _) = x
+
+fsnd :: (f :*: g) a b -> g a b
+fsnd (_ :*: x) = x
+
+
+-- Constant Products
+infixr 7 :&:
+
+{-| This data type adds a constant product to a signature. -}
+data (f :&: p) a b = f a b :&: p
+
+instance Difunctor f => Difunctor (f :&: p) where
+    dimap f g (v :&: c) = dimap f g v :&: c
+
+instance Ditraversable f => Ditraversable (f :&: p) where
+    dimapM f (v :&: c) = liftM (:&: c) (dimapM f v)
+    disequence (v :&: c) = liftM (:&: c) (disequence v)
+
+{-| This class defines how to distribute an annotation over a sum of
+  signatures. -}
+class DistAnn s p s' | s' -> s, s' -> p where
+    {-| Inject an annotation over a signature. -}
+    injectA :: p -> s a b -> s' a b
+    {-| Project an annotation from a signature. -}
+    projectA :: s' a b -> (s a b, p)
+
+class RemA s s' | s -> s'  where
+    {-| Remove annotations from a signature. -}
+    remA :: s a b -> s' a b
+
+instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where
+    remA (Inl (v :&: _)) = Inl v
+    remA (Inr v) = Inr $ remA v
+
+instance RemA (f :&: p) f where
+    remA (v :&: _) = v
+
+instance DistAnn f p (f :&: p) where
+    injectA c v = v :&: c
+
+    projectA (v :&: p) = (v,p)
+
+instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where
+    injectA c (Inl v) = Inl (v :&: c)
+    injectA c (Inr v) = Inr $ injectA c v
+
+    projectA (Inl (v :&: p)) = (Inl v,p)
+    projectA (Inr v) = let (v',p) = projectA v
+                       in  (Inr v',p)
diff --git a/src/Data/Comp/Param/Ordering.hs b/src/Data/Comp/Param/Ordering.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Ordering.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE TypeOperators, TypeSynonymInstances, FlexibleInstances,
+  UndecidableInstances, IncoherentInstances, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Ordering
+-- 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 ordering of signatures, which lifts to ordering of
+-- terms and contexts.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Ordering
+    (
+     POrd(..),
+     OrdD(..),
+     compList
+    ) where
+
+import Data.Comp.Param.Term
+import Data.Comp.Param.Sum
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.FreshM
+import Data.Comp.Param.Equality
+import Data.Maybe (fromMaybe)
+import Data.List (find)
+import Control.Monad (liftM)
+
+-- |Ordering of parametric values.
+class PEq a => POrd a where
+    pcompare :: a -> a -> FreshM Ordering
+
+instance POrd a => POrd [a] where
+    pcompare l1 l2
+        | length l1 < length l2 = return LT
+        | length l1 > length l2 = return GT
+        | otherwise = liftM compList $ mapM (uncurry pcompare) $ zip l1 l2
+
+compList :: [Ordering] -> Ordering
+compList = fromMaybe EQ . find (/= EQ)
+
+instance Ord a => POrd a where
+    pcompare x y = return $ compare x y
+
+{-| Signature ordering. An instance @OrdD f@ gives rise to an instance
+  @Ord (Term f)@. -}
+class EqD f => OrdD f where
+    compareD :: POrd a => f Name a -> f Name a -> FreshM Ordering
+
+{-| 'OrdD' is propagated through sums. -}
+instance (OrdD f, OrdD g) => OrdD (f :+: g) where
+    compareD (Inl x) (Inl y) = compareD x y
+    compareD (Inl _) (Inr _) = return LT
+    compareD (Inr x) (Inr y) = compareD x y
+    compareD (Inr _) (Inl _) = return GT
+
+{-| From an 'OrdD' difunctor an 'Ord' instance of the corresponding term type
+  can be derived. -}
+instance OrdD f => OrdD (Cxt h f) where
+    compareD (In e1) (In e2) = compareD e1 e2
+    compareD (Hole h1) (Hole h2) = pcompare h1 h2
+    compareD (Var p1) (Var p2) = pcompare p1 p2
+    compareD (In _) _ = return LT
+    compareD (Hole _) (In _) = return GT
+    compareD (Hole _) (Var _) = return LT
+    compareD (Var _) _ = return GT
+
+instance (OrdD f, POrd a) => POrd (Cxt h f Name a) where
+    pcompare = compareD
+
+{-| Ordering of terms. -}
+instance (Difunctor f, OrdD f) => Ord (Term f) where
+    compare (Term x) (Term y) = evalFreshM $ compareD x y
diff --git a/src/Data/Comp/Param/Show.hs b/src/Data/Comp/Param/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Show.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE TypeOperators, FlexibleInstances, TypeSynonymInstances,
+  IncoherentInstances, UndecidableInstances, TemplateHaskell, GADTs #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Show
+-- 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 showing of signatures, which lifts to showing of terms.
+--
+--------------------------------------------------------------------------------
+module Data.Comp.Param.Show
+    (
+     ShowD(..)
+    ) where
+
+import Data.Comp.Param.Term
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Derive
+import Data.Comp.Param.FreshM
+
+-- Lift ShowD to sums
+$(derive [liftSum] [''ShowD])
+
+{-| From an 'ShowD' difunctor an 'ShowD' instance of the corresponding term type
+  can be derived. -}
+instance (Difunctor f, ShowD f) => ShowD (Cxt h f) where
+    showD (In t) = showD $ fmap showD t
+    showD (Hole h) = h
+    showD (Var p) = return $ show p
+
+{-| Printing of terms. -}
+instance (Difunctor f, ShowD f) => Show (Term f) where
+    show = evalFreshM . showD . toCxt . unTerm
+
+instance (ShowD f, Show p) => ShowD (f :&: p) where
+    showD (x :&: p) = do sx <- showD x
+                         return $ sx ++ " :&: " ++ show p
diff --git a/src/Data/Comp/Param/Sum.hs b/src/Data/Comp/Param/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Sum.hs
@@ -0,0 +1,186 @@
+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, IncoherentInstances,
+  FlexibleInstances, FlexibleContexts, GADTs, TypeSynonymInstances,
+  ScopedTypeVariables, TemplateHaskell, Rank2Types #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Sum
+-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
+-- License     :  BSD3
+-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides the infrastructure to extend signatures.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Sum
+    (
+     (:<:),
+     (:+:),
+     caseD,
+
+     -- * Projections for Signatures and Terms
+     proj,
+     proj2,
+     proj3,
+     proj4,
+     proj5,
+     proj6,
+     proj7,
+     proj8,
+     proj9,
+     proj10,
+     project,
+     project2,
+     project3,
+     project4,
+     project5,
+     project6,
+     project7,
+     project8,
+     project9,
+     project10,
+     deepProject,
+     deepProject2,
+     deepProject3,
+     deepProject4,
+     deepProject5,
+     deepProject6,
+     deepProject7,
+     deepProject8,
+     deepProject9,
+     deepProject10,
+
+     -- * Injections for Signatures and Terms
+     inj,
+     inj2,
+     inj3,
+     inj4,
+     inj5,
+     inj6,
+     inj7,
+     inj8,
+     inj9,
+     inj10,
+     inject,
+     inject',
+     inject2,
+     inject3,
+     inject4,
+     inject5,
+     inject6,
+     inject7,
+     inject8,
+     inject9,
+     inject10,
+     deepInject,
+     deepInject2,
+     deepInject3,
+     deepInject4,
+     deepInject5,
+     deepInject6,
+     deepInject7,
+     deepInject8,
+     deepInject9,
+     deepInject10,
+
+     injectCxt,
+     liftCxt
+    ) where
+
+import Prelude hiding (sequence)
+import Control.Monad hiding (sequence)
+import Data.Comp.Param.Term
+import Data.Comp.Param.Algebra
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Derive.Projections
+import Data.Comp.Param.Derive.Injections
+import Data.Comp.Param.Difunctor
+import Data.Comp.Param.Ditraversable
+
+$(liftM concat $ mapM projn [2..10])
+
+-- |Project the outermost layer of a term to a sub signature. If the signature
+-- @g@ is compound of /n/ atomic signatures, use @project@/n/ instead.
+project :: (g :<: f) => Cxt h f a b -> Maybe (g a (Cxt h f a b))
+project (In t) = proj t
+project (Hole _) = Nothing
+project (Var _) = Nothing
+
+$(liftM concat $ mapM projectn [2..10])
+
+-- | Tries to coerce a term/context to a term/context over a sub-signature. If
+-- the signature @g@ is compound of /n/ atomic signatures, use
+-- @deepProject@/n/ instead.
+deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)
+{-# INLINE deepProject #-}
+deepProject = appTSigFunM' proj
+
+$(liftM concat $ mapM deepProjectn [2..10])
+{-# INLINE deepProject2 #-}
+{-# INLINE deepProject3 #-}
+{-# INLINE deepProject4 #-}
+{-# INLINE deepProject5 #-}
+{-# INLINE deepProject6 #-}
+{-# INLINE deepProject7 #-}
+{-# INLINE deepProject8 #-}
+{-# INLINE deepProject9 #-}
+{-# INLINE deepProject10 #-}
+
+$(liftM concat $ mapM injn [2..10])
+
+-- |Inject a term where the outermost layer is a sub signature. If the signature
+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.
+inject :: (g :<: f) => g a (Cxt h f a b) -> Cxt h f a b
+inject = In . inj
+
+-- |Inject a term where the outermost layer is a sub signature. If the signature
+-- @g@ is compound of /n/ atomic signatures, use @inject@/n/ instead.
+inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b
+inject' = inject . dimap Var id
+
+$(liftM concat $ mapM injectn [2..10])
+
+-- |Inject a term over a sub signature to a term over larger signature. If the
+-- signature @g@ is compound of /n/ atomic signatures, use @deepInject@/n/
+-- instead.
+deepInject :: (Difunctor g, g :<: f) => Term g -> Term f
+{-# INLINE deepInject #-}
+deepInject (Term t) = Term (appSigFun inj t)
+
+$(liftM concat $ mapM deepInjectn [2..10])
+{-# INLINE deepInject2 #-}
+{-# INLINE deepInject3 #-}
+{-# INLINE deepInject4 #-}
+{-# INLINE deepInject5 #-}
+{-# INLINE deepInject6 #-}
+{-# INLINE deepInject7 #-}
+{-# INLINE deepInject8 #-}
+{-# INLINE deepInject9 #-}
+{-# INLINE deepInject10 #-}
+
+{-| This function injects a whole context into another context. -}
+injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a b
+injectCxt (In t) = inject $ difmap injectCxt t
+injectCxt (Hole x) = x
+injectCxt (Var p) = Var p
+
+{-| This function lifts the given functor to a context. -}
+liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a b
+liftCxt g = simpCxt $ inj g
+
+instance (Show (f a b), Show (g a b)) => Show ((f :+: g) a b) where
+    show (Inl v) = show v
+    show (Inr v) = show v
+
+instance (Ord (f a b), Ord (g a b)) => Ord ((f :+: g) a b) where
+    compare (Inl _) (Inr _) = LT
+    compare (Inr _) (Inl _) = GT
+    compare (Inl x) (Inl y) = compare x y
+    compare (Inr x) (Inr y) = compare x y
+
+instance (Eq (f a b), Eq (g a b)) => Eq ((f :+: g) a b) where
+    (Inl x) == (Inl y) = x == y
+    (Inr x) == (Inr y) = x == y                   
+    _ == _ = False
diff --git a/src/Data/Comp/Param/Term.hs b/src/Data/Comp/Param/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Term.hs
@@ -0,0 +1,112 @@
+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,
+  MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Term
+-- 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 central notion of /parametrised terms/ and their
+-- generalisation to parametrised contexts.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Term
+    (
+     Cxt(..),
+     Hole,
+     NoHole,
+     Term(..),
+     Trm,
+     Context,
+     simpCxt,
+     toCxt,
+     cxtMap,
+     ParamFunctor(..)
+    ) where
+
+import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
+import Data.Comp.Param.Difunctor
+import Unsafe.Coerce (unsafeCoerce)
+
+import Data.Maybe (fromJust)
+
+{-| This data type represents contexts over a signature. Contexts are terms
+  containing zero or more holes, and zero or more parameters. The first
+  parameter is a phantom type indicating whether the context has holes. The
+  second paramater is the signature of the context, in the form of a
+  "Data.Comp.Param.Difunctor". The third parameter is the type of parameters,
+  and the fourth parameter is the type of holes. -}
+data Cxt :: * -> (* -> * -> *) -> * -> * -> * where
+            In :: f a (Cxt h f a b) -> Cxt h f a b
+            Hole :: b -> Cxt Hole f a b
+            Var :: a -> Cxt h f a b
+
+{-| Phantom type used to define 'Context'. -}
+data Hole
+
+{-| Phantom type used to define 'Term'. -}
+data NoHole
+
+{-| A context may contain holes. -}
+type Context = Cxt Hole
+
+{-| \"Preterms\" -}
+type Trm f a = Cxt NoHole f a ()
+
+{-| A term is a context with no holes, where all occurrences of the
+  contravariant parameter is fully parametric. -}
+newtype Term f = Term{unTerm :: forall a. Trm f a}
+
+{-| Convert a difunctorial value into a context. -}
+simpCxt :: Difunctor f => f a b -> Cxt Hole f a b
+{-# INLINE simpCxt #-}
+simpCxt = In . difmap Hole
+
+toCxt :: Difunctor f => Trm f a -> Cxt h f a b
+{-# INLINE toCxt #-}
+toCxt = unsafeCoerce
+
+-- | This combinator maps a function over a context by applying the
+-- function to each hole.
+cxtMap :: Difunctor f => (b -> c) -> Context f a b -> Context f a c
+cxtMap f (Hole x) = Hole (f x)
+cxtMap _ (Var x)  = Var x
+cxtMap f (In t)   = In (dimap id (cxtMap f) t)
+
+-- Param Functor
+
+{-| Monads for which embedded @Trm@ values, which are parametric at top level,
+  can be made into monadic @Term@ values, i.e. \"pushing the parametricity
+  inwards\". -}
+class ParamFunctor m where
+    termM :: (forall a. m (Trm f a)) -> m (Term f)
+
+coerceTermM :: ParamFunctor m => (forall a. m (Trm f a)) -> m (Term f)
+{-# INLINE coerceTermM #-}
+coerceTermM t = unsafeCoerce t
+
+{-# RULES
+    "termM/coerce" termM = coerceTermM
+ #-}
+
+instance ParamFunctor Maybe where
+    {-# NOINLINE [1] termM #-}
+    termM Nothing = Nothing
+    termM x       = Just (Term $ fromJust x)
+
+instance ParamFunctor (Either a) where
+    {-# NOINLINE [1] termM #-}
+    termM (Left x) = Left x
+    termM x        = Right (Term $ fromRight x)
+                             where fromRight :: Either a b -> b
+                                   fromRight (Right x) = x
+                                   fromRight _ = error "fromRight: Left"
+
+instance ParamFunctor [] where
+    {-# NOINLINE [1] termM #-}
+    termM [] = []
+    termM l  = Term (head l) : termM (tail l)
diff --git a/src/Data/Comp/Param/Thunk.hs b/src/Data/Comp/Param/Thunk.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Param/Thunk.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, GADTs #-}
+
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Param.Thunk
+-- Copyright   :  (c) 2011 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This modules defines terms & contexts with thunks, with deferred
+-- monadic computations.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Param.Thunk
+    (TermT
+    ,TrmT
+    ,CxtT
+    ,Thunk
+    ,thunk
+    ,whnf
+    ,whnf'
+    ,whnfPr
+    ,nf
+    ,nfT
+    ,nfPr
+    ,nfTPr
+    ,evalStrict
+    ,AlgT
+    ,strict
+    ,strict')
+ where
+
+import Data.Comp.Param.Term
+import Data.Comp.Param.Sum
+import Data.Comp.Param.Ops
+import Data.Comp.Param.Algebra
+import Data.Comp.Param.Ditraversable
+import Data.Comp.Param.Difunctor
+
+import Control.Monad
+
+-- | This type represents terms with thunks.
+type TermT m f = Term (Thunk m :+: f)
+
+-- | This type represents terms with thunks.
+type TrmT m f a = Trm  (Thunk m :+: f) a
+
+-- | This type represents contexts with thunks.
+type CxtT h  m f a = Cxt h (Thunk m :+: f) a
+
+newtype Thunk m a b = Thunk (m b)
+
+-- | This function turns a monadic computation into a thunk.
+thunk :: (Thunk m :<: f) => m (Cxt h f a b) -> Cxt h f a b
+thunk = inject . Thunk
+
+-- | This function evaluates all thunks until a non-thunk node is
+-- found.
+whnf :: Monad m => TrmT m f a -> m (Either a (f a (TrmT m f a)))
+whnf (In (Inl (Thunk m))) = m >>= whnf
+whnf (In (Inr t)) = return $ Right t
+whnf (Var x) = return $ Left x
+
+whnf' :: Monad m => TrmT m f a -> m (TrmT m f a)
+whnf' =  liftM (either Var inject) . whnf
+
+-- | This function first evaluates the argument term into whnf via
+-- 'whnf' and then projects the top-level signature to the desired
+-- subsignature. Failure to do the projection is signalled as a
+-- failure in the monad.
+whnfPr :: (Monad m, g :<: f) => TrmT m f a -> m (g a (TrmT m f a))
+whnfPr t = do res <- whnf t
+              case res of
+                Left _  -> fail "cannot project variable"
+                Right t ->
+                    case proj t of
+                      Just res' -> return res'
+                      Nothing -> fail "projection failed"
+
+
+-- | This function evaluates all thunks.
+nfT :: (ParamFunctor m, Monad m, Ditraversable f) => TermT m f -> m (Term f)
+nfT t = termM $ nf $ unTerm  t
+
+-- | This function evaluates all thunks.
+nf :: (Monad m, Ditraversable f) => TrmT m f a -> m (Trm f a)
+nf = either (return . Var) (liftM In . dimapM nf) <=< whnf
+
+-- | This function evaluates all thunks while simultaneously
+-- projecting the term to a smaller signature. Failure to do the
+-- projection is signalled as a failure in the monad as in 'whnfPr'.
+nfTPr :: (ParamFunctor m, Monad m, Ditraversable g, g :<: f) => TermT m f -> m (Term g)
+nfTPr t = termM $ nfPr $ unTerm t
+
+-- | This function evaluates all thunks while simultaneously
+-- projecting the term to a smaller signature. Failure to do the
+-- projection is signalled as a failure in the monad as in 'whnfPr'.
+nfPr :: (Monad m, Ditraversable g, g :<: f) => TrmT m f a -> m (Trm g a)
+nfPr = liftM In . dimapM nfPr <=< whnfPr
+
+
+evalStrict :: (Ditraversable g, Monad m, g :<: f) => 
+              (g (TrmT m f a) (f a (TrmT m f a)) -> TrmT m f a)
+           -> g (TrmT m f a) (TrmT m f a) -> TrmT m f a
+evalStrict cont t = thunk $ do 
+                      t' <- dimapM (liftM (either (const Nothing) Just) . whnf) t
+                      case disequence t' of
+                        Nothing -> return $ inject' t
+                        Just s -> return $ cont s
+                      
+
+-- | This type represents algebras which have terms with thunks as
+-- carrier.
+type AlgT m f g = Alg f (TermT m g)
+
+-- | This combinator makes the evaluation of the given functor
+-- application strict by evaluating all thunks of immediate subterms.
+strict :: (f :<: g, Ditraversable f, Monad m) => f a (TrmT m g a) -> TrmT m g a
+strict x = thunk $ liftM inject $ dimapM whnf' x
+
+-- | This combinator makes the evaluation of the given functor
+-- application strict by evaluating all thunks of immediate subterms.
+strict' :: (f :<: g, Ditraversable f, Monad m) => f (TrmT m g a) (TrmT m g a) -> TrmT m g a
+strict'  = strict . dimap Var id
diff --git a/testsuite/tests/Data/Comp/Examples/MultiParam.hs b/testsuite/tests/Data/Comp/Examples/MultiParam.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Examples/MultiParam.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE TypeOperators #-}
+module Data.Comp.Examples.MultiParam where
+
+import Examples.Multi.FOL as FOL
+
+import Data.Comp.Param.Multi
+import Data.Comp.Param.Multi.FreshM (Name)
+
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.HUnit
+
+
+
+
+
+
+--------------------------------------------------------------------------------
+-- Test Suits
+--------------------------------------------------------------------------------
+
+tests = testGroup "Parametric Compositional Data Types" [
+         testCase "FOL" folTest
+        ]
+
+
+--------------------------------------------------------------------------------
+-- Properties
+--------------------------------------------------------------------------------
+
+folTest = show (foodFact7 :: INF Name TFormula) @=? "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Person(Skol6(x2)))\n" ++
+          "(Person(x1) and Food(x2)) -> (Food(Skol2(x1)) or Eats(Skol6(x2), x2))\n" ++
+                                                                                        "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Person(Skol6(x2)))\n" ++
+                                                                                        "(Person(x1) and Eats(x1, Skol2(x1)) and Food(x2)) -> (Eats(Skol6(x2), x2))"
diff --git a/testsuite/tests/Data/Comp/Examples/Param.hs b/testsuite/tests/Data/Comp/Examples/Param.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Examples/Param.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TypeOperators #-}
+module Data.Comp.Examples.Param where
+
+import Examples.Names as Names
+import Examples.Graph as Graph
+
+import Data.Comp.Param
+
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.HUnit
+
+
+
+
+
+
+--------------------------------------------------------------------------------
+-- Test Suits
+--------------------------------------------------------------------------------
+
+tests = testGroup "Parametric Compositional Data Types" [
+         testCase "names" namesTest,
+         testCase "graph" graphTest
+        ]
+
+
+--------------------------------------------------------------------------------
+-- Properties
+--------------------------------------------------------------------------------
+
+instance (EqD f, PEq p) => EqD (f :&: p) where
+    eqD (v1 :&: p1) (v2 :&: p2) = do b1 <- peq p1 p2
+                                     b2 <- eqD v1 v2
+                                     return $ b1 && b2
+
+namesTest = sequence_ [en @=? en', ep @=? ep']
+graphTest = sequence_ [n @=? 5, f @=? [0,2,1,2]]
diff --git a/testsuite/tests/Data/Comp/Examples_Test.hs b/testsuite/tests/Data/Comp/Examples_Test.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Data/Comp/Examples_Test.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeOperators #-}
+module Data.Comp.Examples_Test where
+
+import qualified Data.Comp.Examples.Param as P
+import qualified Data.Comp.Examples.MultiParam as MP
+
+import Test.Framework
+
+tests = testGroup "Examples" [
+         P.tests,
+         MP.tests
+       ]
diff --git a/testsuite/tests/Tests.hs b/testsuite/tests/Tests.hs
new file mode 100644
--- /dev/null
+++ b/testsuite/tests/Tests.hs
@@ -0,0 +1,18 @@
+module Main where
+
+import Test.Framework
+import qualified Data.Comp.Examples_Test
+
+--------------------------------------------------------------------------------
+-- Test Suits
+--------------------------------------------------------------------------------
+
+main = defaultMain [tests]
+
+tests = testGroup "Data.Comp" [
+         Data.Comp.Examples_Test.tests
+       ]
+
+--------------------------------------------------------------------------------
+-- Properties
+--------------------------------------------------------------------------------