diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,10 @@
+# 0.1
+
+* Add `acompare` functiona and `acompare'` method to `Alpha` typeclass.  (christiaanb)
+
+    Handwritten `Alpha` instances will need to define this additional
+    method now.  Major version bump.
+
 # 0.0.3
 
 * Add 'name2Integer' method (christiaanb)
diff --git a/src/Unbound/Generics/LocallyNameless/Alpha.hs b/src/Unbound/Generics/LocallyNameless/Alpha.hs
--- a/src/Unbound/Generics/LocallyNameless/Alpha.hs
+++ b/src/Unbound/Generics/LocallyNameless/Alpha.hs
@@ -39,6 +39,7 @@
   , gswaps
   , gfreshen
   , glfreshen
+  , gacompare
   ) where
 
 import Control.Applicative (Applicative(..), (<$>))
@@ -50,7 +51,7 @@
 import Data.List (intersect)
 import Data.Monoid (Monoid(..), (<>))
 import Data.Ratio (Ratio)
-import Data.Typeable (Typeable, gcast)
+import Data.Typeable (Typeable, gcast, typeOf)
 import GHC.Generics
 
 import Unbound.Generics.LocallyNameless.Name
@@ -201,6 +202,11 @@
   default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
   freshen' ctx = liftM (first to) . gfreshen ctx . from
 
+  -- | See 'Unbound.Generics.LocallyNameless.Operations.acompare'. An alpha-respecting total order on terms involving binders.
+  acompare' :: AlphaCtx -> a -> a -> Ordering
+  default acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering
+  acompare' c = (gacompare c) `on` from
+
 -- | The result of @'nthPatFind' a i@ is @Left k@ where @k@ is the
 -- number of names in pattern @a@ with @k < i@ or @Right x@ where @x@
 -- is the @i@th name in @a@
@@ -231,7 +237,9 @@
   gfreshen :: Fresh m => AlphaCtx -> f a -> m (f a, Perm AnyName)
 
   glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
-  
+
+  gacompare :: AlphaCtx -> f a -> f a -> Ordering
+
 instance (Alpha c) => GAlpha (K1 i c) where
   gaeq ctx (K1 c1) (K1 c2) = aeq' ctx c1 c2
 
@@ -251,6 +259,8 @@
 
   glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1)
 
+  gacompare ctx (K1 c1) (K1 c2) = acompare' ctx c1 c2
+
 instance GAlpha f => GAlpha (M1 i c f) where
   gaeq ctx (M1 f1) (M1 f2) = gaeq ctx f1 f2
 
@@ -264,13 +274,15 @@
 
   gnthPatFind = gnthPatFind . unM1
   gnamePatFind = gnamePatFind . unM1
-  
+
   gswaps ctx perm = M1 . gswaps ctx perm . unM1
   gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1
 
   glfreshen ctx (M1 f) cont =
     glfreshen ctx f (cont . M1)
 
+  gacompare ctx (M1 f1) (M1 f2) = gacompare ctx f1 f2
+
 instance GAlpha U1 where
   gaeq _ctx _ _ = True
 
@@ -290,6 +302,8 @@
 
   glfreshen _ctx _ cont = cont U1 mempty
 
+  gacompare _ctx _ _ = EQ
+
 instance GAlpha V1 where
   gaeq _ctx _ _ = False
 
@@ -309,6 +323,8 @@
 
   glfreshen _ctx _ cont = cont undefined mempty
 
+  gacompare _ctx _ _ = error "LocallyNameless.gacompare: undefined for empty data types"
+
 instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where
   gaeq ctx (f1 :*: g1) (f2 :*: g2) =
     gaeq ctx f1 f2 && gaeq ctx g1 g2
@@ -344,6 +360,9 @@
     glfreshen ctx (gswaps ctx perm2 f) $ \f' perm1 ->
     cont (f' :*: g') (perm1 <> perm2)
 
+  gacompare ctx (f1 :*: g1) (f2 :*: g2) =
+    (gacompare ctx f1 f2) <> (gacompare ctx g1 g2)
+
 instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where
   gaeq ctx  (L1 f1) (L1 f2) = gaeq ctx f1 f2
   gaeq ctx  (R1 g1) (R1 g2) = gaeq ctx g1 g2
@@ -379,8 +398,12 @@
     glfreshen ctx f (cont . L1)
   glfreshen ctx (R1 g) cont =
     glfreshen ctx g (cont . R1)
