diff --git a/Examples/MuFeldspar/Core.hs b/Examples/MuFeldspar/Core.hs
--- a/Examples/MuFeldspar/Core.hs
+++ b/Examples/MuFeldspar/Core.hs
@@ -1,9 +1,9 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module MuFeldspar.Core where
 
@@ -11,7 +11,6 @@
 
 import Prelude hiding (max, min)
 import qualified Prelude
-
 import Data.Typeable
 
 import Language.Syntactic.Features.Binding
@@ -19,6 +18,10 @@
 
 
 
+--------------------------------------------------------------------------------
+-- * Types
+--------------------------------------------------------------------------------
+
 -- | Convenient class alias
 class    (Eq a, Show a, Typeable a) => Type a
 instance (Eq a, Show a, Typeable a) => Type a
@@ -90,70 +93,101 @@
     :+: Parallel
     :+: ForLoop
 
-type Data a = HOAST FeldDomain (Full a)
+data Data a = Type a => Data { unData :: HOAST FeldDomain (Full a) }
 
+instance Type a =>
+    Syntactic (Data a) (HOLambda FeldDomain :+: Variable :+: FeldDomain)
+  where
+    type Internal (Data a) = a
+    desugar = unData
+    sugar   = Data
+
 -- | Specialization of the 'Syntactic' class for the Feldspar domain
 class
     ( Syntactic a (HOLambda FeldDomain :+: Variable :+: FeldDomain)
     , Type (Internal a)
+    , SyntacticN a
+        (ASTF (HOLambda FeldDomain :+: Variable :+: FeldDomain) (Internal a))
     ) =>
       Syntax a
 
 instance
     ( Syntactic a (HOLambda FeldDomain :+: Variable :+: FeldDomain)
     , Type (Internal a)
+    , SyntacticN a
+        (ASTF (HOLambda FeldDomain :+: Variable :+: FeldDomain) (Internal a))
     ) =>
       Syntax a
 
 
 
 --------------------------------------------------------------------------------
--- * Core library
+-- * Back ends
 --------------------------------------------------------------------------------
 
-reifyFeld :: Syntax a =>
-    a -> AST (Lambda :+: Variable :+: FeldDomain) (Full (Internal a))
-reifyFeld = reify . desugar
+printFeld :: Reifiable a FeldDomain internal => a -> IO ()
+printFeld = printExpr . reify
 
-eval :: Syntax a => a -> Internal a
-eval = evalLambda . reifyFeld
+drawFeld :: Reifiable a FeldDomain internal => a -> IO ()
+drawFeld = drawAST . reify
 
+eval :: Reifiable a FeldDomain internal => a -> NAryEval internal
+eval = evalLambda . reify
+
+
+
+--------------------------------------------------------------------------------
+-- * Core library
+--------------------------------------------------------------------------------
+
+value :: Syntax a => Internal a -> a
+value = litSyn
+
 -- | 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
+leT :: (Syntax a, Syntax b) => a -> (a -> b) -> b
+leT a f = sugar $ let_ (desugar a) (desugarN f)
 
+instance Eq (Data a)
+  where
+    Data a == Data b = reifyHOAST a `eqLambda` reifyHOAST b
+
+instance Show (Data a)
+  where
+    show (Data a) = render $ reifyHOAST a
+
 instance (Type a, Num a) => Num (Data a)
   where
-    fromInteger = lit . fromInteger
-    abs         = primFunc "abs" abs
-    signum      = primFunc "signum" signum
-    (+)         = primFunc2 "(+)" (+)
-    (-)         = primFunc2 "(-)" (-)
-    (*)         = primFunc2 "(*)" (*)
+    fromInteger = value . fromInteger
+    abs         = sugarN $ primFunc "abs" abs
+    signum      = sugarN $ primFunc "signum" signum
+    (+)         = sugarN $ primFunc2 "(+)" (+)
+    (-)         = sugarN $ primFunc2 "(-)" (-)
+    (*)         = sugarN $ 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
+parallel len ixf
+    =   sugar
+    $   inject Parallel
+    :$: desugar len
+    :$: lambda (desugarN ixf)
 
 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
+forLoop len init body
+    =   sugar
+    $   inject ForLoop
+    :$: desugar len
+    :$: desugar init
+    :$: lambdaN (desugarN body)
 
 arrLength :: Type a => Data [a] -> Data Length
