diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2008 Universiteit Utrecht
+Copyright (c) 2008--2009 Universiteit Utrecht
 
 All rights reserved.
 
diff --git a/examples/AST.hs b/examples/AST.hs
--- a/examples/AST.hs
+++ b/examples/AST.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE EmptyDataDecls        #-}
 
 module AST where
 
@@ -22,58 +23,8 @@
 
 data Decl   =  Var := Expr
             |  Seq    Decl  Decl
+            |  None
   deriving Show
 
 type Var   =  String
-
--- * Instantiating the library for AST 
-
-data AST :: * -> * where
-  Expr  ::  AST Expr
-  Decl  ::  AST Decl
-  Var   ::  AST Var
-
-type instance PF AST  =    
-                   K Int                  :>:  Expr  -- |Const|
-              :+:  (I Expr :*: I Expr)    :>:  Expr  -- |Add|
-              :+:  (I Expr :*: I Expr)    :>:  Expr  -- |Mul|
-              :+:  I Var                  :>:  Expr  -- |EVar|
-              :+:  (I Decl :*: I Expr)    :>:  Expr  -- |Let|
-              :+:  (I Var :*: I Expr)     :>:  Decl  -- |:=|
-              :+:  (I Decl :*: I Decl)    :>:  Decl  -- |Seq|
-              :+:  K String               :>:  Var   -- |V|
-
-instance Ix AST Expr where
-
-  from_ (Const i)   =  L                     (Tag (K i))
-  from_ (Add e f)   =  R (L                  (Tag (I (I0 e) :*: I (I0 f))))
-  from_ (Mul e f)   =  R (R (L               (Tag (I (I0 e) :*: I (I0 f)))))
-  from_ (EVar x)    =  R (R (R (L            (Tag (I (I0 x))))))
-  from_ (Let d e)   =  R (R (R (R (L         (Tag (I (I0 d) :*: I (I0 e)))))))
-
-  to_ (L                     (Tag (K i)))                        =  Const i
-  to_ (R (L                  (Tag (I (I0 e) :*: I (I0 f)))))     =  Add e f
-  to_ (R (R (L               (Tag (I (I0 e) :*: I (I0 f))))))    =  Mul e f
-  to_ (R (R (R (L            (Tag (I (I0 x)))))))                =  EVar x
-  to_ (R (R (R (R (L         (Tag (I (I0 d) :*: I (I0 e))))))))  =  Let d e
-  
-  index  =  Expr
-
-instance Ix AST Decl where
-
-  from_ (x := e)    =  R (R (R (R (R (L      (Tag (I (I0 x) :*: I (I0 e))))))))
-  from_ (Seq c d)   =  R (R (R (R (R (R (L   (Tag (I (I0 c) :*: I (I0 d)))))))))
-
-  to_ (R (R (R (R (R (L      (Tag (I (I0 x) :*: I (I0 e))))))))) =  x := e
-  to_ (R (R (R (R (R (R (L   (Tag (I (I0 c) :*: I (I0 d))))))))))=  Seq c d
-
-  index  =  Decl
-
-instance Ix AST Var where
-
-  from_ x           =  R (R (R (R (R (R (R(Tag (K x))))))))
-
-  to_ (R (R (R (R (R (R (R(Tag (K x)))))))))           =  x
-
-  index  =  Var
 
diff --git a/examples/ASTExamples.hs b/examples/ASTExamples.hs
--- a/examples/ASTExamples.hs
+++ b/examples/ASTExamples.hs
@@ -7,16 +7,23 @@
 import Control.Arrow ((>>>))
 import Control.Monad ((>=>))
 
+-- Replace ASTUse with ASTTHUse below if you want
+-- to test TH code generation.
 import AST
+import ASTUse
+-- import ASTTHUse
 
 import Generics.MultiRec.Base
 import Generics.MultiRec.Compos
-import Generics.MultiRec.Fold
+import qualified Generics.MultiRec.Fold as F
+import Generics.MultiRec.Fold (con, tag)
+import Generics.MultiRec.FoldAlg as FA
 import Generics.MultiRec.Eq
+import Generics.MultiRec.Show as GS
 
 -- | Example expression
 
-example = Let ("x" := Mul (Const 6) (Const 9))
+example = Let (Seq ("x" := Mul (Const 6) (Const 9)) None)
               (Add (EVar "x") (EVar "y"))
 
 -- | Renaming variables using 'compos'
@@ -44,27 +51,62 @@
 
 -- | Algebra for evaluating an expression
 
-evalAlgebra :: Algebra AST Value
-evalAlgebra _ =  
-     tag (\ (K x)                   -> EV (const x))
-  &  tag (\ (I (EV x) :*: I (EV y)) -> EV (\ env -> x env  +  y env))
-  &  tag (\ (I (EV x) :*: I (EV y)) -> EV (\ env -> x env  *  y env))
-  &  tag (\ (I (VV x))              -> EV (fromJust . lookup x))
-  &  tag (\ (I (DV e) :*: I (EV x)) -> EV (\ env -> x (e env)))
-  &  tag (\ (I (VV x) :*: I (EV v)) -> DV (\ env -> (x, v env) : env ))
-  &  tag (\ (I (DV f) :*: I (DV g)) -> DV (g . f))
-  &  tag (\ (K x)                   -> VV x)
+infixr 5 &.
 
+(&.) = (F.&)
+
+evalAlgebra1 :: F.Algebra AST Value
+evalAlgebra1 _ =  
+ 
+      tag  (   con (\ (K x)                   -> EV (const x))
+           &.  con (\ (I (EV x) :*: I (EV y)) -> EV (\ env -> x env  +  y env))
+           &.  con (\ (I (EV x) :*: I (EV y)) -> EV (\ env -> x env  *  y env))
+           &.  con (\ (I (VV x))              -> EV (fromJust . lookup x))
+           &.  con (\ (I (DV e) :*: I (EV x)) -> EV (\ env -> x (e env)))
+           )
+  &.  tag  (   con (\ (I (VV x) :*: I (EV v)) -> DV (\ env -> (x, v env) : env ))
+           &.  con (\ (I (DV f) :*: I (DV g)) -> DV (g . f))
+           &.  con (\ U                       -> DV id)
+           )
+  &.  tag          (\ (K x)                   -> VV x)
+
+-- | More convenient algebra for evaluating an expression
+
+evalAlgebra2 :: FA.Algebra AST Value
+evalAlgebra2 _ =
+
+     (  (\ x             -> EV (const x))
+     &  (\ (EV x) (EV y) -> EV (\ env -> x env  +  y env))
+     &  (\ (EV x) (EV y) -> EV (\ env -> x env  *  y env))
+     &  (\ (VV x)        -> EV (fromJust . lookup x))
+     &  (\ (DV e) (EV x) -> EV (\ env -> x (e env)))
+     )
+  &  (  (\ (VV x) (EV v) -> DV (\ env -> (x, v env) : env ))
+     &  (\ (DV f) (DV g) -> DV (g . f))
+     &  (                   DV id)
+     )
+  &     (\ x             -> VV x)
+
 -- | Evaluator
 
-eval :: Expr -> Env -> Int
-eval x = let (EV f) = fold evalAlgebra x in f
+eval1 :: Expr -> Env -> Int
+eval1 x = let (EV f) = F.fold evalAlgebra1 x in f
 
--- | Test for 'eval'
+-- | Evaluator
 
-testEval :: Int
-testEval = eval example [("y", -12)] 
+eval2 :: Expr -> Env -> Int
+eval2 x = let (EV f) = FA.fold evalAlgebra2 x in f
 
