diff --git a/Examples/ALaCarte.hs b/Examples/ALaCarte.hs
new file mode 100644
--- /dev/null
+++ b/Examples/ALaCarte.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- | Demonstration of the fact that "Language.Syntactic" has the same
+-- functionality as /Data types a la carte/ (Wouter Swierstra, in
+-- /Journal of Functional Programming/, 2008)
+
+module ALaCarte where
+
+
+
+import Language.Syntactic
+
+
+
+data Val a
+  where
+    Val :: Int -> Val (Full Int)
+
+data Add a
+  where
+    Add :: Add (Int :-> Int :-> Full Int)
+
+data Mul a
+  where
+    Mul :: Mul (Int :-> Int :-> Full Int)
+
+instance Eval Val
+  where
+    evaluate (Val a) = Full a
+
+instance Eval Add
+  where
+    evaluate Add = Partial $ \a -> Partial $ \b -> Full (a+b)
+
+instance Eval Mul
+  where
+    evaluate Mul = Partial $ \a -> Partial $ \b -> Full (a*b)
+
+instance Render Val
+  where
+    render (Val a) = show a
+
+instance Render Add
+  where
+    render Add = "(+)"
+
+instance Render Mul
+  where
+    render Mul = "(*)"
+
+
+
+-- Manual injection:
+
+addExample :: ASTF (Val :+: Add) Int
+addExample = Symbol (InjectR Add) :$: Symbol (InjectL (Val 118)) :$: Symbol (InjectL (Val 1219))
+
+
+
+-- Automatic injection:
+
+val :: (Val :<: expr) => Int -> ASTF expr Int
+val = inject . Val
+
+(<+>) :: (Add :<: expr) => ASTF expr Int -> ASTF expr Int -> ASTF expr Int
+a <+> b = inject Add :$: a :$: b
+
+(<*>) :: (Mul :<: expr) => ASTF expr Int -> ASTF expr Int -> ASTF expr Int
+a <*> b = inject Mul :$: a :$: b
+
+infixl 6 <+>
+infixl 7 <*>
+
+example1 :: ASTF (Add :+: Val) Int
+example1 = val 30000 <+> val 1330 <+> val 7
+
+test1 = evaluate example1
+
+example2 :: ASTF (Val :+: Add :+: Mul) Int
+example2 = val 80 <*> val 5 <+> val 4
+
+test2 = evaluate example2
+
+example3 :: ASTF (Val :+: Mul) Int
+example3 = val 6 <*> val 7
+
+test3 = evaluate example3
+
+example4 :: ASTF (Val :+: Add :+: Mul) Int
+example4 = val 80 <*> val 5 <+> val 4
+
+test4 = render example4
+
+
+
+-- Pattern matching:
+
+distr :: (Add :<: expr, Mul :<: expr, ConsType a) => AST expr a -> AST expr a
+distr ((project -> Just Mul) :$: a :$: b) = case distr b of
+    (project -> Just Add) :$: c :$: d -> a' <*> c <+> a' <*> d
+    b' -> a' <*> b'
+  where
+    a' = distr a
+distr (f :$: a) = distr f :$: distr a
+distr a         = a
+  -- Note the use of direct recursion instead of a fold combinator
+
+example5 :: ASTF (Val :+: Add :+: Mul) Int
+example5 = val 80 <*> (val 5 <+> val 4) <+> val 543
+
+test5 = render (distr example5)
+
+example6 :: ASTF (Mul :+: Add :+: Val) Int
+example6 = val 444 <*> (val 80 <*> (val 5 <+> val 3 <*> val 4))
+
+test6 = render (distr example6)
+
diff --git a/Examples/MuFeldspar/Core.hs b/Examples/MuFeldspar/Core.hs
new file mode 100644
--- /dev/null
+++ b/Examples/MuFeldspar/Core.hs
@@ -0,0 +1,169 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module MuFeldspar.Core where
+
+
+
+import Prelude hiding (max, min)
+import qualified Prelude
+
+import Data.Typeable
+
+import Language.Syntactic.Features.Binding
+import Language.Syntactic.Features.Binding.HigherOrder
+
+
+
+-- | Convenient class alias
+class    (Eq a, Show a, Typeable a) => Type a
+instance (Eq a, Show a, Typeable a) => Type a
+
+type Length = Int
+type Index  = Int
+
+
+
+--------------------------------------------------------------------------------
+-- * Parallel arrays
+--------------------------------------------------------------------------------
+
+data Parallel a
+  where
+    Parallel :: Parallel (Length :-> (Index -> a) :-> Full [a])
+
+instance Render Parallel
+  where
+    render Parallel = "parallel"
+
+instance ToTree Parallel
+
+instance ExprEq Parallel
+  where
+    Parallel `exprEq` Parallel = True
+
+instance Eval Parallel
+  where
+    evaluate Parallel = consEval $ \len ixf -> Prelude.map ixf [0 .. len-1]
+
+
+
+--------------------------------------------------------------------------------
+-- * For loops
+--------------------------------------------------------------------------------
+
+data ForLoop a
+  where
+    ForLoop :: ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)
+
+instance ExprEq ForLoop
+  where
+    ForLoop `exprEq` ForLoop = True
+
+instance Render ForLoop
+  where
+    render ForLoop = "forLoop"
+
+instance ToTree ForLoop
+
+instance Eval ForLoop
+  where
+    evaluate ForLoop = consEval $ \len init body -> foldr body init [0 .. len-1]
+
+
+
+--------------------------------------------------------------------------------
+-- * Feldspar domain
+--------------------------------------------------------------------------------
+
+type FeldDomain
+    =   Literal
+    :+: PrimFunc
+    :+: Condition
+    :+: Tuple
+    :+: Select
+    :+: Let
+    :+: Parallel
+    :+: ForLoop
+
+type Data a = HOAST FeldDomain (Full a)
+
+-- | Specialization of the 'Syntactic' class for the Feldspar domain
+class
+    ( Syntactic a (HOLambda FeldDomain :+: Variable :+: FeldDomain)
+    , Type (Internal a)
+    ) =>
+      Syntax a
+
+instance
+    ( Syntactic a (HOLambda FeldDomain :+: Variable :+: FeldDomain)
+    , Type (Internal a)
+    ) =>
+      Syntax a
+
+
+
+--------------------------------------------------------------------------------
+-- * Core library
+--------------------------------------------------------------------------------
+
+reifyFeld :: Syntax a =>
+    a -> AST (Lambda :+: Variable :+: FeldDomain) (Full (Internal a))
+reifyFeld = reify . desugar
+
+eval :: Syntax a => a -> Internal a
+eval = evalLambda . reifyFeld
+
+-- | For types containing some kind of \"thunk\", this function can be used to
+-- force computation
+force :: Syntax a => a -> a
+force = resugar
+
+-- TODO Hacks to make the 'Num' instance work:
+instance ExprEq (HOLambda a) where exprEq = undefined
+instance Render (HOLambda a) where render = undefined
+instance ExprEq Variable     where exprEq = undefined
+
+instance (Type a, Num a) => Num (Data a)
+  where
+    fromInteger = lit . fromInteger
+    abs         = primFunc "abs" abs
+    signum      = primFunc "signum" signum
+    (+)         = primFunc2 "(+)" (+)
+    (-)         = primFunc2 "(-)" (-)
+    (*)         = primFunc2 "(*)" (*)
+
+parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]
+parallel len ixf = inject Parallel :$: len :$: lambda ixf
+
+forLoopCore :: Type st =>
+     Data Length -> Data st -> (Data Index -> Data st -> Data st) -> Data st
+forLoopCore len init body = inject ForLoop :$: len :$: init :$: lambdaN body
+
+forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st
+forLoop len init body = sugar $ forLoopCore len (desugar init) body'
+  where
+    body' i = desugar . body i . sugar
+
+arrLength :: Type a => Data [a] -> Data Length
+arrLength = primFunc "arrLength" Prelude.length
+
+getIx :: Type a => Data [a] -> Data Index -> Data a
+getIx arr ix = primFunc2 "getIx" eval arr ix
+  where
+    eval as i
+        | i >= len || i < 0 = error "getIx: index out of bounds"
+        | otherwise         = as !! i
+      where
+        len = Prelude.length as
+
+max :: (Type a, Ord a) => Data a -> Data a -> Data a
+max = primFunc2 "max" Prelude.max
+
+min :: (Type a, Ord a) => Data a -> Data a -> Data a
+min = primFunc2 "min" Prelude.min
+
diff --git a/Examples/MuFeldspar/Test.hs b/Examples/MuFeldspar/Test.hs
new file mode 100644
--- /dev/null
+++ b/Examples/MuFeldspar/Test.hs
@@ -0,0 +1,39 @@
+import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip)
+
+import Language.Syntactic.Features.Binding.HigherOrder
+
+import MuFeldspar.Core
+import MuFeldspar.Vector
+
+
+
+prog1 :: Data Int -> Data Int -> Data Int
+prog1 a b = min (max a (getIx (parallel b (\i -> min i b)) 3)) 2
+
+test1_1 = drawAST $ reify $ lambdaN prog1
+test1_2 = printExpr $ reify $ lambdaN prog1
+test1_3 = eval $ prog1 0 10
+
+prog2 :: Data Int -> Data Int
+prog2 a = let_ (min a a) $ \b -> max b b
+
+test2_1 = drawAST $ reify $ lambdaN prog2
+test2_2 = printExpr $ reify $ lambdaN prog2
+test2_3 = eval $ prog2 34
+
+prog3 :: Data Index
+prog3 = sum $ reverse (10...45)
+
+test3_1 = drawAST $ reify prog3
+test3_2 = printExpr $ reify prog3
+test3_3 = eval prog3
+test3_4 = eval (forLoop ((45 - 10) + 1) 0 (\var0 -> (\var1 -> ((((((45 - 10) + 1) - var0) - 1) + 10) + var1))))
+  -- Pasted in the result of 'test3_2'
+
+prog4 :: Vector (Data Index)
+prog4 = map (uncurry (*)) $ zip (1...1000) (vector [34,43,52,61])
+
+test4_1 = drawAST $ reify $ desugar prog4
+test4_2 = printExpr $ reify $ desugar prog4
+test4_3 = eval $ desugar prog4
+
diff --git a/Examples/MuFeldspar/Vector.hs b/Examples/MuFeldspar/Vector.hs
new file mode 100644
--- /dev/null
+++ b/Examples/MuFeldspar/Vector.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module MuFeldspar.Vector where
+
+
+
+import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip)
+import qualified Prelude
+
+import Language.Syntactic
+import Language.Syntactic.Features.Binding.HigherOrder
+
+import MuFeldspar.Core
+
+
+data Vector a
+  where
+    Indexed :: Data Length -> (Data Index -> a) -> Vector a
+
+
+
+length :: Vector a -> Data Length
+length (Indexed len _) = len
+
+indexed :: Data Length -> (Data Index -> a) -> Vector a
+indexed = Indexed
+
+index :: Vector a -> Data Index -> a
+index (Indexed _ ixf) = ixf
+
+freezeVector :: Type a => Vector (Data a) -> Data [a]
+freezeVector vec = parallel (length vec) (index vec)
+
+unfreezeVector :: Type a => Data [a] -> Vector (Data a)
+unfreezeVector arr = Indexed (arrLength arr) (getIx arr)
+
+vector :: Type a => [a] -> Vector (Data a)
+vector = unfreezeVector . lit
+
+zip :: Vector a -> Vector b -> Vector (a,b)
+zip a b = indexed (length a `min` length b) (\i -> (index a i, index b i))
+
+unzip :: Vector (a,b) -> (Vector a, Vector b)
+unzip ab = (indexed len (fst . index ab), indexed len (snd . index ab))
+  where
+    len = length ab
+
+permute :: (Data Length -> Data Index -> Data Index) -> (Vector a -> Vector a)
+permute perm vec = indexed len (index vec . perm len)
+  where
+    len = length vec
+
+reverse :: Vector a -> Vector a
+reverse = permute $ \len i -> len-i-1
+
+(...) :: Data Index -> Data Index -> Vector (Data Index)
+l ... h = indexed (h-l+1) (+l)
+
+map :: (a -> b) -> Vector a -> Vector b
+map f (Indexed len ixf) = Indexed len (f . ixf)
+
+fold :: Syntax b => (a -> b -> b) -> b -> Vector a -> b
+fold f b (Indexed len ixf) = forLoop len b (\i st -> f (ixf i) st)
+
+sum :: (Type a, Num a) => Vector (Data a) -> Data a
+sum = fold (+) 0
+
+instance Syntax a =>
+    Syntactic (Vector a) (HOLambda FeldDomain :+: Variable :+: FeldDomain)
+  where
+    type Internal (Vector a) = [Internal a]
+    desugar = freezeVector . map desugar
+    sugar   = map sugar . unfreezeVector
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c)2011, Emil Axelsson
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Emil Axelsson nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"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 COPYRIGHT
+OWNER 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/Language/Syntactic.hs b/Language/Syntactic.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic.hs
@@ -0,0 +1,31 @@
+-- | The syntactic library
+--
+-- The basic functionality is provided by the module
+-- "Language.Syntactic.Syntax".
+
+module Language.Syntactic
+    ( module Language.Syntactic.Syntax
+    , module Language.Syntactic.Analysis.Equality
+    , module Language.Syntactic.Analysis.Render
+    , module Language.Syntactic.Analysis.Evaluation
+    , module Language.Syntactic.Analysis.Hash
+    , module Language.Syntactic.Features.Literal
+    , module Language.Syntactic.Features.PrimFunc
+    , module Language.Syntactic.Features.Condition
+    , module Language.Syntactic.Features.Tuple
+    , module Language.Syntactic.Features.Annotate
+    ) where
+
+
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+import Language.Syntactic.Analysis.Render
+import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Analysis.Hash
+import Language.Syntactic.Features.Literal
+import Language.Syntactic.Features.PrimFunc
+import Language.Syntactic.Features.Condition
+import Language.Syntactic.Features.Tuple
+import Language.Syntactic.Features.Annotate
+
diff --git a/Language/Syntactic/Analysis/Equality.hs b/Language/Syntactic/Analysis/Equality.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Analysis/Equality.hs
@@ -0,0 +1,42 @@
+module Language.Syntactic.Analysis.Equality where
+
+
+
+import Language.Syntactic.Syntax
+
+
+
+-- | Equality for expressions. The difference between 'Eq' and 'ExprEq' is that
+-- 'ExprEq' allows comparison of expressions with different value types. It is
+-- assumed that when the types differ, the expressions also differ. The reason
+-- for allowing comparison of different types is that this is convenient when
+-- the types are existentially quantified.
+class ExprEq expr
+  where
+    exprEq :: expr a -> expr b -> Bool
+
+instance ExprEq expr => ExprEq (AST expr)
+  where
+    exprEq (Symbol a)  (Symbol b)  = exprEq a b
+    exprEq (f1 :$: a1) (f2 :$: a2) = exprEq f1 f2 && exprEq a1 a2
+    exprEq _ _ = False
+
+instance ExprEq expr => Eq (AST expr a)
+  where
+    (==) = exprEq
+
+instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2)
+  where
+    exprEq (InjectL a) (InjectL b) = exprEq a b
+    exprEq (InjectR a) (InjectR b) = exprEq a b
+    exprEq _ _ = False
+
+instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a)
+  where
+    (==) = exprEq
+
+
+
+eqSyn :: (Syntactic a dom, ExprEq dom) => a -> a -> Bool
+eqSyn a b = desugar a `exprEq` desugar b
+
diff --git a/Language/Syntactic/Analysis/Evaluation.hs b/Language/Syntactic/Analysis/Evaluation.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Analysis/Evaluation.hs
@@ -0,0 +1,29 @@
+module Language.Syntactic.Analysis.Evaluation where
+
+
+
+import Language.Syntactic.Syntax
+
+
+
+class Eval expr
+  where
+    -- | Evaluation of expressions
+    evaluate :: expr a -> a
+
+instance Eval expr => Eval (AST expr)
+  where
+    evaluate (Symbol a) = evaluate a
+    evaluate (f :$: a)  = evaluate f $: result (evaluate a)
+
+instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)
+  where
+    evaluate (InjectL a) = evaluate a
+    evaluate (InjectR a) = evaluate a
+
+evalFull :: Eval expr => ASTF expr a -> a
+evalFull = result . evaluate
+
+evalSyn :: (Syntactic a dom, Eval dom) => a -> Internal a
+evalSyn = evalFull . desugar
+
diff --git a/Language/Syntactic/Analysis/Hash.hs b/Language/Syntactic/Analysis/Hash.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Analysis/Hash.hs
@@ -0,0 +1,27 @@
+module Language.Syntactic.Analysis.Hash where
+
+
+
+import Data.Hash
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+
+
+
+class ExprEq expr => ExprHash expr
+  where
+    -- | Computes a 'Hash' for an expression. Expressions that are equal
+    -- according to 'exprEq' must result in the same hash.
+    exprHash :: expr a -> Hash
+
+instance ExprHash expr => ExprHash (AST expr)
+  where
+    exprHash (Symbol a) = hashInt 0 `combine` exprHash a
+    exprHash (f :$: a)  = hashInt 1 `combine` exprHash f `combine` exprHash a
+
+instance (ExprHash expr1, ExprHash expr2) => ExprHash (expr1 :+: expr2)
+  where
+    exprHash (InjectL a) = hashInt 0 `combine` exprHash a
+    exprHash (InjectR a) = hashInt 1 `combine` exprHash a
+
diff --git a/Language/Syntactic/Analysis/Render.hs b/Language/Syntactic/Analysis/Render.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Analysis/Render.hs
@@ -0,0 +1,83 @@
+module Language.Syntactic.Analysis.Render
+    ( Render (..)
+    , printExpr
+    , ToTree (..)
+    , showAST
+    , drawAST
+    ) where
+
+
+
+import Data.Tree
+
+import Language.Syntactic.Syntax
+
+
+
+-- | Render an expression as concrete syntax. A complete instance must define
+-- either of the methods 'render' and 'renderPart'.
+class Render expr
+  where
+    -- | Render an expression as a 'String'
+    render :: expr a -> String
+    render = renderPart []
+
+    -- | Render a partially applied constructor given a list of rendered missing
+    -- arguments
+    renderPart :: [String] -> expr a -> String
+    renderPart []   a = render a
+    renderPart args a = "(" ++ unwords (render a : args) ++ ")"
+
+instance Render expr => Render (AST expr)
+  where
+    renderPart args (Symbol a) = renderPart args a
+    renderPart args (f :$: a)  = renderPart (render a : args) f
+
+instance Render expr => Show (AST expr a)
+  where
+    show = render
+
+instance (Render expr1, Render expr2) => Render (expr1 :+: expr2)
+  where
+    renderPart args (InjectL a) = renderPart args a
+    renderPart args (InjectR a) = renderPart args a
+
+instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a)
+  where
+    show = render
+
+-- | Print an expression
+printExpr :: Render expr => expr a -> IO ()
+printExpr = putStrLn . render
+
+
+
+class Render expr => ToTree expr
+  where
+    -- | Convert a partially applied constructor to a syntax tree given a list
+    -- of rendered missing arguments
+    toTreePart :: [Tree String] -> expr a -> Tree String
+    toTreePart args a = Node (render a) args
+
+instance ToTree dom => ToTree (AST dom)
+  where
+    toTreePart args (Symbol a) = toTreePart args a
+    toTreePart args (f :$: a)  = toTreePart (toTree a : args) f
+
+instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2)
+  where
+    toTreePart args (InjectL a) = toTreePart args a
+    toTreePart args (InjectR a) = toTreePart args a
+
+-- | Convert an expression to a syntax tree
+toTree :: ToTree expr => expr a -> Tree String
+toTree = toTreePart []
+
+-- | Show syntax tree using ASCII art
+showAST :: ToTree dom => AST dom a -> String
+showAST = drawTree . toTree
+
+-- | Print syntax tree using ASCII art
+drawAST :: ToTree dom => AST dom a -> IO ()
+drawAST = putStrLn . showAST
+
diff --git a/Language/Syntactic/Features/Annotate.hs b/Language/Syntactic/Features/Annotate.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Annotate.hs
@@ -0,0 +1,70 @@
+-- | Annotations for syntax trees
+
+module Language.Syntactic.Features.Annotate where
+
+
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+import Language.Syntactic.Analysis.Render
+import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Analysis.Hash
+
+
+
+-- | Annotating an expression with arbitrary information.
+--
+-- This can be used to annotate every node of a syntax tree, which is done by
+-- changing
+--
+-- > AST dom a
+--
+-- to
+--
+-- > AST (Ann info dom) a
+--
+-- Injection/projection of an annotated tree is done using
+-- 'injectAnn' / 'projectAnn'.
+data Ann info expr a
+  where
+    Ann :: info (EvalResult a) -> expr a -> Ann info expr a
+
+
+
+instance ExprEq expr => ExprEq (Ann info expr)
+  where
+    Ann _ a `exprEq` Ann _ b = exprEq a b
+
+instance Render expr => Render (Ann info expr)
+  where
+    render (Ann _ a) = render a
+
+instance ToTree expr => ToTree (Ann info expr)
+  where
+    toTreePart args (Ann _ a) = toTreePart args a
+
+instance Eval expr => Eval (Ann info expr)
+  where
+    evaluate (Ann _ a) = evaluate a
+
+instance ExprHash expr => ExprHash (Ann info expr)
+  where
+    exprHash (Ann _ a) = exprHash a
+
+
+
+injectAnn :: (sub :<: sup, ConsType a) =>
+    info (EvalResult a) -> sub a -> AST (Ann info sup) a
+injectAnn info = Symbol . Ann info . inject
+
+projectAnn :: (sub :<: sup) =>
+    AST (Ann info sup) a -> Maybe (info (EvalResult a), sub a)
+projectAnn a = do
+    Symbol (Ann info b) <- return a
+    c                   <- project b
+    return (info, c)
+
+getInfo :: AST (Ann info sup) a -> info (EvalResult a)
+getInfo (Symbol (Ann info _)) = info
+getInfo (f :$: _)             = getInfo f
+
diff --git a/Language/Syntactic/Features/Binding.hs b/Language/Syntactic/Features/Binding.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Binding.hs
@@ -0,0 +1,191 @@
+-- | General binding constructs
+
+module Language.Syntactic.Features.Binding where
+
+
+
+import Control.Monad.Reader
+import Data.Dynamic
+import Data.Ix
+import Data.Tree
+
+import Data.Hash
+
+import Language.Syntactic
+
+
+
+-- | Variable identifier
+newtype VarId = VarId { varInteger :: Integer }
+  deriving (Eq, Ord, Num, Enum, Ix)
+
+instance Show VarId
+  where
+    show (VarId i) = show i
+
+showVar :: VarId -> String
+showVar v = "var" ++ show v
+
+
+
+-- | Variables
+data Variable a
+  where
+    Variable :: Typeable a => VarId -> Variable (Full a)
+
+instance Render Variable
+  where
+    render (Variable v) = showVar v
+
+instance ToTree Variable
+  where
+    toTreePart [] (Variable v) = Node ("var:" ++ show v) []
+
+
+
+-- | Lambda binding
+data Lambda a
+  where
+    Lambda :: (Typeable a, Typeable b) => VarId -> Lambda (b :-> Full (a -> b))
+
+instance Render Lambda
+  where
+    renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> "  ++ body ++ ")"
+
+instance ToTree Lambda
+  where
+    toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body]
+
+
+
+-- | Alpha-equivalence on 'Lambda' expressions. Free variables are taken to be
+-- equvalent if they have the same identifier.
+eqLambda :: ExprEq dom
+    => AST (Lambda :+: Variable :+: dom) a
+    -> AST (Lambda :+: Variable :+: dom) b
+    -> Reader [(VarId,VarId)] Bool
+
+eqLambda (project -> Just (Variable v1)) (project -> Just (Variable v2)) = do
+    env <- ask
+    case lookup v1 env of
+      Nothing  -> return (v1==v2)   -- Free variables
+      Just v2' -> return (v2==v2')
+
+eqLambda
+    ((project -> Just (Lambda v1)) :$: a1)
+    ((project -> Just (Lambda v2)) :$: a2)
+      = local ((v1,v2):) $ eqLambda a1 a2
+
+eqLambda (f1 :$: a1) (f2 :$: a2) = do
+    e <- eqLambda f1 f2
+    if e then eqLambda a1 a2 else return False
+
+eqLambda
+    (Symbol (InjectR (InjectR a)))
+    (Symbol (InjectR (InjectR b)))
+      = return (exprEq a b)
+
+eqLambda _ _ = return False
+
+
+
+-- | Evaluation of possibly open 'LambdaAST' expressions
+evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
+    AST (Lambda :+: Variable :+: dom) (Full a) -> m a
+evalLambdaM = liftM result . eval
+  where
+    eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
+        AST (Lambda :+: Variable :+: dom) a -> m a
+    eval (project -> Just (Variable v)) = do
+        env <- ask
+        case lookup v env of
+          Nothing -> return $ error "eval: evaluating free variable"
+          Just a  -> case fromDynamic a of
+            Just a -> return (Full a)
+            _      -> return $ error "eval: internal type error"
+
+    eval ((project -> Just (Lambda v)) :$: body) = do
+        env <- ask
+        return
+            $ Full
+            $ \a -> flip runReader ((v,toDyn a):env)
+            $ liftM result
+            $ eval body
+
+    eval (f :$: a) = do
+        f' <- eval f
+        a' <- eval a
+        return (f' $: result a')
+
+    eval (Symbol (InjectR (InjectR a))) = return (evaluate a)
+
+
+
+-- | Evaluation of closed 'Lambda' expressions
+evalLambda :: Eval dom => AST (Lambda :+: Variable :+: dom) (Full a) -> a
+evalLambda = flip runReader [] . evalLambdaM
+
+
+
+-- | The class of n-ary binding functions
+class NAry a
+  where
+    type NAryEval a
+    type NAryDom  a :: * -> *
+
+    -- | N-ary binding by nested use of the supplied binder
+    bindN
+      :: (  forall b c . (Typeable b, Typeable c)
+         => (AST (NAryDom a) (Full b) -> AST (NAryDom a) (Full c))
+         -> AST (NAryDom a) (Full (b -> c))
+         )
+      -> a -> AST (NAryDom a) (Full (NAryEval a))
+
+instance NAry (AST dom (Full a))
+  where
+    type NAryEval (AST dom (Full a)) = a
+    type NAryDom  (AST dom (Full a)) = dom
+    bindN _ = id
+
+instance
+    ( Typeable a
+    , NAry b
+    , Typeable (NAryEval b)
+    , NAryDom b ~ dom
+    ) =>
+      NAry (AST dom (Full a) -> b)
+  where
+    type NAryEval (AST dom (Full a) -> b) = a -> NAryEval b
+    type NAryDom  (AST dom (Full a) -> b) = dom
+    bindN lambda = lambda . (bindN lambda .)
+
+
+
+-- | Let binding
+data Let a
+  where
+    Let :: Let (a :-> (a -> b) :-> Full b)
+
+instance ExprEq Let
+  where
+    exprEq Let Let = True
+
+instance Render Let
+  where
+    render Let = "Let"
+
+instance ToTree Let
+  where
+    toTreePart [a,body] Let = Node ("Let " ++ var) [a,body']
+      where
+        Node node [body'] = body
+        var               = drop 7 node  -- Drop the "Lambda " prefix
+
+instance Eval Let
+  where
+    evaluate Let = consEval (flip ($))
+
+instance ExprHash Let
+  where
+    exprHash Let = hashInt 0
+
diff --git a/Language/Syntactic/Features/Binding/HigherOrder.hs b/Language/Syntactic/Features/Binding/HigherOrder.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Binding/HigherOrder.hs
@@ -0,0 +1,78 @@
+-- | This module provides binding constructs using higher-order syntax and a
+-- function for translating back to first-order syntax. Expressions constructed
+-- using the exported interface are guaranteed to have a well-behaved
+-- translation.
+
+module Language.Syntactic.Features.Binding.HigherOrder
+    ( module Language.Syntactic
+    , Variable
+    , evalLambda
+    , Let (..)
+    , HOLambda (..)
+    , HOAST
+    , lambda
+    , lambdaN
+    , let_
+    , reifyM
+    , reify
+    ) where
+
+
+
+import Control.Monad.State
+import Data.Typeable
+
+import Language.Syntactic
+import Language.Syntactic.Features.Binding
+
+
+
+-- | Higher-order lambda binding
+data HOLambda dom a
+  where
+    HOLambda :: (Typeable a, Typeable b)
+        => (HOAST dom (Full a) -> HOAST dom (Full b))
+        -> HOLambda dom (Full (a -> b))
+
+type HOAST dom = AST (HOLambda dom :+: Variable :+: dom)
+
+
+
+-- | Lambda binding
+lambda :: (Typeable a, Typeable b) =>
+    (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b))
+lambda = inject . HOLambda
+
+-- | N-ary lambda binding
+lambdaN ::
+    ( NAry a
+    , NAryDom a ~ (HOLambda dom :+: Variable :+: dom)
+    ) =>
+      a -> HOAST dom (Full (NAryEval a))
+lambdaN = bindN lambda
+
+-- | Let binding
+let_ :: (Typeable a, Typeable b, Let :<: dom)
+    => HOAST dom (Full a)
+    -> (HOAST dom (Full a) -> HOAST dom (Full b))
+    -> HOAST dom (Full b)
+let_ a f = inject Let :$: a :$: lambda f
+
+
+
+reifyM :: Typeable a
+    => HOAST dom a
+    -> State VarId (AST (Lambda :+: Variable :+: dom) a)
+reifyM (f :$: a)            = liftM2 (:$:) (reifyM f) (reifyM a)
+reifyM (Symbol (InjectR a)) = return $ Symbol $ InjectR a
+reifyM (Symbol (InjectL (HOLambda f))) = do
+    v <- get; put (v+1)
+    liftM (inject (Lambda v) :$:) $ reifyM $ f $ inject $ Variable v
+
+-- | Translating expressions with higher-order binding to corresponding
+-- expressions using first-order binding
+reify :: Typeable a => HOAST dom a -> AST (Lambda :+: Variable :+: dom) a
+reify = flip evalState 0 . reifyM
+  -- It is assumed that there are no 'Variable' constructors (i.e. no free
+  -- variables) in the argument. This is guaranteed by the exported interface.
+
diff --git a/Language/Syntactic/Features/Condition.hs b/Language/Syntactic/Features/Condition.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Condition.hs
@@ -0,0 +1,48 @@
+-- | Conditional expressions
+
+module Language.Syntactic.Features.Condition where
+
+
+
+import Data.Hash
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+import Language.Syntactic.Analysis.Render
+import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Analysis.Hash
+
+
+
+data Condition a
+  where
+    Condition :: Condition (Bool :-> a :-> a :-> Full a)
+
+instance ExprEq Condition
+  where
+    exprEq Condition Condition = True
+
+instance Render Condition
+  where
+    render Condition = "condition"
+
+instance ToTree Condition
+
+instance Eval Condition
+  where
+    evaluate Condition = consEval $
+        \cond tHEN eLSE -> if cond then tHEN else eLSE
+
+instance ExprHash Condition
+  where
+    exprHash Condition = hashInt 0
+
+
+
+condition :: (Condition :<: expr, Syntactic a expr) =>
+    ASTF expr Bool -> a -> a -> a
+condition cond tHEN eLSE = sugar $ inject Condition
+    :$: cond
+    :$: desugar tHEN
+    :$: desugar eLSE
+
diff --git a/Language/Syntactic/Features/Literal.hs b/Language/Syntactic/Features/Literal.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Literal.hs
@@ -0,0 +1,47 @@
+-- | Literal expressions
+
+module Language.Syntactic.Features.Literal where
+
+
+
+import Data.Typeable
+
+import Data.Hash
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+import Language.Syntactic.Analysis.Render
+import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Analysis.Hash
+
+
+
+data Literal a
+  where
+    Literal :: (Eq a, Show a, Typeable a) => a -> Literal (Full a)
+
+instance ExprEq Literal
+  where
+    Literal a `exprEq` Literal b = case cast a of
+        Just a' -> a'==b
+        Nothing -> False
+
+instance Render Literal
+  where
+    render (Literal a) = show a
+
+instance ToTree Literal
+
+instance Eval Literal
+  where
+    evaluate (Literal a) = consEval a
+
+instance ExprHash Literal
+  where
+    exprHash (Literal a) = hash (show a)
+
+
+
+lit :: (Eq a, Show a, Typeable a, Literal :<: expr) => a -> ASTF expr a
+lit = inject . Literal
+
diff --git a/Language/Syntactic/Features/PrimFunc.hs b/Language/Syntactic/Features/PrimFunc.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/PrimFunc.hs
@@ -0,0 +1,88 @@
+-- | Primitive functions
+
+module Language.Syntactic.Features.PrimFunc where
+
+
+
+import Data.Typeable
+
+import Data.Hash
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+import Language.Syntactic.Analysis.Render
+import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Analysis.Hash
+
+
+
+data PrimFunc a
+  where
+    PrimFunc :: ConsType b =>
+        String -> (ConsEval (a :-> b)) -> PrimFunc (a :-> b)
+
+instance ExprEq PrimFunc
+  where
+    PrimFunc f1 _ `exprEq` PrimFunc f2 _ = f1==f2
+
+instance Render PrimFunc
+  where
+    renderPart [] (PrimFunc name _) = name
+    renderPart args (PrimFunc name _)
+        | isInfix   = "(" ++ unwords [a,op,b] ++ ")"
+        | otherwise = "(" ++ unwords (name : args) ++ ")"
+      where
+        [a,b] = args
+        op    = init $ tail name
+        isInfix
+          =  not (null name)
+          && head name == '('
+          && last name == ')'
+          && length args == 2
+
+instance ToTree PrimFunc
+
+instance Eval PrimFunc
+  where
+    evaluate (PrimFunc _ f) = consEval f
+
+instance ExprHash PrimFunc
+  where
+    exprHash (PrimFunc name _) = hash name
+
+
+
+primFunc :: (Typeable a, PrimFunc :<: expr)
+    => String
+    -> (a -> b)
+    -> ASTF expr a
+    -> ASTF expr b
+primFunc name f a = inject (PrimFunc name f) :$: a
+
+primFunc2 :: (Typeable a, Typeable b, PrimFunc :<: expr)
+    => String
+    -> (a -> b -> c)
+    -> ASTF expr a
+    -> ASTF expr b
+    -> ASTF expr c
+primFunc2 name f a b = inject (PrimFunc name f) :$: a :$: b
+
+primFunc3 :: (Typeable a, Typeable b, Typeable c, PrimFunc :<: expr)
+    => String
+    -> (a -> b -> c -> d)
+    -> ASTF expr a
+    -> ASTF expr b
+    -> ASTF expr c
+    -> ASTF expr d
+primFunc3 name f a b c = inject (PrimFunc name f) :$: a :$: b :$: c
+
+primFunc4 :: (Typeable a, Typeable b, Typeable c, Typeable d, PrimFunc :<: expr)
+    => String
+    -> (a -> b -> c -> d -> e)
+    -> ASTF expr a
+    -> ASTF expr b
+    -> ASTF expr c
+    -> ASTF expr d
+    -> ASTF expr e
+primFunc4 name f a b c d = inject (PrimFunc name f) :$: a :$: b :$: c :$: d
+
diff --git a/Language/Syntactic/Features/Tuple.hs b/Language/Syntactic/Features/Tuple.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Features/Tuple.hs
@@ -0,0 +1,328 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Construction and selection of tuples
+
+module Language.Syntactic.Features.Tuple where
+
+
+
+import Data.Hash
+import Data.Tuple.Select
+
+import Language.Syntactic.Syntax
+import Language.Syntactic.Analysis.Equality
+import Language.Syntactic.Analysis.Render
+import Language.Syntactic.Analysis.Evaluation
+import Language.Syntactic.Analysis.Hash
+
+
+
+-- | Expressions for constructing tuples
+data Tuple a
+  where
+    Tup2 :: Tuple (a :-> b :-> Full (a,b))
+    Tup3 :: Tuple (a :-> b :-> c :-> Full (a,b,c))
+    Tup4 :: Tuple (a :-> b :-> c :-> d :-> Full (a,b,c,d))
+    Tup5 :: Tuple (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))
+    Tup6 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))
+    Tup7 :: Tuple (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))
+
+instance ExprEq Tuple
+  where
+    Tup2 `exprEq` Tup2 = True
+    Tup3 `exprEq` Tup3 = True
+    Tup4 `exprEq` Tup4 = True
+    Tup5 `exprEq` Tup5 = True
+    Tup6 `exprEq` Tup6 = True
+    Tup7 `exprEq` Tup7 = True
+    exprEq _ _ = False
+
+instance Render Tuple
+  where
+    render Tup2 = "tup2"
+    render Tup3 = "tup3"
+    render Tup4 = "tup4"
+    render Tup5 = "tup5"
+    render Tup6 = "tup6"
+    render Tup7 = "tup7"
+
+instance ToTree Tuple
+
+instance Eval Tuple
+  where
+    evaluate Tup2 = consEval (,)
+    evaluate Tup3 = consEval (,,)
+    evaluate Tup4 = consEval (,,,)
+    evaluate Tup5 = consEval (,,,,)
+    evaluate Tup6 = consEval (,,,,,)
+    evaluate Tup7 = consEval (,,,,,,)
+
+instance ExprHash Tuple
+  where
+    exprHash Tup2 = hashInt 0
+    exprHash Tup3 = hashInt 1
+    exprHash Tup4 = hashInt 2
+    exprHash Tup5 = hashInt 3
+    exprHash Tup6 = hashInt 4
+    exprHash Tup7 = hashInt 5
+
+-- | Expressions for selecting elements of a tuple
+data Select a
+  where
+    Sel1 :: Sel1 a b => Select (a :-> Full b)
+    Sel2 :: Sel2 a b => Select (a :-> Full b)
+    Sel3 :: Sel3 a b => Select (a :-> Full b)
+    Sel4 :: Sel4 a b => Select (a :-> Full b)
+    Sel5 :: Sel5 a b => Select (a :-> Full b)
+    Sel6 :: Sel6 a b => Select (a :-> Full b)
+    Sel7 :: Sel7 a b => Select (a :-> Full b)
+
+instance ExprEq Select
+  where
+    Sel1 `exprEq` Sel1 = True
+    Sel2 `exprEq` Sel2 = True
+    Sel3 `exprEq` Sel3 = True
+    Sel4 `exprEq` Sel4 = True
+    Sel5 `exprEq` Sel5 = True
+    Sel6 `exprEq` Sel6 = True
+    Sel7 `exprEq` Sel7 = True
+    exprEq _ _ = False
+
+instance Eval Select
+  where
+    evaluate Sel1 = consEval sel1
+    evaluate Sel2 = consEval sel2
+    evaluate Sel3 = consEval sel3
+    evaluate Sel4 = consEval sel4
+    evaluate Sel5 = consEval sel5
+    evaluate Sel6 = consEval sel6
+    evaluate Sel7 = consEval sel7
+
+instance Render Select
+  where
+    render Sel1 = "sel1"
+    render Sel2 = "sel2"
+    render Sel3 = "sel3"
+    render Sel4 = "sel4"
+    render Sel5 = "sel5"
+    render Sel6 = "sel6"
+    render Sel7 = "sel7"
+
+instance ToTree Select
+
+instance ExprHash Select
+  where
+    exprHash Sel1 = hashInt 0
+    exprHash Sel2 = hashInt 1
+    exprHash Sel3 = hashInt 2
+    exprHash Sel4 = hashInt 3
+    exprHash Sel5 = hashInt 4
+    exprHash Sel6 = hashInt 5
+    exprHash Sel7 = hashInt 6
+
+-- | Return the selected position, e.g.
+--
+-- > selectPos (Sel3 :: Select ((Int,Int,Int,Int) -> Int)) = 3
+selectPos :: Select a -> Int
+selectPos Sel1 = 1
+selectPos Sel2 = 2
+selectPos Sel3 = 3
+selectPos Sel4 = 4
+selectPos Sel5 = 5
+selectPos Sel6 = 6
+selectPos Sel7 = 7
+
+
+
+instance
+    ( Syntactic a expr
+    , Syntactic b expr
+    , Tuple  :<: expr
+    , Select :<: expr
+    ) =>
+      Syntactic (a,b) expr
+  where
+    type Internal (a,b) =
+        ( Internal a
+        , Internal b
+        )
+
+    desugar (a,b) = inject Tup2
+        :$: desugar a
+        :$: desugar b
+
+    sugar a =
+        ( sugar $ inject Sel1 :$: a
+        , sugar $ inject Sel2 :$: a
+        )
+
+instance
+    ( Syntactic a expr
+    , Syntactic b expr
+    , Syntactic c expr
+    , Tuple  :<: expr
+    , Select :<: expr
+    ) =>
+      Syntactic (a,b,c) expr
+  where
+    type Internal (a,b,c) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        )
+
+    desugar (a,b,c) = inject Tup3
+        :$: desugar a
+        :$: desugar b
+        :$: desugar c
+
+    sugar a =
+        ( sugar $ inject Sel1 :$: a
+        , sugar $ inject Sel2 :$: a
+        , sugar $ inject Sel3 :$: a
+        )
+
+instance
+    ( Syntactic a expr
+    , Syntactic b expr
+    , Syntactic c expr
+    , Syntactic d expr
+    , Tuple  :<: expr
+    , Select :<: expr
+    ) =>
+      Syntactic (a,b,c,d) expr
+  where
+    type Internal (a,b,c,d) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        )
+
+    desugar (a,b,c,d) = inject Tup4
+        :$: desugar a
+        :$: desugar b
+        :$: desugar c
+        :$: desugar d
+
+    sugar a =
+        ( sugar $ inject Sel1 :$: a
+        , sugar $ inject Sel2 :$: a
+        , sugar $ inject Sel3 :$: a
+        , sugar $ inject Sel4 :$: a
+        )
+
+instance
+    ( Syntactic a expr
+    , Syntactic b expr
+    , Syntactic c expr
+    , Syntactic d expr
+    , Syntactic e expr
+    , Tuple  :<: expr
+    , Select :<: expr
+    ) =>
+      Syntactic (a,b,c,d,e) expr
+  where
+    type Internal (a,b,c,d,e) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        , Internal e
+        )
+
+    desugar (a,b,c,d,e) = inject Tup5
+        :$: desugar a
+        :$: desugar b
+        :$: desugar c
+        :$: desugar d
+        :$: desugar e
+
+    sugar a =
+        ( sugar $ inject Sel1 :$: a
+        , sugar $ inject Sel2 :$: a
+        , sugar $ inject Sel3 :$: a
+        , sugar $ inject Sel4 :$: a
+        , sugar $ inject Sel5 :$: a
+        )
+
+instance
+    ( Syntactic a expr
+    , Syntactic b expr
+    , Syntactic c expr
+    , Syntactic d expr
+    , Syntactic e expr
+    , Syntactic f expr
+    , Tuple  :<: expr
+    , Select :<: expr
+    ) =>
+      Syntactic (a,b,c,d,e,f) expr
+  where
+    type Internal (a,b,c,d,e,f) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        , Internal e
+        , Internal f
+        )
+
+    desugar (a,b,c,d,e,f) = inject Tup6
+        :$: desugar a
+        :$: desugar b
+        :$: desugar c
+        :$: desugar d
+        :$: desugar e
+        :$: desugar f
+
+    sugar a =
+        ( sugar $ inject Sel1 :$: a
+        , sugar $ inject Sel2 :$: a
+        , sugar $ inject Sel3 :$: a
+        , sugar $ inject Sel4 :$: a
+        , sugar $ inject Sel5 :$: a
+        , sugar $ inject Sel6 :$: a
+        )
+
+instance
+    ( Syntactic a expr
+    , Syntactic b expr
+    , Syntactic c expr
+    , Syntactic d expr
+    , Syntactic e expr
+    , Syntactic f expr
+    , Syntactic g expr
+    , Tuple  :<: expr
+    , Select :<: expr
+    ) =>
+      Syntactic (a,b,c,d,e,f,g) expr
+  where
+    type Internal (a,b,c,d,e,f,g) =
+        ( Internal a
+        , Internal b
+        , Internal c
+        , Internal d
+        , Internal e
+        , Internal f
+        , Internal g
+        )
+
+    desugar (a,b,c,d,e,f,g) = inject Tup7
+        :$: desugar a
+        :$: desugar b
+        :$: desugar c
+        :$: desugar d
+        :$: desugar e
+        :$: desugar f
+        :$: desugar g
+
+    sugar a =
+        ( sugar $ inject Sel1 :$: a
+        , sugar $ inject Sel2 :$: a
+        , sugar $ inject Sel3 :$: a
+        , sugar $ inject Sel4 :$: a
+        , sugar $ inject Sel5 :$: a
+        , sugar $ inject Sel6 :$: a
+        , sugar $ inject Sel7 :$: a
+        )
+
diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/Language/Syntactic/Syntax.hs
@@ -0,0 +1,306 @@
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Generic representation of typed syntax trees
+--
+-- As a simple demonstration, take the following simple language:
+--
+-- > data Expr1 a
+-- >   where
+-- >     Num1 :: Int -> Expr1 Int
+-- >     Add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
+--
+-- Using the present library, this can be rewritten as follows:
+--
+-- > data Num2 a where Num2 :: Int -> Num2 (Full Int)
+-- > data Add2 a where Add2 :: Add2 (Int :-> Int :-> Full Int)
+-- >
+-- > type Expr2 a = ASTF (Num2 :+: Add2) a
+--
+-- Note that @Num2@ and @Add2@ are /non-recursive/. The only recursive data type
+-- here is 'AST', which is provided by the library. Now, the important point is
+-- that @Expr1@ and @Expr2@ are completely isomorphic! This is indicated by the
+-- following conversions:
+--
+-- > conv12 :: Expr1 a -> Expr2 a
+-- > conv12 (Num1 n)   = inject (Num2 n)
+-- > conv12 (Add1 a b) = inject Add2 :$: conv12 a :$: conv12 b
+-- >
+-- > conv21 :: Expr2 a -> Expr1 a
+-- > conv21 (project -> Just (Num2 n))           = Num1 n
+-- > conv21 ((project -> Just Add2) :$: a :$: b) = Add1 (conv21 a) (conv21 b)
+--
+-- A key property here is that the patterns in @conv21@ are actually complete.
+--
+-- So, why should one use @Expr2@ instead of @Expr1@? The answer is that @Expr2@
+-- can be processed by generic algorithms defined over 'AST', for example:
+--
+-- > countNodes :: ASTF domain a -> Int
+-- > countNodes = count
+-- >   where
+-- >     count :: AST domain a -> Int
+-- >     count (Symbol _) = 1
+-- >     count (a :$: b)  = count a + count b
+--
+-- Furthermore, although @Expr2@ was defined to use exactly the constructors
+-- 'Num2' and 'Add2', it is possible to leave the set of constructors open,
+-- leading to more modular and reusable code. This can be seen by relaxing the
+-- types of @conv12@ and @conv21@:
+--
+-- > conv12 :: (Num2 :<: dom, Add2 :<: dom) => Expr1 a -> ASTF dom a
+-- > conv21 :: (Num2 :<: dom, Add2 :<: dom) => ASTF dom a -> Expr1 a
+--
+-- This way of encoding open data types is taken from /Data types a la carte/,
+-- by Wouter Swierstra, in /Journal of Functional Programming/, 2008. However,
+-- we do not need Swierstra's fixed-point machinery for recursive data types.
+-- Instead we rely on 'AST' being recursive.
+
+module Language.Syntactic.Syntax
+    ( -- * Syntax trees
+      Full (..)
+    , (:->) (..)
+    , ConsType
+    , ConsEval
+    , EvalResult
+    , consEval
+    , ($:)
+    , AST (..)
+    , ASTF
+    , (:+:) (..)
+      -- * Subsumption
+    , (:<:) (..)
+      -- * Syntactic sugar
+    , Syntactic (..)
+    , resugar
+      -- * AST processing
+    , SubTrees (..)
+    , processNode
+    ) where
+
+
+
+import Data.Typeable
+
+
+
+-- | The type of a fully applied constructor
+newtype Full a = Full { result :: a }
+  deriving (Eq, Show, Typeable)
+
+-- | The type of a partially applied (or unapplied) constructor
+newtype a :-> b = Partial (a -> b)
+  deriving (Typeable)
+
+infixr :->
+
+-- | Fully or partially applied constructor
+--
+-- This class is private to the module to guarantee that all members of the
+-- class have the form:
+--
+-- > Full a
+-- > a1 :-> Full a2
+-- > a1 :-> a2 :-> ... :-> Full an
+--
+-- The closed class also has the property:
+-- @ConsType' (a :-> b)@   iff.   @ConsType' b@.
+class ConsType' a
+  where
+    type ConsEval' a
+    type EvalResult' a
+    consEval' :: ConsEval' a -> a
+
+instance ConsType' (Full a)
+  where
+    type ConsEval'   (Full a) = a
+    type EvalResult' (Full a) = a
+    consEval' = Full
+
+instance ConsType' b => ConsType' (a :-> b)
+  where
+    type ConsEval'   (a :-> b) = a -> ConsEval' b
+    type EvalResult' (a :-> b) = EvalResult' b
+    consEval' = Partial . (consEval' .)
+
+-- | Fully or partially applied constructor
+--
+-- This is a public alias for the hidden class 'ConsType''. The only instances
+-- are:
+--
+-- > instance ConsType' (Full a)
+-- > instance ConsType' b => ConsType' (a :-> b)
+class    ConsType' a => ConsType a
+instance ConsType' a => ConsType a
+
+-- | Maps a 'ConsType' to a simpler form where ':->' has been replaced by @->@,
+-- and 'Full' has been removed. This is a public alias for the hidden type
+-- 'ConsEval''.
+type ConsEval a = ConsEval' a
+
+-- | Returns the result type ('Full' removed) of a 'ConsType'. This is a public
+-- alias for the hidden type 'EvalResult''.
+type EvalResult a = EvalResult' a
+
+-- | Make a constructor evaluation from a 'ConsEval' representation
+consEval :: ConsType a => ConsEval a -> a
+consEval = consEval'
+
+-- | Semantic constructor application
+($:) :: (a :-> b) -> a -> b
+Partial f $: a = f a
+
+
+
+-- | Generic abstract syntax tree, parameterized by a symbol domain
+--
+-- In general, @(`AST` dom (a `:->` b))@ represents a partially applied (or
+-- unapplied) constructor, missing at least one argument, while
+-- @(`AST` dom (`Full` a))@ represents a fully applied constructor, i.e. a
+-- complete syntax tree.
+-- It is not possible to construct a total value of type @(`AST` dom a)@ that
+-- does not fulfill the constraint @(`ConsType` a)@.
+--
+-- Note that the hidden class 'ConsType'' mentioned in the type of 'Symbol' is
+-- interchangeable with 'ConsType'.
+data AST dom a
+  where
+    Symbol :: ConsType' a => dom a -> AST dom a
+    (:$:)  :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b
+
+-- | Fully applied abstract syntax tree
+type ASTF dom a = AST dom (Full a)
+
+-- | Co-product of two symbol domains
+data dom1 :+: dom2 :: * -> *
+  where
+    InjectL :: dom1 a -> (dom1 :+: dom2) a
+    InjectR :: dom2 a -> (dom1 :+: dom2) a
+
+infixl 1 :$:
+infixr :+:
+
+
+
+class sub :<: sup
+  where
+    -- | Injection from @sub@ to @sup@
+    inject :: ConsType a => sub a -> sup a
+
+    -- | Partial projection from @sup@ to @sub@
+    project :: sup a -> Maybe (sub a)
+
+instance (sub :<: sup) => ((:<:) sub (AST sup))
+                            -- GHC 6.12 requires prefix syntax here
+  where
+    inject = Symbol . inject
+
+    project (Symbol a) = project a
+    project _          = Nothing
+
+instance ((:<:) expr expr)
+  where
+    inject  = id
+    project = Just
+
+instance ((:<:) expr1 (expr1 :+: expr2))
+  where
+    inject = InjectL
+
+    project (InjectL a) = Just a
+    project _           = Nothing
+
+instance (expr1 :<: expr3) => ((:<:) expr1 (expr2 :+: expr3))
+  where
+    inject = InjectR . inject
+
+    project (InjectR a) = project a
+    project _           = Nothing
+
+
+
+-- | It is assumed that for all types @A@ fulfilling @(`Syntactic` A dom)@:
+--
+-- > eval a == eval (desugar $ (id :: A -> A) $ sugar a)
+--
+-- (using 'Language.Syntactic.Analysis.Evaluation.eval')
+class Typeable (Internal a) => Syntactic a dom | a -> dom
+    -- Note: using a two-parameter class rather than an associated type, because
+    -- this makes it possible to make a class alias constraining dom. GHC
+    -- doesn't yet handle equality super classes.
+  where
+    type Internal a
+    desugar :: a -> ASTF dom (Internal a)
+    sugar   :: ASTF dom (Internal a) -> a
+
+instance Typeable a => Syntactic (ASTF dom a) dom
+  where
+    type Internal (ASTF dom a) = a
+    desugar = id
+    sugar   = id
+
+-- | Syntactic type casting
+resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b
+resugar = sugar . desugar
+
+
+
+-- | Data family for collecting the children of a constructor, for example:
+--
+-- > subTrees :: forall dom . SubTrees dom (Int :-> Bool :-> Full [Int])
+-- > subTrees = a :*: b :*: Nil
+-- >   where
+-- >     a = undefined :: ASTF dom Int
+-- >     b = undefined :: ASTF dom Bool
+--
+-- @(`SubTrees` a)@ is meaningful iff. @(`ConsType` a)@
+data family SubTrees (dom :: * -> *) a
+
+data instance SubTrees dom (Full a)  = Nil
+data instance SubTrees dom (a :-> b) = ASTF dom a :*: SubTrees dom b
+
+infixr :*:
+
+-- | Process an 'AST' using a function that gets direct access to the top-most
+-- constructor and its sub-trees
+--
+-- This function can be used to create 'AST' traversal functions indexed by the
+-- symbol types, for example:
+--
+-- > class Count subDomain
+-- >   where
+-- >     count' :: Count domain => subDomain a -> SubTrees domain a -> Int
+-- >
+-- > instance (Count sub1, Count sub2) => Count (sub1 :+: sub2)
+-- >   where
+-- >     count' (InjectL a) args = count' a args
+-- >     count' (InjectR a) args = count' a args
+-- >
+-- > count :: Count dom => ASTF dom a -> Int
+-- > count = processNode count'
+--
+-- Here, @count@ represents some static analysis on an 'AST'. Each constructor
+-- in the tree will be processed by @count'@ indexed by the corresponding symbol
+-- type. That way, @count'@ can be seen as an open-ended function on an open
+-- data type. The @(Count domain)@ constraint on @count'@ is to allow recursion
+-- over sub-trees.
+--
+-- Let's say we have a symbol
+--
+-- > data Add a
+-- >   where
+-- >     Add :: Add (Int :-> Int :-> Full Int)
+--
+-- Then the @Count@ instance for @Add@ might look as follows:
+--
+-- > instance Count Add
+-- >   where
+-- >     count' Add (a :*: b :*: Nil) = 1 + count a + count b
+processNode :: forall dom a b
+    .  (forall a . ConsType a => dom a -> SubTrees dom a -> b)
+    -> ASTF dom a -> b
+processNode f a = process a Nil
+  where
+    process :: AST dom c -> SubTrees dom c -> b
+    process (Symbol a) args = f a args
+    process (c :$: a)  args = process c (a :*: args)
+
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/syntactic.cabal b/syntactic.cabal
new file mode 100644
--- /dev/null
+++ b/syntactic.cabal
@@ -0,0 +1,91 @@
+Name:           syntactic
+Version:        0.1
+Synopsis:       Generic abstract syntax, and utilities for embedded languages
+Description:    This library provides:
+                .
+                  * Generic representation and manipulation of abstract syntax
+                    using a practical encoding of open data types (based on Data
+                    Types à la Carte [1])
+                .
+                  * Utilities for analyzing and transforming generic syntax
+                .
+                  * General variable binding constructs
+                .
+                  * Utilities for building extensible embedded languages based
+                    on generic syntax
+                .
+                  * A small proof-of-concept implementation of the embedded
+                    language Feldspar [2] (see the @Examples@ directory)
+                .
+                Note: The library is probably mostly useful for data-flow
+                languages, such as Feldspar. Currently, it does not support
+                cyclic programs.
+                .
+                \[1\] /Data types a la carte/, by Wouter Swierstra, in
+                /Journal of Functional Programming/, 2008
+                .
+                \[2\] <http://hackage.haskell.org/package/feldspar-language>
+License:        BSD3
+License-file:   LICENSE
+Author:         Emil Axelsson
+Maintainer:     emax@chalmers.se
+Copyright:      Copyright (c) 2011, Emil Axelsson
+Homepage:       http://projects.haskell.org/syntactic/
+Category:       Language
+Build-type:     Simple
+Cabal-version:  >=1.6
+
+Extra-source-files:
+  Examples/ALaCarte.hs
+  Examples/MuFeldspar/Core.hs
+  Examples/MuFeldspar/Vector.hs
+  Examples/MuFeldspar/Test.hs
+
+source-repository head
+  type:     darcs
+  location: http://code.haskell.org/syntactic/
+
+Library
+  Exposed-modules:
+    Language.Syntactic
+    Language.Syntactic.Syntax
+    Language.Syntactic.Analysis.Equality
+    Language.Syntactic.Analysis.Render
+    Language.Syntactic.Analysis.Evaluation
+    Language.Syntactic.Analysis.Hash
+    Language.Syntactic.Features.Literal
+    Language.Syntactic.Features.PrimFunc
+    Language.Syntactic.Features.Condition
+    Language.Syntactic.Features.Tuple
+    Language.Syntactic.Features.Annotate
+    Language.Syntactic.Features.Binding
+    Language.Syntactic.Features.Binding.HigherOrder
+
+  Other-modules:
+
+  Build-depends:
+    array,
+    base >= 4 && < 4.4,
+    containers,
+    data-hash,
+    mtl >= 1.1 && < 3,
+    tuple >= 0.2
+
+  Extensions:
+    DeriveDataTypeable
+    FlexibleContexts
+    FlexibleInstances
+    FunctionalDependencies
+    GADTs
+    GeneralizedNewtypeDeriving
+    MultiParamTypeClasses
+    Rank2Types
+    ScopedTypeVariables
+    TypeFamilies
+    TypeOperators
+    TypeSynonymInstances
+    ViewPatterns
+
+    -- Required by GHC-6.12:
+    EmptyDataDecls
+    PatternGuards