-  
 
+  gacompare _ctx (L1 _) (R1 _)   = LT
+  gacompare _ctx (R1 _) (L1 _)   = GT
+  gacompare ctx  (L1 f1) (L1 f2) = gacompare ctx f1 f2
+  gacompare ctx  (R1 g1) (R1 g2) = gacompare ctx g1 g2
+
 -- ============================================================
 -- Alpha instances for the usual types
 
@@ -402,6 +425,8 @@
   freshen' _ctx i = return (i, mempty)
   lfreshen' _ctx i cont = cont i mempty
 
+  acompare' _ctx i j = compare i j
+
 instance Alpha Char where
   aeq' _ctx i j = i == j
 
@@ -420,6 +445,8 @@
   freshen' _ctx i = return (i, mempty)
   lfreshen' _ctx i cont = cont i mempty
 
+  acompare' _ctx i j = compare i j
+
 instance Alpha Integer where
   aeq' _ctx i j = i == j
 
@@ -438,6 +465,8 @@
   freshen' _ctx i = return (i, mempty)
   lfreshen' _ctx i cont = cont i mempty
 
+  acompare' _ctx i j = compare i j
+
 instance Alpha Float where
   aeq' _ctx i j = i == j
 
@@ -456,6 +485,8 @@
   freshen' _ctx i = return (i, mempty)
   lfreshen' _ctx i cont = cont i mempty
 
+  acompare' _ctx i j = compare i j
+
 instance Alpha Double where
   aeq' _ctx i j = i == j
 
@@ -474,6 +505,8 @@
   freshen' _ctx i = return (i, mempty)
   lfreshen' _ctx i cont = cont i mempty
 
+  acompare' _ctx i j = compare i j
+
 instance (Integral n, Alpha n) => Alpha (Ratio n) where
   aeq' _ctx i j = i == j
 
@@ -492,6 +525,8 @@
   freshen' _ctx i = return (i, mempty)
   lfreshen' _ctx i cont = cont i mempty
 
+  acompare' _ctx i j = compare i j
+
 instance Alpha Bool
 
 instance Alpha a => Alpha (Maybe a)
@@ -575,6 +610,20 @@
       avoid [AnyName nm'] $ cont nm' $ single (AnyName nm) (AnyName nm')
     else error "lfreshen' on a Name in term position"
 
+  acompare' ctx (Fn s1 i1) (Fn s2 i2)
+    | isTermCtx ctx = (compare s1 s2) <> (compare i1 i2)
+
+  acompare' ctx n1@(Bn i1 j1) n2@(Bn i2 j2)
+    | isTermCtx ctx = mconcat [ compare (typeOf n1) (typeOf n2)
+                              , compare i1 i2
+                              , compare j1 j2
+                              ]
+
+  acompare' ctx (Fn _ _) (Bn _ _) | isTermCtx ctx = LT
+  acompare' ctx (Bn _ _) (Fn _ _) | isTermCtx ctx = GT
+
+  acompare' _ _          _                        = EQ
+
 instance Alpha AnyName where
   aeq' ctx x y =
     if x == y
@@ -624,3 +673,15 @@
     if nmHave == nmWant
     then Right 0
     else Left 1
+
+  acompare' _ x y | x == y = EQ
+
+  acompare' ctx (AnyName n1) (AnyName n2)
+    | isTermCtx ctx =
+      case compare (typeOf n1) (typeOf n2) of
+        EQ -> case gcast n2 of
+          Just n2' -> acompare' ctx n1 n2'
+          Nothing -> error "LocallyNameless.acompare': Equal type representations, but gcast failed in comparing two AnyName values"
+        ord -> ord
+
+  acompare' _ _ _ = EQ
diff --git a/src/Unbound/Generics/LocallyNameless/Bind.hs b/src/Unbound/Generics/LocallyNameless/Bind.hs
--- a/src/Unbound/Generics/LocallyNameless/Bind.hs
+++ b/src/Unbound/Generics/LocallyNameless/Bind.hs
@@ -75,3 +75,6 @@
     lfreshen' (patternCtx ctx) p $ \p' pm1 ->
     lfreshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) pm1 t) $ \t' pm2 ->
     cont (B p' t') (pm1 <> pm2)