-arrLength = primFunc "arrLength" Prelude.length
+arrLength = sugarN $ primFunc "arrLength" Prelude.length
 
 getIx :: Type a => Data [a] -> Data Index -> Data a
-getIx arr ix = primFunc2 "getIx" eval arr ix
+getIx = sugarN $ primFunc2 "getIx" eval
   where
     eval as i
         | i >= len || i < 0 = error "getIx: index out of bounds"
@@ -162,8 +196,8 @@
         len = Prelude.length as
 
 max :: (Type a, Ord a) => Data a -> Data a -> Data a
-max = primFunc2 "max" Prelude.max
+max = sugarN $ primFunc2 "max" Prelude.max
 
 min :: (Type a, Ord a) => Data a -> Data a -> Data a
-min = primFunc2 "min" Prelude.min
+min = sugarN $ primFunc2 "min" Prelude.min
 
diff --git a/Examples/MuFeldspar/Test.hs b/Examples/MuFeldspar/Test.hs
--- a/Examples/MuFeldspar/Test.hs
+++ b/Examples/MuFeldspar/Test.hs
@@ -1,6 +1,4 @@
-import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip)
-
-import Language.Syntactic.Features.Binding.HigherOrder
+import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)
 
 import MuFeldspar.Core
 import MuFeldspar.Vector
@@ -10,30 +8,37 @@
 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
+test1_1 = drawFeld prog1
+test1_2 = printFeld prog1
+test1_3 = eval prog1 0 10
 
 prog2 :: Data Int -> Data Int
-prog2 a = let_ (min a a) $ \b -> max b b
+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
+test2_1 = drawFeld prog2
+test2_2 = printFeld 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_1 = drawFeld prog3
+test3_2 = printFeld 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])
+prog4 = map (uncurry (*)) $ zip (1...1000) (value [34,43,52,61])
 
-test4_1 = drawAST $ reify $ desugar prog4
-test4_2 = printExpr $ reify $ desugar prog4
-test4_3 = eval $ desugar prog4
+test4_1 = drawFeld prog4
+test4_2 = printFeld prog4
+test4_3 = eval prog4
+
+prog5 :: Vector (Data Index) -> Vector (Data Index)
+prog5 = zipWith (*) (1...1000)
+
+test5_1 = drawFeld prog5
+test5_2 = printFeld prog5
+test5_3 = eval prog5 [20..30]
 
diff --git a/Examples/MuFeldspar/Vector.hs b/Examples/MuFeldspar/Vector.hs
--- a/Examples/MuFeldspar/Vector.hs
+++ b/Examples/MuFeldspar/Vector.hs
@@ -8,7 +8,7 @@
 
 
 
-import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip)
+import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)
 import qualified Prelude
 
 import Language.Syntactic
@@ -17,12 +17,20 @@
 import MuFeldspar.Core
 
 
+
 data Vector a
   where
     Indexed :: Data Length -> (Data Index -> a) -> Vector a
 
+instance Syntax a =>
+    Syntactic (Vector a) (HOLambda FeldDomain :+: Variable :+: FeldDomain)
+  where
+    type Internal (Vector a) = [Internal a]
+    desugar = desugar . freezeVector . map resugar
+    sugar   = map resugar . unfreezeVector . sugar
 
 
+
 length :: Vector a -> Data Length
 length (Indexed len _) = len
 
@@ -38,9 +46,6 @@
 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))
 
@@ -63,16 +68,12 @@
 map :: (a -> b) -> Vector a -> Vector b
 map f (Indexed len ixf) = Indexed len (f . ixf)
 
+zipWith :: (a -> b -> c) -> Vector a -> Vector b -> Vector c
+zipWith f a b = map (uncurry f) $ zip a b
+
 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/Language/Syntactic/Analysis/Equality.hs b/Language/Syntactic/Analysis/Equality.hs
--- a/Language/Syntactic/Analysis/Equality.hs
+++ b/Language/Syntactic/Analysis/Equality.hs
@@ -15,13 +15,13 @@
   where
     exprEq :: expr a -> expr b -> Bool
 
-instance ExprEq expr => ExprEq (AST expr)
+instance ExprEq dom => ExprEq (AST dom)
   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)