+-- | Test for 'eval1'
+
+testEval1 :: Int
+testEval1 = eval1 example [("y", -12)] 
+
+-- | Test for 'eval2'
+
+testEval2 :: Int
+testEval2 = eval2 example [("y", -12)] 
+
 -- | Equality instance for 'Expr'
 
 instance Eq Expr where
@@ -74,3 +116,8 @@
 
 testEq :: (Bool, Bool)
 testEq = (example == example, example == testRename)
+
+-- | Test for generic show
+
+testShow :: IO ()
+testShow = putStrLn $ GS.show Expr example
diff --git a/examples/ASTTHUse.hs b/examples/ASTTHUse.hs
new file mode 100644
--- /dev/null
+++ b/examples/ASTTHUse.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE TemplateHaskell       #-}
+
+module ASTTHUse where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.TH
+import AST
+
+-- * Instantiating the library for AST using TH
+
+-- ** Index type
+
+data AST :: * -> * where
+  Expr  ::  AST Expr
+  Decl  ::  AST Decl
+  Var   ::  AST Var
+
+-- ** Constructors
+
+$(deriveConstructors [''Expr, ''Decl, ''Var])
+
+-- ** Functor encoding and 'Ix' instances
+
+$(deriveSystem ''AST [''Expr, ''Decl, ''Var] "PFAST")
+type instance PF AST = PFAST
+
diff --git a/examples/ASTUse.hs b/examples/ASTUse.hs
new file mode 100644
--- /dev/null
+++ b/examples/ASTUse.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE EmptyDataDecls        #-}
+
+module ASTUse where
+
+import Generics.MultiRec.Base
+import AST
+
+-- * Instantiating the library for AST 
+
+-- ** Index type
+
+data AST :: * -> * where
+  Expr  ::  AST Expr
+  Decl  ::  AST Decl
+  Var   ::  AST Var
+
+-- ** Constructors
+
+data Const
+instance Constructor Const  where conName _ = "Const"
+data Add
+instance Constructor Add    where conName _ = "Add"
+data Mul
+instance Constructor Mul    where conName _ = "Mul"
+data EVar
+instance Constructor EVar   where conName _ = "EVar"
+data Let
+instance Constructor Let    where conName _ = "Let"
+data Assign
+instance Constructor Assign where
+  conName _ = ":="
+  conFixity _ = Infix NotAssociative 1
+data Seq
+instance Constructor Seq   where conName _ = "Seq"
+data None
+instance Constructor None  where conName _ = "None"
+
+-- ** Functor encoding
+
+-- Variations of the encoding below are possible. For instance,
+-- the 'C' applications can be omitted if no functions that require
+-- constructor information are needed. Furthermore, it is possible
+-- to tag every constructor rather than every datatype. That makes
+-- the overall structure slightly simpler, but makes the nesting
+-- of 'L' and 'R' constructors larger in turn.
+
+type instance PF AST  =    
+      (     C Const   (K Int)
+       :+:  C Add     (I Expr :*: I Expr)
+       :+:  C Mul     (I Expr :*: I Expr)
+       :+:  C EVar    (I Var)
+       :+:  C Let     (I Decl :*: I Expr)
+      ) :>: Expr
+  :+: (     C Assign  (I Var  :*: I Expr)
+       :+:  C Seq     (I Decl :*: I Decl)
+       :+:  C None    U
+      ) :>: Decl
+  :+: (               (K String)
+      ) :>: Var
+
+-- ** 'Ix' instances
+
+instance Ix AST Expr where
+
+  from_ (Const i)  =  L (Tag (L          (C (K i))))
+  from_ (Add e f)  =  L (Tag (R (L       (C (I (I0 e) :*: I (I0 f))))))
+  from_ (Mul e f)  =  L (Tag (R (R (L    (C (I (I0 e) :*: I (I0 f)))))))
+  from_ (EVar x)   =  L (Tag (R (R (R (L (C (I (I0 x))))))))
+  from_ (Let d e)  =  L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e))))))))
+
+  to_ (L (Tag (L          (C (K i)))))                       =  Const i
+  to_ (L (Tag (R (L       (C (I (I0 e) :*: I (I0 f)))))))    =  Add e f
+  to_ (L (Tag (R (R (L    (C (I (I0 e) :*: I (I0 f))))))))   =  Mul e f
+  to_ (L (Tag (R (R (R (L (C (I (I0 x)))))))))               =  EVar x
+  to_ (L (Tag (R (R (R (R (C (I (I0 d) :*: I (I0 e)))))))))  =  Let d e
+
+  index  =  Expr
+
+instance Ix AST Decl where
+
+  from_ (x := e)   =  R (L (Tag (L    (C (I (I0 x) :*: I (I0 e))))))
+  from_ (Seq c d)  =  R (L (Tag (R (L (C (I (I0 c) :*: I (I0 d)))))))
+  from_ (None)     =  R (L (Tag (R (R (C U)))))
+
+  to_ (R (L (Tag (L    (C (I (I0 x) :*: I (I0 e)))))))   =  x := e
+  to_ (R (L (Tag (R (L (C (I (I0 c) :*: I (I0 d))))))))  = Seq c d
+  to_ (R (L (Tag (R (R (C U))))))                        = None
+
+  index  =  Decl
+
+instance Ix AST Var where
+
+  from_ x  =  R (R (Tag (K x)))
+
+  to_ (R (R (Tag (K x))))  =  x
+
+  index  =  Var
+
diff --git a/examples/Single.hs b/examples/Single.hs
new file mode 100644
--- /dev/null
+++ b/examples/Single.hs
@@ -0,0 +1,16 @@
+module Single where
+
+import Generics.MultiRec.Base
+
+
+-- * A single datatype
+
+data Logic = Var String
+           | Logic :->:  Logic            -- implication
+           | Logic :<->: Logic            -- equivalence
+           | Logic :&&:  Logic            -- and (conjunction)
+           | Logic :||:  Logic            -- or (disjunction)
+           | Not Logic                    -- not
+           | T                            -- true
+           | F                            -- false
+ deriving (Show, Eq, Ord)
diff --git a/examples/SingleExamples.hs b/examples/SingleExamples.hs
new file mode 100644
--- /dev/null
+++ b/examples/SingleExamples.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE FlexibleContexts      #-}
+
+module SingleExamples where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.FoldAlgK
+
+-- Replace SingleUse with SingleTHUse below if you want
+-- to test TH code generation.
+import SingleUse
+import Single
+
+-- | evalLogic takes a function that gives a logic values to variables,
+-- | and a Logic expression, and evaluates it.
+evalLogic :: (String -> Bool) -> Logic -> Bool
+evalLogic env = fold algebra 
+ where
+   algebra :: Algebra LogicF Bool
+   algebra _ = env & impl & (==) & (&&) & (||) & not & True & False
+
+   impl p q = not p || q
diff --git a/examples/SingleTHUse.hs b/examples/SingleTHUse.hs
new file mode 100644
--- /dev/null
+++ b/examples/SingleTHUse.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module SingleTHUse where
+
+import Single
+import Generics.MultiRec.Base
+import Generics.MultiRec.TH
+
+
+-- * Instantiating multirec for Logic using TH
+-- ** Index type
+data LogicF :: * -> * where
+  Logic :: LogicF Logic
+
+-- ** Constructors
+$(deriveConstructors [''Logic])
+
+-- ** Functor encoding and 'Ix' instances
+$(deriveSystem ''LogicF [''Logic] "PFLogic")
+type instance PF LogicF = PFLogic
diff --git a/examples/SingleUse.hs b/examples/SingleUse.hs
new file mode 100644
--- /dev/null
+++ b/examples/SingleUse.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+
+module SingleUse where
+
+import Generics.MultiRec.Base
+import Single
+
+-- * Instantiating the library for Logic 
+
+-- ** Index type
+
+data LogicF :: * -> * where
+  Logic ::  LogicF Logic
+
+-- ** Constructors
+
+data Var
+instance Constructor Var   where conName _   = "Var"
+
+data Impl
+instance Constructor Impl  where
+  conName _   = ":->:"
+  conFixity _ = Infix RightAssociative 2
+
+data Equiv
+instance Constructor Equiv where
+  conName _ = ":<->:"
+  conFixity _ = Infix RightAssociative 1
+
+data And
+instance Constructor And   where
+  conName _ = ":&&:"
+  conFixity _ = Infix RightAssociative 4
+
+data Or
+instance Constructor Or    where
+  conName _ = ":||:"
+  conFixity _ = Infix RightAssociative 3
+
+data Not
+instance Constructor Not   where conName _ = "Not"
+data T
+instance Constructor T     where conName _ = "T"
+data F
+instance Constructor F     where conName _ = "F"
+
+-- ** Functor encoding
+
+type instance PF LogicF  =    
+      (     C Var   (K String)
+       :+:  C Impl  (I Logic :*: I Logic)
+       :+:  C Equiv (I Logic :*: I Logic)
+       :+:  C And   (I Logic :*: I Logic)
+       :+:  C Or    (I Logic :*: I Logic)
+       :+:  C Not   (I Logic)
+       :+:  C T     U
+       :+:  C F     U
+      ) :>: Logic
+
+-- ** 'Ix' instances
+
+instance Ix LogicF Logic where
+
+  from_ (Var s)       = Tag (L                   (C (K s)))
+  from_ (l1 :->: l2)  = Tag (R (L                (C (I (I0 l1) :*: I (I0 l2)))))
+  from_ (l1 :<->: l2) = Tag (R (R (L             (C (I (I0 l1) :*: I (I0 l2))))))
+  from_ (l1 :&&: l2)  = Tag (R (R (R (L          (C (I (I0 l1) :*: I (I0 l2)))))))
+  from_ (l1 :||: l2)  = Tag (R (R (R (R (L       (C (I (I0 l1) :*: I (I0 l2))))))))
+  from_ (Not l)       = Tag (R (R (R (R (R (L    (C (I (I0 l)))))))))
+  from_ T             = Tag (R (R (R (R (R (R (L (C U))))))))
+  from_ F             = Tag (R (R (R (R (R (R (R (C U))))))))
+
+  to_ (Tag (L                   (C (K s))))                         = Var s
+  to_ (Tag (R (L                (C (I (I0 l1) :*: I (I0 l2))))))    = l1 :->: l2
+  to_ (Tag (R (R (L             (C (I (I0 l1) :*: I (I0 l2)))))))   = l1 :<->: l2
+  to_ (Tag (R (R (R (L          (C (I (I0 l1) :*: I (I0 l2))))))))  = l1 :&&: l2
+  to_ (Tag (R (R (R (R (L       (C (I (I0 l1) :*: I (I0 l2))))))))) = l1 :||: l2
+  to_ (Tag (R (R (R (R (R (L    (C (I (I0 l))))))))))               = Not l
+  to_ (Tag (R (R (R (R (R (R (L (C U)))))))))                       = T
+  to_ (Tag (R (R (R (R (R (R (R (C U)))))))))                       = F
+
+  index  =  Logic
diff --git a/multirec.cabal b/multirec.cabal
--- a/multirec.cabal
+++ b/multirec.cabal
@@ -1,5 +1,5 @@
 name:			multirec