+
+  acompare' ctx (B p1 t1) (B p2 t2) =
+    acompare' (patternCtx ctx) p1 p2 <> acompare' (incrLevelCtx ctx) t1 t2
diff --git a/src/Unbound/Generics/LocallyNameless/Embed.hs b/src/Unbound/Generics/LocallyNameless/Embed.hs
--- a/src/Unbound/Generics/LocallyNameless/Embed.hs
+++ b/src/Unbound/Generics/LocallyNameless/Embed.hs
@@ -75,3 +75,5 @@
 
   nthPatFind _ = Left
   namePatFind _ _ = Left 0
+
+  acompare' ctx (Embed x) (Embed y) = acompare' (termCtx ctx) x y
diff --git a/src/Unbound/Generics/LocallyNameless/Operations.hs b/src/Unbound/Generics/LocallyNameless/Operations.hs
--- a/src/Unbound/Generics/LocallyNameless/Operations.hs
+++ b/src/Unbound/Generics/LocallyNameless/Operations.hs
@@ -10,6 +10,7 @@
 module Unbound.Generics.LocallyNameless.Operations
        (-- * Equivalence, free variables, freshness
          aeq
+       , acompare
        , fvAny
        , fv
        , freshen
@@ -59,6 +60,10 @@
 -- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms.
 aeq :: Alpha a => a -> a -> Bool
 aeq = aeq' initialCtx
+
+-- | An alpha-respecting total order on terms involving binders.
+acompare :: Alpha a => a -> a -> Ordering
+acompare = acompare' initialCtx
 
 -- | @'fvAny'@ returns a fold over any names in a term @a@.
 --
diff --git a/src/Unbound/Generics/LocallyNameless/Rebind.hs b/src/Unbound/Generics/LocallyNameless/Rebind.hs
--- a/src/Unbound/Generics/LocallyNameless/Rebind.hs
+++ b/src/Unbound/Generics/LocallyNameless/Rebind.hs
@@ -81,3 +81,6 @@
 
   open ctx b (Rebnd p1 p2) = Rebnd (open ctx b p1) (open (incrLevelCtx ctx) b p2)
   close ctx b (Rebnd p1 p2) = Rebnd (close ctx b p1) (close (incrLevelCtx ctx) b p2)
+
+  acompare' ctx (Rebnd p1 p2) (Rebnd q1 q2) =
+    acompare' ctx p1 q1 <> acompare' (incrLevelCtx ctx) p2 q2
diff --git a/test/TestACompare.hs b/test/TestACompare.hs
new file mode 100644
--- /dev/null
+++ b/test/TestACompare.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
+module TestACompare where
+
+import Data.Typeable
+import GHC.Generics
+import Unbound.Generics.LocallyNameless
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+data Expr
+  = V (Name Expr)
+  | Add Expr Expr
+  | L (Bind (Name Expr) Expr)
+  deriving (Show,Generic,Typeable)
+
+instance Alpha Expr
+
+assertAcompare :: (Alpha t, Show t) => t -> t -> Ordering -> Assertion
+assertAcompare x y o =
+  let o' = acompare x y
+  in  assertBool (show x ++ " not alpha-" ++ show o' ++ " to " ++ show y ++ ", but alpha-" ++ show o) (o' == o)
+
+nameA, nameB, nameC :: Name Expr
+nameA = s2n "a"
+nameB = s2n "b"
+nameC = s2n "c"
+
+test_acompare :: TestTree
+test_acompare = testGroup "acompare"
+   -- Names compare in the obvious way.
+   [ testGroup "obvious"
+      [testCase "ac1 (a < b)"  $ assertAcompare nameA nameB LT
+      ,testCase "ac2 (b = b)" $ assertAcompare nameB nameB EQ
+      ,testCase "ac3 (b > a)"  $ assertAcompare nameB nameA GT
+      ]
+   -- structured date compares lexicographically
+   , testGroup "lexicographically"
+      [testCase "ac4 (a + a = a + a)" $
+        assertAcompare (Add (V nameA) (V nameA)) (Add (V nameA) (V nameA)) EQ
+      ,testCase "ac5 (a + a < a + b)" $
+        assertAcompare (Add (V nameA) (V nameA)) (Add (V nameA) (V nameB)) LT
+      ,testCase "ac6 (a + b > a + a)" $
+        assertAcompare (Add (V nameA) (V nameB)) (Add (V nameA) (V nameA)) GT
+      ,testCase "ac7 (a + a < b + a)" $
+        assertAcompare (Add (V nameA) (V nameA)) (Add (V nameB) (V nameA)) LT
+      ,testCase "ac8 (b + a > a + a)" $
+        assertAcompare (Add (V nameB) (V nameA)) (Add (V nameA) (V nameA)) GT
+      ,testCase "ac9 (b + a > a + b)" $
+        assertAcompare (Add (V nameB) (V nameA)) (Add (V nameA) (V nameB)) GT
+      ]
+   -- comparison goes under binders, alpha-respectingly.
+   , testGroup "binders"
+      [testCase "ac10 (\\a.a+a = \\b.b+b)" $
+        assertAcompare (bind nameA (Add (V nameA) (V nameA)))
+                       (bind nameB (Add (V nameB) (V nameB)))
+                       EQ
+      ,testCase "ac11 (\\a.a+a > \\a.a+b)" $
+        assertAcompare (bind nameA (Add (V nameA) (V nameA)))
+                       (bind nameA (Add (V nameA) (V nameB)))
+                       GT
+      ,testCase "ac12 (\\c.c+a < \\a.a+b)" $
+        assertAcompare (bind nameC (Add (V nameC) (V nameA)))
+                       (bind nameA (Add (V nameA) (V nameB)))
+                       LT
+      ]
+   -- non-matching binders handled alpha-respectingly.
+   , testGroup "non-matching binders"
+      [testCase "ac13 ((\\a.a `ac` \\a b.a) = (\\c.c `ac` \\a b.a))" $
+        assertAcompare (bind [nameA] nameA)
+                       (bind [nameA,nameB] nameA)
+                       (acompare (bind [nameC] nameC) (bind [nameA,nameB] nameA))
+      ,testCase "ac14 ((\\a b.a `ac` \\a.a) = (\\c b.c `ac` \\a.a))" $
+        assertAcompare (bind [nameA,nameB] nameA)
+                       (bind [nameA] nameA)
+                       (acompare (bind [nameC,nameB] nameC) (bind [nameA] nameA))
+      ]
+   -- non-binding stuff in patterns gets compared
+   , testGroup "non-binding stuff"
+      [testCase "ac15 (<a> < <b>)" $
+          assertAcompare (Embed nameA) (Embed nameB) LT
+      ,testCase "ac16 (\\c<a>.c+c < \\c<b>.c+c)" $
+        assertAcompare
+          (bind (nameC, Embed nameA) (Add (V nameC) (V nameC)))
+          (bind (nameC, Embed nameB) (Add (V nameC) (V nameC)))
+          LT
+      ,testCase "ac17 (\\c<a>.b+b < \\c<b>.a+a)" $
+        assertAcompare
+          (bind (nameC, Embed nameA) (Add (V nameB) (V nameB)))
+          (bind (nameC, Embed nameB) (Add (V nameA) (V nameA)))
+          LT
+      ]
+   ]
diff --git a/test/TinyLam.hs b/test/TinyLam.hs
--- a/test/TinyLam.hs
+++ b/test/TinyLam.hs
@@ -55,6 +55,7 @@
   swaps' _ctx _p x = x
   freshen' _ctx x = return (x, mempty)
   lfreshen' _ctx x cont = cont x mempty
+  acompare' _ctx (ArithOp s1 _) (ArithOp s2 _) = compare s1 s2
 
 instance Alpha Expr
 instance Alpha Fun
diff --git a/test/test-main.hs b/test/test-main.hs
--- a/test/test-main.hs
+++ b/test/test-main.hs
@@ -6,6 +6,7 @@
 import TestParallelReduction
 import PropOpenClose
 import TinyLam
+import TestACompare
 
 main :: IO ()
 main = defaultMain $ testGroup "unboundGenerics"
@@ -14,4 +15,5 @@
        , test_parallelReduction
        , test_openClose
        , test_tinyLam
+       , test_acompare
        ]
diff --git a/unbound-generics.cabal b/unbound-generics.cabal
--- a/unbound-generics.cabal
+++ b/unbound-generics.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                unbound-generics
-version:             0.0.3
+version:             0.1
 synopsis:            Reimplementation of Unbound using GHC Generics
 description:         Specify the binding structure of your data type with an
                      expressive set of type combinators, and unbound-generics
@@ -66,6 +66,7 @@
                        TestParallelReduction
                        PropOpenClose
                        TinyLam
+                       TestACompare
   build-depends:       base,
                        mtl,
                        tasty,