+instance ExprEq dom => Eq (AST dom a)
   where
     (==) = exprEq
 
diff --git a/Language/Syntactic/Analysis/Evaluation.hs b/Language/Syntactic/Analysis/Evaluation.hs
--- a/Language/Syntactic/Analysis/Evaluation.hs
+++ b/Language/Syntactic/Analysis/Evaluation.hs
@@ -11,7 +11,7 @@
     -- | Evaluation of expressions
     evaluate :: expr a -> a
 
-instance Eval expr => Eval (AST expr)
+instance Eval dom => Eval (AST dom)
   where
     evaluate (Symbol a) = evaluate a
     evaluate (f :$: a)  = evaluate f $: result (evaluate a)
@@ -21,7 +21,7 @@
     evaluate (InjectL a) = evaluate a
     evaluate (InjectR a) = evaluate a
 
-evalFull :: Eval expr => ASTF expr a -> a
+evalFull :: Eval dom => ASTF dom a -> a
 evalFull = result . evaluate
 
 evalSyn :: (Syntactic a dom, Eval dom) => a -> Internal a
diff --git a/Language/Syntactic/Analysis/Hash.hs b/Language/Syntactic/Analysis/Hash.hs
--- a/Language/Syntactic/Analysis/Hash.hs
+++ b/Language/Syntactic/Analysis/Hash.hs
@@ -15,7 +15,7 @@
     -- according to 'exprEq' must result in the same hash.
     exprHash :: expr a -> Hash
 
-instance ExprHash expr => ExprHash (AST expr)
+instance ExprHash dom => ExprHash (AST dom)
   where
     exprHash (Symbol a) = hashInt 0 `combine` exprHash a
     exprHash (f :$: a)  = hashInt 1 `combine` exprHash f `combine` exprHash a
diff --git a/Language/Syntactic/Analysis/Render.hs b/Language/Syntactic/Analysis/Render.hs
--- a/Language/Syntactic/Analysis/Render.hs
+++ b/Language/Syntactic/Analysis/Render.hs
@@ -28,12 +28,12 @@
     renderPart []   a = render a
     renderPart args a = "(" ++ unwords (render a : args) ++ ")"
 
-instance Render expr => Render (AST expr)
+instance Render dom => Render (AST dom)
   where
     renderPart args (Symbol a) = renderPart args a
     renderPart args (f :$: a)  = renderPart (render a : args) f
 
-instance Render expr => Show (AST expr a)
+instance Render dom => Show (AST dom a)
   where
     show = render
 
diff --git a/Language/Syntactic/Features/Binding.hs b/Language/Syntactic/Features/Binding.hs
--- a/Language/Syntactic/Features/Binding.hs
+++ b/Language/Syntactic/Features/Binding.hs
@@ -60,38 +60,45 @@
 
 -- | Alpha-equivalence on 'Lambda' expressions. Free variables are taken to be
 -- equvalent if they have the same identifier.
-eqLambda :: ExprEq dom
+eqLambdaM :: 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
+eqLambdaM (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
+eqLambdaM
     ((project -> Just (Lambda v1)) :$: a1)
     ((project -> Just (Lambda v2)) :$: a2)
-      = local ((v1,v2):) $ eqLambda a1 a2
+      = local ((v1,v2):) $ eqLambdaM a1 a2
 
-eqLambda (f1 :$: a1) (f2 :$: a2) = do
-    e <- eqLambda f1 f2
-    if e then eqLambda a1 a2 else return False
+eqLambdaM (f1 :$: a1) (f2 :$: a2) = do
+    e <- eqLambdaM f1 f2
+    if e then eqLambdaM a1 a2 else return False
 
-eqLambda
+eqLambdaM
     (Symbol (InjectR (InjectR a)))
     (Symbol (InjectR (InjectR b)))
       = return (exprEq a b)
 
-eqLambda _ _ = return False
+eqLambdaM _ _ = return False
 
 
 
+eqLambda :: ExprEq dom
+    => AST (Lambda :+: Variable :+: dom) a
+    -> AST (Lambda :+: Variable :+: dom) b
+    -> Bool
+eqLambda a b = runReader (eqLambdaM a b) []
+
+
 -- | Evaluation of possibly open 'LambdaAST' expressions
 evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
-    AST (Lambda :+: Variable :+: dom) (Full a) -> m a
+    ASTF (Lambda :+: Variable :+: dom) a -> m a
 evalLambdaM = liftM result . eval
   where
     eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
@@ -122,41 +129,36 @@
 
 
 -- | Evaluation of closed 'Lambda' expressions
-evalLambda :: Eval dom => AST (Lambda :+: Variable :+: dom) (Full a) -> a
+evalLambda :: Eval dom => ASTF (Lambda :+: Variable :+: dom) a -> a
 evalLambda = flip runReader [] . evalLambdaM
 
 
 
 -- | The class of n-ary binding functions
-class NAry a
+class NAry 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 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))
+         => (ASTF dom b -> ASTF dom c)
+         -> ASTF dom (b -> c)
          )