-version:		0.1
+version:		0.2
 license:		BSD3
 license-file:		LICENSE
 author:			Alexey Rodriguez,
@@ -21,7 +21,7 @@
   .
   With the multirec library, we provide a mechanism to talk about fixed
   points of systems of datatypes that may be mutually recursive. On top
-  of this representations, generic functions such as the fold or the zipper
+  of this representations, generic functions such as the fold or the Zipper
   can then be defined.
   .
   We expect that the library will be especially interesting for compiler
@@ -38,20 +38,35 @@
 stability:		experimental
 build-type:		Simple
 cabal-version:		>= 1.2.1
-tested-with:		GHC == 6.8.3
+tested-with:		GHC == 6.8.3, GHC == 6.10.1
 hs-source-dirs:		src
 exposed-modules:	Generics.MultiRec
 
 			-- Base
                         Generics.MultiRec.Base
+			Generics.MultiRec.Constructor
+                        Generics.MultiRec.TH
 
 			-- Generic functions
+			Generics.MultiRec.ConNames
 			Generics.MultiRec.HFunctor
+			Generics.MultiRec.HFix
 			Generics.MultiRec.Fold
+			Generics.MultiRec.FoldK
+			Generics.MultiRec.FoldAlg
+			Generics.MultiRec.FoldAlgK
 			Generics.MultiRec.Compos
 			Generics.MultiRec.Eq
+			Generics.MultiRec.Show
 
 extra-source-files:	examples/AST.hs
+                        examples/ASTUse.hs
+                        examples/ASTTHUse.hs
 			examples/ASTExamples.hs
+			examples/Single.hs
+			examples/SingleUse.hs
+			examples/SingleTHUse.hs
+			examples/SingleExamples.hs
 			CREDITS
-build-depends:		base >= 3.0 
+build-depends:		base >= 3.0 && < 4,
+                        template-haskell >= 2.2 && < 2.4
diff --git a/src/Generics/MultiRec/Base.hs b/src/Generics/MultiRec/Base.hs
--- a/src/Generics/MultiRec/Base.hs
+++ b/src/Generics/MultiRec/Base.hs
@@ -9,7 +9,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Base
--- Copyright   :  (c) 2008 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -29,9 +29,13 @@
 module Generics.MultiRec.Base 
   (-- * Structure types
    I(..), unI,
-   K(..), (:+:)(..), (:*:)(..),
+   K(..), U(..), (:+:)(..), (:*:)(..),
    (:>:)(..), unTag,
+   C(..), unC,
 
+   -- ** Constructor information
+   module Generics.MultiRec.Constructor,
+
    -- ** Unlifted variants
    I0(..), K0(..),
 
@@ -40,6 +44,7 @@
   ) where
 
 import Control.Applicative
+import Generics.MultiRec.Constructor
 
 -- * Structure types
 
@@ -59,6 +64,9 @@
 -- | Represents constant types that do not belong to the system.
 data K a       (s :: * -> *) (r :: * -> *) ix = K {unK :: a}
 
+-- | Represents constructors without fields.
+data U         (s :: * -> *) (r :: * -> *) ix = U
+
 -- | Represents sums (choices between constructors).
 data (f :+: g) (s :: * -> *) (r :: * -> *) ix = L (f s r ix) | R (g s r ix)
 
@@ -74,6 +82,14 @@
 unTag :: (f :>: ix) s r ix -> f s r ix
 unTag (Tag x) = x
 
+-- | Represents constructors.
+data C c f     (s :: * -> *) (r :: * -> *) ix where
+  C :: (Constructor c) => f s r ix -> C c f s r ix
+
+-- | Destructor for 'C'.
+unC :: C c f s r ix -> f s r ix
+unC (C x) = x
+
 -- ** Unlifted variants
 
 -- | Unlifted version of 'I'.