-      -> a -> AST (NAryDom a) (Full (NAryEval a))
+      -> a -> ASTF dom (NAryEval a)
 
-instance NAry (AST dom (Full a))
+instance NAry (ASTF dom a) dom
   where
-    type NAryEval (AST dom (Full a)) = a
-    type NAryDom  (AST dom (Full a)) = dom
+    type NAryEval (ASTF dom a) = a
     bindN _ = id
 
-instance
-    ( Typeable a
-    , NAry b
-    , Typeable (NAryEval b)
-    , NAryDom b ~ dom
-    ) =>
-      NAry (AST dom (Full a) -> b)
+instance (Typeable a, NAry b dom, Typeable (NAryEval b)) =>
+    NAry (ASTF dom a -> b) dom
   where
-    type NAryEval (AST dom (Full a) -> b) = a -> NAryEval b
-    type NAryDom  (AST dom (Full a) -> b) = dom
+    type NAryEval (ASTF dom a -> b) = a -> NAryEval b
     bindN lambda = lambda . (bindN lambda .)
 
 
diff --git a/Language/Syntactic/Features/Binding/HigherOrder.hs b/Language/Syntactic/Features/Binding/HigherOrder.hs
--- a/Language/Syntactic/Features/Binding/HigherOrder.hs
+++ b/Language/Syntactic/Features/Binding/HigherOrder.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE UndecidableInstances #-}
+
 -- | 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
@@ -14,6 +16,8 @@
     , lambdaN
     , let_
     , reifyM
+    , reifyHOAST
+    , Reifiable
     , reify
     ) where
 
@@ -44,11 +48,8 @@
 lambda = inject . HOLambda
 
 -- | N-ary lambda binding
-lambdaN ::
-    ( NAry a
-    , NAryDom a ~ (HOLambda dom :+: Variable :+: dom)
-    ) =>
-      a -> HOAST dom (Full (NAryEval a))
+lambdaN :: NAry a (HOLambda dom :+: Variable :+: dom) =>
+    a -> HOAST dom (Full (NAryEval a))
 lambdaN = bindN lambda
 
 -- | Let binding
@@ -71,8 +72,30 @@
 
 -- | 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
+reifyHOAST :: Typeable a => HOAST dom a -> AST (Lambda :+: Variable :+: dom) a
+reifyHOAST = 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.
+
+
+
+-- | Convenient class alias for n-ary syntactic functions
+class
+    ( SyntacticN a internal
+    , NAry internal (HOLambda dom :+: Variable :+: dom)
+    , Typeable (NAryEval internal)
+    ) =>
+      Reifiable a dom internal | a -> dom internal
+
+instance
+    ( SyntacticN a internal
+    , NAry internal (HOLambda dom :+: Variable :+: dom)
+    , Typeable (NAryEval internal)
+    ) =>
+      Reifiable a dom internal
+
+-- | Reifying an n-ary syntactic function
+reify :: Reifiable a dom internal =>
+    a -> ASTF (Lambda :+: Variable :+: dom) (NAryEval internal)
+reify = reifyHOAST . lambdaN . desugarN
 
diff --git a/Language/Syntactic/Features/Condition.hs b/Language/Syntactic/Features/Condition.hs
--- a/Language/Syntactic/Features/Condition.hs
+++ b/Language/Syntactic/Features/Condition.hs
@@ -39,8 +39,8 @@
 
 
 
-condition :: (Condition :<: expr, Syntactic a expr) =>
-    ASTF expr Bool -> a -> a -> a
+condition :: (Condition :<: dom, Syntactic a dom) =>
+    ASTF dom Bool -> a -> a -> a
 condition cond tHEN eLSE = sugar $ inject Condition
     :$: cond
     :$: desugar tHEN
diff --git a/Language/Syntactic/Features/Literal.hs b/Language/Syntactic/Features/Literal.hs
--- a/Language/Syntactic/Features/Literal.hs
+++ b/Language/Syntactic/Features/Literal.hs
@@ -42,6 +42,15 @@
 
 
 
-lit :: (Eq a, Show a, Typeable a, Literal :<: expr) => a -> ASTF expr a
+lit :: (Eq a, Show a, Typeable a, Literal :<: dom) => a -> ASTF dom a
 lit = inject . Literal
+
+litSyn
+    :: ( Eq (Internal a)
+       , Show (Internal a)
+       , Syntactic a dom
+       , Literal :<: dom
+       )
+    => Internal a -> a
+litSyn = sugar . inject . Literal
 
diff --git a/Language/Syntactic/Features/PrimFunc.hs b/Language/Syntactic/Features/PrimFunc.hs
--- a/Language/Syntactic/Features/PrimFunc.hs
+++ b/Language/Syntactic/Features/PrimFunc.hs
@@ -52,37 +52,37 @@
 
 
 
-primFunc :: (Typeable a, PrimFunc :<: expr)
+primFunc :: (Typeable a, PrimFunc :<: dom)
     => String
     -> (a -> b)
-    -> ASTF expr a
-    -> ASTF expr b
+    -> ASTF dom a
+    -> ASTF dom b
 primFunc name f a = inject (PrimFunc name f) :$: a
 
-primFunc2 :: (Typeable a, Typeable b, PrimFunc :<: expr)
+primFunc2 :: (Typeable a, Typeable b, PrimFunc :<: dom)
     => String
     -> (a -> b -> c)
-    -> ASTF expr a
-    -> ASTF expr b
-    -> ASTF expr c
+    -> ASTF dom a
+    -> ASTF dom b
+    -> ASTF dom c
 primFunc2 name f a b = inject (PrimFunc name f) :$: a :$: b
 
-primFunc3 :: (Typeable a, Typeable b, Typeable c, PrimFunc :<: expr)
+primFunc3 :: (Typeable a, Typeable b, Typeable c, PrimFunc :<: dom)
     => String
     -> (a -> b -> c -> d)
-    -> ASTF expr a
-    -> ASTF expr b
-    -> ASTF expr c
-    -> ASTF expr d
+    -> ASTF dom a
+    -> ASTF dom b
+    -> ASTF dom c
+    -> ASTF dom 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)
+primFunc4 :: (Typeable a, Typeable b, Typeable c, Typeable d, PrimFunc :<: dom)
     => String
     -> (a -> b -> c -> d -> e)
-    -> ASTF expr a
-    -> ASTF expr b
-    -> ASTF expr c
-    -> ASTF expr d
-    -> ASTF expr e
+    -> ASTF dom a
+    -> ASTF dom b
+    -> ASTF dom c
+    -> ASTF dom d
+    -> ASTF dom 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
--- a/Language/Syntactic/Features/Tuple.hs
+++ b/Language/Syntactic/Features/Tuple.hs
@@ -135,12 +135,12 @@
 
 
 instance