@@ -88,6 +104,9 @@
 instance Applicative I0 where
   pure              = I0
   (I0 f) <*> (I0 x) = I0 (f x)
+
+instance Functor (K0 a) where
+  fmap f = K0 . unK0
 
 -- * Indexed systems
 
diff --git a/src/Generics/MultiRec/Compos.hs b/src/Generics/MultiRec/Compos.hs
--- a/src/Generics/MultiRec/Compos.hs
+++ b/src/Generics/MultiRec/Compos.hs
@@ -4,7 +4,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Compos
--- Copyright   :  (c) 2008 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -18,6 +18,7 @@
 --   ICFP 2006
 --
 -----------------------------------------------------------------------------
+
 module Generics.MultiRec.Compos where
 
 import Control.Monad (liftM)
diff --git a/src/Generics/MultiRec/ConNames.hs b/src/Generics/MultiRec/ConNames.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/ConNames.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes       #-}
+{-# LANGUAGE TypeOperators    #-}
+{-# LANGUAGE KindSignatures   #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSignatures #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.ConNames
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Generic function that returns the constructor names available in a system
+-- of datatypes.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.ConNames where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.Constructor
+
+class ConNames (f :: (* -> *) -> (* -> *) -> * -> *) where
+  hconNames :: f s r ix -> [String]
+
+instance Constructor c => ConNames (C c f) where
+  hconNames c = [conName c]
+
+instance (ConNames f, ConNames g) => ConNames (f :+: g) where
+  hconNames (_ :: (f :+: g) r s ix) = hconNames (undefined :: f r s ix) ++
+                                      hconNames (undefined :: g r s ix)
+
+instance ConNames (K x) where
+  hconNames _ = []
+
+instance ConNames U where
+  hconNames _ = []
+
+instance ConNames (f :*: g) where
+  hconNames _ = []
+
+instance ConNames (I a) where
+  hconNames _ = []
+
+instance (ConNames f) => ConNames (f :>: ix) where
+  hconNames (_ :: (f :>: ix) r s xi) = hconNames (undefined :: f r s ix)
+
+conNames :: forall s ix . (Ix s ix, ConNames (PF s)) => s ix -> [String]
+conNames s = hconNames (undefined :: PF s s I0 ix)
diff --git a/src/Generics/MultiRec/Constructor.hs b/src/Generics/MultiRec/Constructor.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/Constructor.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE KindSignatures #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.Constructor
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module contains a class for datatypes that represent data
+-- constructors.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.Constructor
+  (Constructor(..), Fixity(..), Associativity(..)
+  ) where
+
+-- | Class for datatypes that represent data constructors.
+-- For non-symbolic constructors, only 'conName' has to be defined.
+-- The weird argument is supposed to be instantiated with 'C' from
+-- base, hence the complex kind.
+class Constructor c where
+  conName   :: t c (f :: (* -> *) -> (* -> *) -> * -> *) (s :: * -> *) (r :: * -> *) ix -> String
+  conFixity :: t c (f :: (* -> *) -> (* -> *) -> * -> *) (s :: * -> *) (r :: * -> *) ix -> Fixity
+  conFixity = const Prefix
+
+-- | Datatype to represent the fixity of a constructor. An infix declaration
+-- directly corresponds to an application of 'Infix'.
+data Fixity = Prefix | Infix Associativity Int
+  deriving (Eq, Show, Ord, Read)
+
+data Associativity = LeftAssociative | RightAssociative | NotAssociative
+  deriving (Eq, Show, Ord, Read)
+
diff --git a/src/Generics/MultiRec/Eq.hs b/src/Generics/MultiRec/Eq.hs
--- a/src/Generics/MultiRec/Eq.hs
+++ b/src/Generics/MultiRec/Eq.hs
@@ -1,12 +1,11 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes       #-}
 {-# LANGUAGE TypeOperators    #-}
-{-# LANGUAGE TypeFamilies     #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Eq
--- Copyright   :  (c) 2008 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -16,6 +15,7 @@
 -- Generic equality.
 --
 -----------------------------------------------------------------------------
+
 module Generics.MultiRec.Eq where
 
 import Generics.MultiRec.Base
@@ -30,9 +30,14 @@
 instance HEq (I xi) where
   heq _ eq (I x1) (I x2) = eq index x1 x2
 
+-- | For constant types, we make use of the standard
+-- equality function.
 instance Eq x => HEq (K x) where
   heq _ eq (K x1) (K x2) = x1 == x2
 
+instance HEq U where
+  heq _ eq U U = True
+
 instance (HEq f, HEq g) => HEq (f :+: g) where
   heq ix eq (L x1) (L x2) = heq ix eq x1 x2
   heq ix eq (R y1) (R y2) = heq ix eq y1 y2
@@ -44,6 +49,9 @@
 -- The following instance does not compile with ghc-6.8.2
 instance HEq f => HEq (f :>: ix) where
   heq ix eq (Tag x1) (Tag x2) = heq ix eq x1 x2
+
+instance HEq f => HEq (C c f) where
+  heq ix eq (C x1) (C x2) = heq ix eq x1 x2
 
 eq :: (Ix s ix, HEq (PF s)) => s ix -> ix -> ix -> Bool
 eq ix x1 x2 = heq ix (\ ix (I0 x1) (I0 x2) -> eq ix x1 x2) (from x1) (from x2)
diff --git a/src/Generics/MultiRec/Fold.hs b/src/Generics/MultiRec/Fold.hs
--- a/src/Generics/MultiRec/Fold.hs
+++ b/src/Generics/MultiRec/Fold.hs
@@ -4,19 +4,29 @@
 {-# LANGUAGE KindSignatures      #-}
 {-# LANGUAGE LiberalTypeSynonyms #-}
 {-# LANGUAGE GADTs               #-}
+{-# LANGUAGE TypeFamilies        #-}
 
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.Fold
--- Copyright   :  (c) 2008 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- The definition of generic fold.
+-- The definition of generic fold, unfold, paramorphisms. In addition,
+-- some combinators that facilitate the construction of algebras.
 --
+-- There are several variants of fold in other modules that are probably
+-- easier to use:
+--
+--   * for folds with constant return type, look at 
+--     "Generics.MultiRec.FoldAlgK" (or "Generics.MultiRec.FoldK"),
+--
+--   * for other folds, look at "Generics.MultiRec.FoldAlg".
+--
 -----------------------------------------------------------------------------
 
 module Generics.MultiRec.Fold where
@@ -24,26 +34,53 @@
 import Generics.MultiRec.Base
 import Generics.MultiRec.HFunctor
 
+import Control.Monad hiding (foldM)
+import Control.Applicative
+
 -- * Generic fold and unfold
 
-type Algebra s r = forall ix. Ix s ix => s ix -> PF s s r ix -> r ix
+type Algebra'  s f   r = forall ix. Ix s ix => s ix -> f s r ix -> r ix
+type Algebra   s     r = Algebra' s (PF s) r
+type AlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s r ix -> g (r ix)
+type AlgebraF  s   g r = AlgebraF' s (PF s) g r
 
 fold :: (Ix s ix, HFunctor (PF s)) =>
         Algebra s r -> ix -> r ix
 fold f = f index . hmap (\ _ (I0 x) -> fold f x) . from
 
-type CoAlgebra s r = forall ix. Ix s ix => s ix -> r ix -> PF s s r ix
+foldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
+         AlgebraF s m r -> ix -> m (r ix)
+foldM f x = hmapM (\ _ (I0 x) -> foldM f x) (from x) >>= f index
 
+type CoAlgebra'  s f   r = forall ix. Ix s ix => s ix -> r ix -> f s r ix
+type CoAlgebra   s     r = CoAlgebra' s (PF s) r
+type CoAlgebraF' s f g r = forall ix. Ix s ix => s ix -> r ix -> g (f s r ix)
+type CoAlgebraF  s   g r = CoAlgebraF' s (PF s) g r
+
 unfold :: (Ix s ix, HFunctor (PF s)) =>
           CoAlgebra s r -> r ix -> ix
 unfold f = to . hmap (\ _ x -> I0 (unfold f x)) . f index
 
-type ParaAlgebra s r = forall ix. Ix s ix => s ix -> PF s s r ix -> ix -> r ix
+unfoldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
+           CoAlgebraF s m r -> r ix -> m ix
+unfoldM f x = f index x >>= liftMto . hmapM (\ _ x -> liftM I0 (unfoldM f x))
+  where
+    -- only for ghc-6.8.3 compatibility
+    liftMto :: (Monad m, Ix s ix, pfs ~ PF s) => m (pfs s I0 ix) -> m ix
+    liftMto = liftM to
 
+type ParaAlgebra'  s f   r = forall ix. Ix s ix => s ix -> f s r ix -> ix -> r ix
+type ParaAlgebra   s     r = ParaAlgebra' s (PF s) r
+type ParaAlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s r ix -> ix -> g (r ix)
+type ParaAlgebraF  s   g r = ParaAlgebraF' s (PF s) g r
+
 para :: (Ix s ix, HFunctor (PF s)) => 
         ParaAlgebra s r -> ix -> r ix
 para f x = f index (hmap (\ _ (I0 x) -> para f x) (from x)) x
 
+paraM :: (Ix s ix, HFunctor (PF s), Monad m) => 
+         ParaAlgebraF s m r -> ix -> m (r ix)
+paraM f x = hmapM (\ _ (I0 x) -> paraM f x) (from x) >>= \ r -> f index r x
 
 -- * Creating an algebra
 
@@ -59,4 +96,7 @@
 
 tag :: AlgPart a s r ix -> AlgPart (a :>: ix) s r ix'
 tag f (Tag x) = f x
+
+con :: AlgPart a s r ix -> AlgPart (C c a) s r ix
+con f (C x) = f x
 
diff --git a/src/Generics/MultiRec/FoldAlg.hs b/src/Generics/MultiRec/FoldAlg.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/FoldAlg.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE LiberalTypeSynonyms   #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE FlexibleInstances     #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.FoldAlg
+-- Copyright   :  (c) 2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- A variant of fold that allows the specification of the algebra in a
+-- convenient way.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.FoldAlg where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.HFunctor
+
+-- * The type family of convenient algebras.
+
+-- | The type family we use to describe the convenient algebras.
+type family Alg (f :: (* -> *) -> (* -> *) -> * -> *) 
+                (s :: * -> *)      -- system
+                (r :: * -> *)      -- recursive positions
+                (ix :: *)          -- index
+                :: *
+
+-- | For a constant, we take the constant value to a result.
+type instance Alg (K a) (s :: * -> *) (r :: * -> *) ix = a -> r ix
+
+-- | For a unit, no arguments are available.
+type instance Alg U (s :: * -> *) (r :: * -> *) ix = r ix
+
+-- | For an identity, we turn the recursive result into a final result.
+--   Note that the index can change.
+type instance Alg (I xi) (s :: * -> *) r ix = r xi -> r ix
+
+-- | For a sum, the algebra is a pair of two algebras.
+type instance Alg (f :+: g) s r ix = (Alg f s r ix, Alg g s r ix)
+
+-- | For a product where the left hand side is a constant, we
+--   take the value as an additional argument.
+type instance Alg (K a :*: g) s r ix = a -> Alg g s r ix
+
+-- | For a product where the left hand side is an identity, we
+--   take the recursive result as an additional argument.
+type instance Alg (I xi :*: g) s r ix = r xi -> Alg g s r ix
+
+-- | A tag changes the index of the final result.
+type instance Alg (f :>: xi) s r ix = Alg f s r xi
+
+-- | Constructors are ignored.
+type instance Alg (C c f) s r ix = Alg f s r ix
+
+-- | The algebras passed to the fold have to work for all index types
+--   in the system. The additional witness argument is required only
+--   to make GHC's typechecker happy.
+type Algebra s r = forall ix. Ix s ix => s ix -> Alg (PF s) s r ix
+
+-- * The class to turn convenient algebras into standard algebras.
+
+-- | The class fold explains how to convert a convenient algebra
+--   'Alg' back into a function from functor to result, as required
+--   by the standard fold function.
+class Fold (f :: (* -> *) -> (* -> *) -> * -> *) where
+  alg :: (Ix s ix) => Alg f s r ix -> f s r ix -> r ix
+
+instance Fold (K a) where
+  alg f (K x) = f x
+
+instance Fold U where
+  alg f U     = f
+
+instance Fold (I xi) where
+  alg f (I x) = f x
+
+instance (Fold f, Fold g) => Fold (f :+: g) where
+  alg (f, g) (L x) = alg f x
+  alg (f, g) (R x) = alg g x
+
+instance (Fold g) => Fold (K a :*: g) where
+  alg f (K x :*: y) = alg (f x) y
+
+instance (Fold g) => Fold (I xi :*: g) where
+  alg f (I x :*: y) = alg (f x) y
+
+instance (Fold f) => Fold (f :>: xi) where
+  alg f (Tag x) = alg f x
+
+instance (Fold f) => Fold (C c f) where
+  alg f (C x) = alg f x
+
+-- * Interface
+
+-- | Variant of fold that takes an additional witness argument.
+fold_ :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
+         s ix ->
+         Algebra s r ->
+         ix -> r ix
+fold_ ix f = (alg :: Alg (PF s) s r ix -> (PF s) s r ix -> r ix) (f ix) .
+             hmap (\ _ (I0 x) -> fold_ index f x) .
+             from
+
+-- | Fold with convenient algebras.
+fold :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
+        Algebra s r ->
+        ix -> r ix
+fold = fold_ index
+
+-- * Construction of algebras
+
+infixr 5 &
+
+-- | For constructing algebras that are made of nested pairs rather
+--   than n-ary tuples, it is helpful to use this pairing combinator.
+(&) :: a -> b -> (a, b)
+(&) = (,)
diff --git a/src/Generics/MultiRec/FoldAlgK.hs b/src/Generics/MultiRec/FoldAlgK.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/FoldAlgK.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE LiberalTypeSynonyms   #-}
+{-# LANGUAGE Rank2Types            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE FlexibleInstances     #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.FoldAlgK
+-- Copyright   :  (c) 2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- A variant of fold that allows the specification of the algebra in a
+-- convenient way, and that fixes the result type to a constant.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.FoldAlgK where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.HFunctor
+
+-- * The type family of convenient algebras.
+
+-- | The type family we use to describe the convenient algebras.
+type family Alg (f :: (* -> *) -> (* -> *) -> * -> *) 
+                (s :: * -> *)      -- system
+                (r :: *)           -- result type
+                :: *
+
+-- | For a constant, we take the constant value to a result.
+type instance Alg (K a) (s :: * -> *) r = a -> r
+
+-- | For a unit, no arguments are available.
+type instance Alg U (s :: * -> *) r = r
+
+-- | For an identity, we turn the recursive result into a final result.
+--   Note that the index can change.
+type instance Alg (I xi) (s :: * -> *) r = r -> r
+
+-- | For a sum, the algebra is a pair of two algebras.
+type instance Alg (f :+: g) s r = (Alg f s r, Alg g s r)
+
+-- | For a product where the left hand side is a constant, we
+--   take the value as an additional argument.
+type instance Alg (K a :*: g) s r = a -> Alg g s r
+
+-- | For a product where the left hand side is an identity, we
+--   take the recursive result as an additional argument.
+type instance Alg (I xi :*: g) s r = r -> Alg g s r
+
+-- | A tag changes the index of the final result.
+type instance Alg (f :>: xi) s r = Alg f s r
+
+-- | Constructors are ignored.
+type instance Alg (C c f) s r = Alg f s r
+
+-- | The algebras passed to the fold have to work for all index types
+--   in the system. The additional witness argument is required only
+--   to make GHC's typechecker happy.
+type Algebra s r = forall ix. Ix s ix => s ix -> Alg (PF s) s r
+
+-- * The class to turn convenient algebras into standard algebras.
+
+-- | The class fold explains how to convert a convenient algebra
+--   'Alg' back into a function from functor to result, as required
+--   by the standard fold function.
+class Fold (f :: (* -> *) -> (* -> *) -> * -> *) where
+  alg :: (Ix s ix) => Alg f s r -> f s (K0 r) ix -> r
+
+instance Fold (K a) where
+  alg f (K x) = f x
+
+instance Fold U where
+  alg f U     = f
+
+instance Fold (I xi) where
+  alg f (I (K0 x)) = f x
+
+instance (Fold f, Fold g) => Fold (f :+: g) where
+  alg (f, g) (L x) = alg f x
+  alg (f, g) (R x) = alg g x
+
+instance (Fold g) => Fold (K a :*: g) where
+  alg f (K x :*: y) = alg (f x) y
+
+instance (Fold g) => Fold (I xi :*: g) where
+  alg f (I (K0 x) :*: y) = alg (f x) y
+
+instance (Fold f) => Fold (f :>: xi) where
+  alg f (Tag x) = alg f x
+
+instance (Fold f) => Fold (C c f) where
+  alg f (C x) = alg f x
+
+-- * Interface
+
+-- | Variant of fold that takes an additional witness argument.
+fold_ :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
+         s ix ->
+         Algebra s r ->
+         ix -> r
+fold_ ix f = (alg :: Alg (PF s) s r -> (PF s) s (K0 r) ix -> r) (f ix) .
+             hmap (\ _ (I0 x) -> K0 (fold_ index f x)) .
+             from
+
+-- | Fold with convenient algebras.
+fold :: forall s ix r . (Ix s ix, HFunctor (PF s), Fold (PF s)) =>
+        Algebra s r ->
+        ix -> r
+fold = fold_ index
+
+-- * Construction of algebras
+
+infixr 5 &
+
+-- | For constructing algebras that are made of nested pairs rather
+--   than n-ary tuples, it is helpful to use this pairing combinator.
+(&) :: a -> b -> (a, b)
+(&) = (,)
diff --git a/src/Generics/MultiRec/FoldK.hs b/src/Generics/MultiRec/FoldK.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/FoldK.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE KindSignatures      #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE TypeFamilies        #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.FoldK
+-- Copyright   :  (c) 2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Variant of "Generics.MultiRec.Fold" where the result type is independent of
+-- the index.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.FoldK where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.HFunctor
+
+import Control.Monad hiding (foldM)
+import Control.Applicative
+
+-- * Generic fold and unfold
+
+type Algebra'  s f   r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> r
+type Algebra   s     r = Algebra' s (PF s) r
+type AlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> g r
+type AlgebraF  s   g r = AlgebraF' s (PF s) g r
+
+fold :: (Ix s ix, HFunctor (PF s)) =>
+        Algebra s r -> ix -> r
+fold f = f index . hmap (\ _ (I0 x) -> K0 (fold f x)) . from
+
+foldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
+         AlgebraF s m r -> ix -> m r
+foldM f x = hmapM (\ _ (I0 x) -> liftM K0 (foldM f x)) (from x) >>= f index
+
+type CoAlgebra'  s f   r = forall ix. Ix s ix => s ix -> r -> f s (K0 r) ix
+type CoAlgebra   s     r = CoAlgebra' s (PF s) r
+type CoAlgebraF' s f g r = forall ix. Ix s ix => s ix -> r -> g (f s (K0 r) ix)
+type CoAlgebraF  s   g r = CoAlgebraF' s (PF s) g r
+
+unfold :: (Ix s ix, HFunctor (PF s)) =>
+          CoAlgebra s r -> r -> ix
+unfold f = to . hmap (\ _ (K0 x) -> I0 (unfold f x)) . f index
+
+unfoldM :: (Ix s ix, HFunctor (PF s), Monad m) =>
+           CoAlgebraF s m r -> r -> m ix
+unfoldM f x = f index x >>= liftMto . hmapM (\ _ (K0 x) -> liftM I0 (unfoldM f x))
+  where
+    -- only for ghc-6.8.3 compatibility
+    liftMto :: (Monad m, Ix s ix, pfs ~ PF s) => m (pfs s I0 ix) -> m ix
+    liftMto = liftM to
+
+type ParaAlgebra'  s f   r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> ix -> r
+type ParaAlgebra   s     r = ParaAlgebra' s (PF s) r
+type ParaAlgebraF' s f g r = forall ix. Ix s ix => s ix -> f s (K0 r) ix -> ix -> g r
+type ParaAlgebraF  s   g r = ParaAlgebraF' s (PF s) g r
+
+para :: (Ix s ix, HFunctor (PF s)) => 
+        ParaAlgebra s r -> ix -> r
+para f x = f index (hmap (\ _ (I0 x) -> K0 (para f x)) (from x)) x
+
+paraM :: (Ix s ix, HFunctor (PF s), Monad m) => 
+         ParaAlgebraF s m r -> ix -> m r
+paraM f x = hmapM (\ _ (I0 x) -> liftM K0 (paraM f x)) (from x) >>= \ r -> f index r x
+
+-- * Creating an algebra
+
+infixr 5 &
+infixr :->
+
+type AlgPart a (s :: * -> *) b ix = a s (K0 b) ix -> b
+type (f :-> g) (s :: * -> *) b ix = f s b ix -> g s b ix
+
+(&) :: (AlgPart a :-> AlgPart b :-> AlgPart (a :+: b)) s c ix
+(f & g) (L x) = f x
+(f & g) (R x) = g x 
+
+tag :: AlgPart a s c ix -> AlgPart (a :>: ix) s c ix'
+tag f (Tag x) = f x
+
+con :: AlgPart a s b ix -> AlgPart (C c a) s b ix
+con f (C x) = f x
diff --git a/src/Generics/MultiRec/HFix.hs b/src/Generics/MultiRec/HFix.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/HFix.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE KindSignatures   #-}
+{-# LANGUAGE TypeFamilies     #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.HFix
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Higher-order fixed point operator as well as conversion functions.
+-- It is rarely necessary to use 'HFix'. Generic functions
+-- usually convert between the original datatype and the functor directly.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.HFix where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.HFunctor
+
+-- * Fixed point of indexed types
+
+data HFix (h :: (* -> *) -> * -> *) ix = HIn { hout :: h (HFix h) ix }
+
+hfrom :: (pfs ~ PF s, Ix s ix, HFunctor (PF s)) => ix -> HFix (pfs s) ix
+hfrom = HIn . hmap (const (hfrom . unI0)) . from
+
+hto :: (pfs ~ PF s, Ix s ix, HFunctor (PF s)) => HFix (pfs s) ix -> ix
+hto = to . hmap (const (I0 . hto)) . hout
diff --git a/src/Generics/MultiRec/HFunctor.hs b/src/Generics/MultiRec/HFunctor.hs
--- a/src/Generics/MultiRec/HFunctor.hs
+++ b/src/Generics/MultiRec/HFunctor.hs
@@ -5,7 +5,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.MultiRec.HFunctor
--- Copyright   :  (c) 2008 Universiteit Utrecht
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
 -- License     :  BSD3
 --
 -- Maintainer  :  generics@haskell.org
@@ -38,6 +38,9 @@
 instance HFunctor (K x) where
   hmapA _ (K x)  = pure (K x)
 
+instance HFunctor U where
+  hmapA _ U = pure U
+
 instance (HFunctor f, HFunctor g) => HFunctor (f :+: g) where
   hmapA f (L x) = liftA L (hmapA f x)
   hmapA f (R y) = liftA R (hmapA f y)
@@ -47,6 +50,9 @@
 
 instance HFunctor f => HFunctor (f :>: ix) where
   hmapA f (Tag x) = liftA Tag (hmapA f x)
+
+instance HFunctor f => HFunctor (C c f) where
+  hmapA f (C x) = liftA C (hmapA f x)
 
 -- | The function 'hmap' takes a functor @f@. All the recursive instances
 -- in that functor are wrapped by an application of @r@. The argument to
diff --git a/src/Generics/MultiRec/Show.hs b/src/Generics/MultiRec/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/Show.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes       #-}
+{-# LANGUAGE TypeOperators    #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.Show
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Generic show.
+--
+-----------------------------------------------------------------------------
+
+module Generics.MultiRec.Show where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.HFunctor
+import Generics.MultiRec.Fold
+
+import qualified Prelude as P
+import Prelude hiding (show, showsPrec)
+
+-- * Generic show
+
+class HFunctor f => HShow f where
+  hShowsPrecAlg :: Algebra' s f (K0 [Int -> ShowS])
+
+instance HShow (I xi) where
+  hShowsPrecAlg _ (I (K0 x)) = K0 x
+
+-- | For constant types, we make use of the standard
+-- show function.
+instance Show x => HShow (K x) where
+  hShowsPrecAlg _ (K x) = K0 [\ n -> P.showsPrec n x]
+
+instance HShow U where
+  hShowsPrecAlg _ U = K0 []
+
+instance (HShow f, HShow g) => HShow (f :+: g) where
+  hShowsPrecAlg ix (L x) = hShowsPrecAlg ix x
+  hShowsPrecAlg ix (R y) = hShowsPrecAlg ix y
+
+instance (HShow f, HShow g) => HShow (f :*: g) where
+  hShowsPrecAlg ix (x :*: y) = K0 (unK0 (hShowsPrecAlg ix x) ++ unK0 (hShowsPrecAlg ix y))
+
+instance HShow f => HShow (f :>: ix) where
+  hShowsPrecAlg ix (Tag x) = hShowsPrecAlg ix x
+
+instance HShow f => HShow (C c f) where
+  hShowsPrecAlg ix cx@(C x) =
+    case conFixity cx of
+      Prefix    -> K0 [\ n -> showParen (not (null fields) && n > 10)
+                                        (spaces ((conName cx ++) : map ($ 11) fields))]
+      Infix a p -> K0 [\ n -> showParen (n > p)
+                                        (spaces (head fields p : (conName cx ++) : map ($ p) (tail fields)))]
+   where
+    fields = unK0 $ hShowsPrecAlg ix x
+
+-- | A variant of the algebra that takes an extra argument
+-- to fix the system 's' the algebra works on.
+hShowsPrecAlg_ :: (HShow f) => s ix -> Algebra' s f (K0 [Int -> ShowS])
+hShowsPrecAlg_ _ = hShowsPrecAlg 
+
+showsPrec :: forall s ix. (Ix s ix, HShow (PF s)) => s ix -> Int -> ix -> ShowS
+showsPrec ix n x = spaces (map ($ n) (unK0 (fold (hShowsPrecAlg_ ix) x)))
+
+show :: forall s ix. (Ix s ix, HShow (PF s)) => s ix -> ix -> String
+show ix x = showsPrec ix 0 x ""
+
+-- * Utilities
+
+spaces :: [ShowS] -> ShowS
+spaces []     = id
+spaces [x]    = x
+spaces (x:xs) = x . (' ':) . spaces xs
diff --git a/src/Generics/MultiRec/TH.hs b/src/Generics/MultiRec/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/MultiRec/TH.hs
@@ -0,0 +1,239 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE KindSignatures  #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.MultiRec.TH
+-- Copyright   :  (c) 2008--2009 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module contains Template Haskell code that can be used to
+-- automatically generate the boilerplate code for the multiplate
+-- library. The constructor information can be generated per datatype,
+-- the rest per system of datatypes.
+--
+-----------------------------------------------------------------------------
+
+
+module Generics.MultiRec.TH
+  ( deriveConstructors,
+    deriveSystem,
+    derivePF,
+    deriveIx
+  ) where
+
+import Generics.MultiRec.Base
+import Generics.MultiRec.Constructor
+import Language.Haskell.TH hiding (Fixity())
+import Language.Haskell.TH.Syntax (Lift(..))
+import Control.Monad
+
+-- | Given a list of datatype names, derive datatypes and 
+-- instances of class 'Constructor'.
+
+deriveConstructors :: [Name] -> Q [Dec]
+deriveConstructors =
+  liftM concat . mapM constrInstance
+
+-- | Given the name of the index GADT, the names of the
+-- types in the system, and the name (as string) for the
+-- pattern functor to derive, generate the 'Ix' and 'PF'
+-- instances. /IMPORTANT/: It is assumed that the constructors
+-- of the GADT have the same names as the datatypes in the
+-- family.
+
+deriveSystem :: Name -> [Name] -> String -> Q [Dec]
+deriveSystem n ns pfn =
+  do
+    pf <- derivePF pfn ns
+    ix <- deriveIx n ns
+    return $ pf ++ ix
+
+-- | Derive only the 'PF' instance. Not needed if 'deriveSystem'
+-- is used.
+
+derivePF :: String -> [Name] -> Q [Dec]
+derivePF pfn ns =
+    fmap (:[]) $
+    tySynD (mkName pfn) [] (foldr1 sum (map (pfType ns) ns))
+  where
+    sum :: Q Type -> Q Type -> Q Type
+    sum a b = conT ''(:+:) `appT` a `appT` b
+
+-- | Derive only the 'Ix' instances. Not needed if 'deriveSystem'
+-- is used.
+
+deriveIx :: Name -> [Name] -> Q [Dec]
+deriveIx s ns =
+  zipWithM (ixInstance s ns (length ns)) [0..] ns
+
+constrInstance :: Name -> Q [Dec]
+constrInstance n =
+  do
+    i <- reify n
+    -- runIO (print i)
+    let cs = case i of
+               TyConI (DataD _ _ _ cs _) -> cs
+               _ -> []
+    ds <- mapM mkData cs
+    is <- mapM mkInstance cs
+    return $ ds ++ is
+
+mkData :: Con -> Q Dec
+mkData (NormalC n _) =
+  dataD (cxt []) (mkName (nameBase n)) [] [] [] 
+mkData (InfixC t1 n t2) =
+  mkData (NormalC n [t1,t2])
+
+instance Lift Fixity where
+  lift Prefix      = conE 'Prefix
+  lift (Infix a n) = conE 'Infix `appE` [| a |] `appE` [| n |]
+
+instance Lift Associativity where
+  lift LeftAssociative  = conE 'LeftAssociative
+  lift RightAssociative = conE 'RightAssociative
+  lift NotAssociative   = conE 'NotAssociative
+
+mkInstance :: Con -> Q Dec
+mkInstance (NormalC n _) =
+    instanceD (cxt []) (appT (conT ''Constructor) (conT $ mkName (nameBase n)))
+      [funD 'conName [clause [wildP] (normalB (stringE (nameBase n))) []]]
+mkInstance (InfixC t1 n t2) =
+    do
+      i <- reify n
+      let fi = case i of
+                 DataConI _ _ _ f -> convertFixity f
+                 _ -> Prefix
+      instanceD (cxt []) (appT (conT ''Constructor) (conT $ mkName (nameBase n)))
+        [funD 'conName   [clause [wildP] (normalB (stringE (nameBase n))) []],
+         funD 'conFixity [clause [wildP] (normalB [| fi |]) []]]
+  where
+    convertFixity (Fixity n d) = Infix (convertDirection d) n
+    convertDirection InfixL = LeftAssociative
+    convertDirection InfixR = RightAssociative
+    convertDirection InfixN = NotAssociative
+
+pfType :: [Name] -> Name -> Q Type
+pfType ns n =
+    do
+      -- runIO $ putStrLn $ "processing " ++ show n
+      i <- reify n
+      let b = case i of
+                TyConI (DataD _ _ _ cs _) ->
+                  foldr1 sum (map (pfCon ns) cs)
+                TyConI (TySynD t _ _) ->
+                  conT ''K `appT` conT t
+                _ -> error "unknown construct" 
+      appT (appT (conT ''(:>:)) b) (conT $ mkName (nameBase n))
+  where
+    sum :: Q Type -> Q Type -> Q Type
+    sum a b = conT ''(:+:) `appT` a `appT` b
+
+pfCon :: [Name] -> Con -> Q Type
+pfCon ns (NormalC n []) =
+    appT (appT (conT ''C) (conT $ mkName (nameBase n))) (conT ''U)
+pfCon ns (NormalC n fs) =
+    appT (appT (conT ''C) (conT $ mkName (nameBase n))) (foldr1 prod (map (pfField ns . snd) fs))
+  where
+    prod :: Q Type -> Q Type -> Q Type
+    prod a b = conT ''(:*:) `appT` a `appT` b
+pfCon ns (InfixC t1 n t2) =
+    pfCon ns (NormalC n [t1,t2])
+
+pfField :: [Name] -> Type -> Q Type
+pfField ns t@(ConT n) | n `elem` ns = conT ''I `appT` return t
+pfField ns t                        = conT ''K `appT` return t
+
+ixInstance :: Name -> [Name] -> Int -> Int -> Name -> Q Dec
+ixInstance s ns m i n =
+  instanceD (cxt []) (conT ''Ix `appT` conT s `appT` conT n)
+    [mkFrom ns n m i, mkTo ns n m i, mkIndex n]
+
+mkFrom :: [Name] -> Name -> Int -> Int -> Q Dec
+mkFrom ns n m i =
+    do
+      -- runIO $ putStrLn $ "processing " ++ show n
+      let wrapE e = lrE m i (conE 'Tag `appE` e)
+      i <- reify n
+      let b = case i of
+                TyConI (DataD _ _ _ cs _) ->
+                  zipWith (fromCon wrapE ns (length cs)) [0..] cs
+                TyConI (TySynD t _ _) ->
+                  [clause [varP (field 0)] (normalB (wrapE $ conE 'K `appE` varE (field 0))) []]
+                _ -> error "unknown construct" 
+      funD 'from_ b 
+
+mkTo :: [Name] -> Name -> Int -> Int -> Q Dec
+mkTo ns n m i =
+    do
+      -- runIO $ putStrLn $ "processing " ++ show n
+      let wrapP p = lrP m i (conP 'Tag [p])
+      i <- reify n
+      let b = case i of
+                TyConI (DataD _ _ _ cs _) ->
+                  zipWith (toCon wrapP ns (length cs)) [0..] cs
+                TyConI (TySynD t _ _) ->
+                  [clause [wrapP $ conP 'K [varP (field 0)]] (normalB $ varE (field 0)) []]
+                _ -> error "unknown construct" 
+      funD 'to_ b 
+
+mkIndex :: Name -> Q Dec
+mkIndex n =
+  funD 'index [clause [] (normalB (conE (mkName (nameBase n)))) []]
+
+fromCon :: (Q Exp -> Q Exp) -> [Name] -> Int -> Int -> Con -> Q Clause
+fromCon wrap ns m i (NormalC n []) =
+    clause
+      [conP n []]
+      (normalB $ wrap $ lrE m i $ conE 'C `appE` (conE 'U)) []
+fromCon wrap ns m i (NormalC n fs) =
+    -- runIO (putStrLn ("constructor " ++ show ix)) >>
+    clause
+      [conP n (map (varP . field) [0..length fs - 1])]
+      (normalB $ wrap $ lrE m i $ conE 'C `appE` foldr1 prod (zipWith (fromField ns) [0..] (map snd fs))) []
+  where
+    prod x y = conE '(:*:) `appE` x `appE` y
+fromCon wrap ns m i (InfixC t1 n t2) =
+  fromCon wrap ns m i (NormalC n [t1,t2])
+
+toCon :: (Q Pat -> Q Pat) -> [Name] -> Int -> Int -> Con -> Q Clause
+toCon wrap ns m i (NormalC n []) =
+    clause
+      [wrap $ lrP m i $ conP 'C [conP 'U []]]
+      (normalB $ conE n) []
+toCon wrap ns m i (NormalC n fs) =
+    -- runIO (putStrLn ("constructor " ++ show ix)) >>
+    clause
+      [wrap $ lrP m i $ conP 'C [foldr1 prod (zipWith (toField ns) [0..] (map snd fs))]]
+      (normalB $ foldl appE (conE n) (map (varE . field) [0..length fs - 1])) []
+  where
+    prod x y = conP '(:*:) [x,y]
+toCon wrap ns m i (InfixC t1 n t2) =
+  toCon wrap ns m i (NormalC n [t1,t2])
+
+fromField :: [Name] -> Int -> Type -> Q Exp
+fromField ns nr t@(ConT n) | n `elem` ns = conE 'I `appE` (conE 'I0 `appE` varE (field nr))
+fromField ns nr t                        = conE 'K `appE` varE (field nr)
+
+toField :: [Name] -> Int -> Type -> Q Pat
+toField ns nr t@(ConT n) | n `elem` ns = conP 'I [conP 'I0 [varP (field nr)]]
+toField ns nr t                        = conP 'K [varP (field nr)]
+
+field :: Int -> Name
+field n = mkName $ "f" ++ show n
+
+lrP :: Int -> Int -> (Q Pat -> Q Pat)
+lrP 1 0 p = p
+lrP m 0 p = conP 'L [p]
+lrP m i p = conP 'R [lrP (m-1) (i-1) p]
+
+lrE :: Int -> Int -> (Q Exp -> Q Exp)
+lrE 1 0 e = e
+lrE m 0 e = conE 'L `appE` e
+lrE m i e = conE 'R `appE` lrE (m-1) (i-1) e
+