-    ( Syntactic a expr
-    , Syntactic b expr
-    , Tuple  :<: expr
-    , Select :<: expr
+    ( Syntactic a dom
+    , Syntactic b dom
+    , Tuple  :<: dom
+    , Select :<: dom
     ) =>
-      Syntactic (a,b) expr
+      Syntactic (a,b) dom
   where
     type Internal (a,b) =
         ( Internal a
@@ -157,13 +157,13 @@
         )
 
 instance
-    ( Syntactic a expr
-    , Syntactic b expr
-    , Syntactic c expr
-    , Tuple  :<: expr
-    , Select :<: expr
+    ( Syntactic a dom
+    , Syntactic b dom
+    , Syntactic c dom
+    , Tuple  :<: dom
+    , Select :<: dom
     ) =>
-      Syntactic (a,b,c) expr
+      Syntactic (a,b,c) dom
   where
     type Internal (a,b,c) =
         ( Internal a
@@ -183,14 +183,14 @@
         )
 
 instance
-    ( Syntactic a expr
-    , Syntactic b expr
-    , Syntactic c expr
-    , Syntactic d expr
-    , Tuple  :<: expr
-    , Select :<: expr
+    ( Syntactic a dom
+    , Syntactic b dom
+    , Syntactic c dom
+    , Syntactic d dom
+    , Tuple  :<: dom
+    , Select :<: dom
     ) =>
-      Syntactic (a,b,c,d) expr
+      Syntactic (a,b,c,d) dom
   where
     type Internal (a,b,c,d) =
         ( Internal a
@@ -213,15 +213,15 @@
         )
 
 instance
-    ( Syntactic a expr
-    , Syntactic b expr
-    , Syntactic c expr
-    , Syntactic d expr
-    , Syntactic e expr
-    , Tuple  :<: expr
-    , Select :<: expr
+    ( Syntactic a dom
+    , Syntactic b dom
+    , Syntactic c dom
+    , Syntactic d dom
+    , Syntactic e dom
+    , Tuple  :<: dom
+    , Select :<: dom
     ) =>
-      Syntactic (a,b,c,d,e) expr
+      Syntactic (a,b,c,d,e) dom
   where
     type Internal (a,b,c,d,e) =
         ( Internal a
@@ -247,16 +247,16 @@
         )
 
 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 dom
+    , Syntactic b dom
+    , Syntactic c dom
+    , Syntactic d dom
+    , Syntactic e dom
+    , Syntactic f dom
+    , Tuple  :<: dom
+    , Select :<: dom
     ) =>
-      Syntactic (a,b,c,d,e,f) expr
+      Syntactic (a,b,c,d,e,f) dom
   where
     type Internal (a,b,c,d,e,f) =
         ( Internal a
@@ -285,17 +285,17 @@
         )
 
 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 dom
+    , Syntactic b dom
+    , Syntactic c dom
+    , Syntactic d dom
+    , Syntactic e dom
+    , Syntactic f dom
+    , Syntactic g dom
+    , Tuple  :<: dom
+    , Select :<: dom
     ) =>
-      Syntactic (a,b,c,d,e,f,g) expr
+      Syntactic (a,b,c,d,e,f,g) dom
   where
     type Internal (a,b,c,d,e,f,g) =
         ( Internal a
diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs
--- a/Language/Syntactic/Syntax.hs
+++ b/Language/Syntactic/Syntax.hs
@@ -72,6 +72,7 @@
       -- * Syntactic sugar
     , Syntactic (..)
     , resugar
+    , SyntacticN (..)
       -- * AST processing
     , SubTrees (..)
     , processNode
@@ -241,6 +242,43 @@
 -- | Syntactic type casting
 resugar :: (Syntactic a dom, Syntactic b dom, Internal a ~ Internal b) => a -> b
 resugar = sugar . desugar
+
+-- | N-ary syntactic functions
+--
+-- 'desugarN' has any type of the form:
+--
+-- > desugarN ::
+-- >     ( Syntactic a dom
+-- >     , Syntactic b dom
+-- >     , ...
+-- >     , Syntactic x dom
+-- >     ) => (a -> b -> ... -> x)
+-- >       -> (  AST dom (Full (Internal a))
+-- >          -> AST dom (Full (Internal b))
+-- >          -> ...
+-- >          -> AST dom (Full (Internal x))
+-- >          )
+--
+-- ...and vice versa for 'sugarN'.
+class SyntacticN a internal | a -> internal
+  where
+    desugarN :: a -> internal
+    sugarN   :: internal -> a
+
+instance (Syntactic a dom, ia ~ AST dom (Full (Internal a))) => SyntacticN a ia
+  where
+    desugarN = desugar
+    sugarN   = sugar
+
+instance
+    ( Syntactic a dom
+    , ia ~ Internal a
+    , SyntacticN b ib
+    ) =>
+      SyntacticN (a -> b) (AST dom (Full ia) -> ib)
+  where
+    desugarN f = desugarN . f . sugar
+    sugarN f   = sugarN . f . desugar
 
 
 
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        0.1
+Version:        0.2
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .