diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,9 @@
+# 0.0.2
+
+* Add 'Rec' pattern and 'TRec' term combinators.
+
+* Alpha instance for '()'
+
 # 0.0.1
 
 * Add 'lunbind2' function.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -9,7 +9,7 @@
 
 For the most part, I tried to keep the same methods with the same signatures.  However there are a few differences.
 
-1. `fv :: Alpha t => t -> Fold t (Name n)`
+1. `fv :: Alpha t => Fold t (Name n)`
 
    The `fv` method returns a `Fold` (in the sense of the [lens](http://hackage.haskell.org/package/lens) library),
    rather than an `Unbound.Util.Collection` instance.  That means you will generally have to write `toListOf fv t` or some    other summary operation.
diff --git a/src/Unbound/Generics/LocallyNameless.hs b/src/Unbound/Generics/LocallyNameless.hs
--- a/src/Unbound/Generics/LocallyNameless.hs
+++ b/src/Unbound/Generics/LocallyNameless.hs
@@ -14,6 +14,7 @@
   module Unbound.Generics.LocallyNameless.Bind,
   module Unbound.Generics.LocallyNameless.Embed,
   module Unbound.Generics.LocallyNameless.Rebind,
+  module Unbound.Generics.LocallyNameless.Rec,
   module Unbound.Generics.LocallyNameless.Fresh,
   module Unbound.Generics.LocallyNameless.LFresh,
   module Unbound.Generics.LocallyNameless.Subst
@@ -24,6 +25,7 @@
 import Unbound.Generics.LocallyNameless.Bind hiding (B)
 import Unbound.Generics.LocallyNameless.Embed
 import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)
+import Unbound.Generics.LocallyNameless.Rec
 import Unbound.Generics.LocallyNameless.Fresh
 import Unbound.Generics.LocallyNameless.LFresh
 import Unbound.Generics.LocallyNameless.Operations
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
@@ -124,7 +124,10 @@
   aeq' c = (gaeq c) `on` from
 
   -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.
-  -- @@@ fvAny' :: AlphaCtx -> Fold a AnyName @@@
+  --
+  -- @
+  --  fvAny' :: Fold a AnyName
+  -- @
   fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
   default fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
   fvAny' c nfn = fmap to . gfvAny c nfn . from
@@ -481,6 +484,7 @@
 
 instance Alpha a => Alpha (Maybe a)
 instance Alpha a => Alpha [a]
+instance Alpha ()
 instance (Alpha a,Alpha b) => Alpha (Either a b)
 instance (Alpha a,Alpha b) => Alpha (a,b)
 instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)
diff --git a/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs b/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs
--- a/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs
+++ b/src/Unbound/Generics/LocallyNameless/Internal/Fold.hs
@@ -5,9 +5,11 @@
 -- Maintainer : Aleksey Kliger
 -- Stability  : experimental
 --
--- | Some utilities for working with Folds.
+-- Some utilities for working with Folds.
+--
+-- If you are using <http://hackage.haskell.org/package/lens lens>, you don't need this module.
 {-# LANGUAGE RankNTypes #-}
-module Unbound.Generics.LocallyNameless.Internal.Fold (Fold, Traversal', toListOf, filtered, justFiltered) where
+module Unbound.Generics.LocallyNameless.Internal.Fold (Fold, Traversal', toListOf, filtered, justFiltered, foldMapOf) where
 
 import Control.Applicative
 import Data.Maybe (fromJust)
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
@@ -30,6 +30,14 @@
        , Embed(..)
        , embed
        , unembed
+         -- * Recursive bindings
+       , Rec
+       , Unbound.Generics.LocallyNameless.Rec.rec
+       , Unbound.Generics.LocallyNameless.Rec.unrec
+       , TRec(..)
+       , trec
+       , untrec
+       , luntrec
        ) where
 
 import Control.Applicative (Applicative)
@@ -44,6 +52,7 @@
 import Unbound.Generics.LocallyNameless.Bind
 import Unbound.Generics.LocallyNameless.Embed (Embed(..))
 import Unbound.Generics.LocallyNameless.Rebind
+import Unbound.Generics.LocallyNameless.Rec
 import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)
 import Unbound.Generics.PermM
 
@@ -51,18 +60,18 @@
 aeq :: Alpha a => a -> a -> Bool
 aeq = aeq' initialCtx
 
--- | @'fvAny' t@ returns the free variables of the term @t@.
+-- | @'fvAny'@ returns a fold over any names in a term @a@.
 --
 -- @
---   fvAny :: Alpha a => a -> Fold a AnyName
+--   fvAny :: Alpha a => Fold a AnyName
 -- @
 fvAny :: (Alpha a, Contravariant f, Applicative f) => (AnyName -> f AnyName) -> a -> f a
 fvAny = fvAny' initialCtx
 
--- | @'fv' t@ returns the free @b@ variables of term @t@.
+-- | @'fv'@ returns the free @b@ variables of term @a@.
 --
 -- @
---  fv :: (Alpha a, Typeable b) => a -> Fold a (Name b)
+--  fv :: (Alpha a, Typeable b) => Fold a (Name b)
 -- @
 fv :: forall a f b . (Alpha a, Typeable b, Contravariant f, Applicative f)
       => (Name b -> f (Name b)) -> a -> f a
@@ -177,3 +186,20 @@
 -- | @'unembed' p@ extracts the term embedded in the pattern @p@.
 unembed :: Embed t -> t
 unembed (Embed t) = t
+
+-- | Constructor for recursive abstractions.
+trec :: Alpha p => p -> TRec p
+trec p = TRec (bind (rec p) ())
+
+-- | Destructor for recursive abstractions which picks globally fresh
+--   names for the binders.
+untrec :: (Alpha p, Fresh m) => TRec p -> m p
+untrec (TRec b) = do
+  (p, ()) <- unbind b
+  return (unrec p)
+
+-- | Destructor for recursive abstractions which picks /locally/ fresh
+--   names for binders (see 'LFresh').
+luntrec :: (Alpha p, LFresh m) => TRec p -> m p
+luntrec (TRec b) =
+  lunbind b $ \(p, ()) -> return (unrec p)
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
@@ -31,12 +31,10 @@
 --
 -- @
 -- type Var = Name Expr
--- data Lets = EmptyLets
---           | Bind (Rebind (Var, Embed Expr) Lets)
+-- data Lets = EmptyLs
+--           | ConsLs (Rebind (Var, Embed Expr) Lets)
 -- data Expr = ...
---           | LetStar { letStarBindings :: Lets
---                     , letStarBody :: Expr
---                     }
+--           | LetStar (Bind Lets Expr)
 --           | ...
 -- @
 data Rebind p1 p2 = Rebnd p1 p2
diff --git a/src/Unbound/Generics/LocallyNameless/Rec.hs b/src/Unbound/Generics/LocallyNameless/Rec.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Rec.hs
@@ -0,0 +1,67 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Rec
+-- Copyright  : (c) 2014, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- The pattern @'Rec' p@ binds the names in @p@ like @p@ itself would,
+-- but additinoally, the names in @p@ are scope over @p@.
+--
+-- The term @'TRec' p@ is shorthand for @'Bind' (Rec p) ()@
+{-# LANGUAGE DeriveGeneric #-}
+module Unbound.Generics.LocallyNameless.Rec
+       (
+         Rec
+       , rec
+       , unrec
+       , TRec (..)
+       ) where
+
+import GHC.Generics (Generic)
+
+import Unbound.Generics.LocallyNameless.Alpha
+import Unbound.Generics.LocallyNameless.Bind
+
+-- | If @p@ is a pattern type, then @Rec p@ is also a pattern type,
+-- which is /recursive/ in the sense that @p@ may bind names in terms
+-- embedded within itself.  Useful for encoding e.g. lectrec and
+-- Agda's dot notation.
+newtype Rec p = Rec p
+              deriving (Generic, Eq)
+
+instance Show a => Show (Rec a) where
+  showsPrec _ (Rec a) = showString "[" . showsPrec 0 a . showString "]"
+
+-- | @TRec@ is a standalone variant of 'Rec': the only difference is
+--   that whereas @'Rec' p@ is a pattern type, @TRec p@
+--   is a /term type/.  It is isomorphic to @'Bind' ('Rec' p) ()@.
+--
+--   Note that @TRec@ corresponds to Pottier's /abstraction/ construct
+--   from alpha-Caml.  In this context, @'Embed' t@ corresponds to
+--   alpha-Caml's @inner t@, and @'Shift' ('Embed' t)@ corresponds to
+--   alpha-Caml's @outer t@.
+newtype TRec p = TRec (Bind (Rec p) ())
+                 deriving (Generic)
+
+instance Show a => Show (TRec a) where
+  showsPrec _ (TRec (B (Rec p) ())) = showString "[" . showsPrec 0 p . showString "]"
+
+
+instance Alpha p => Alpha (Rec p) where
+  isTerm _ = False
+  isPat (Rec p) = isPat p
+
+  open ctx b (Rec p) = Rec (open (incrLevelCtx ctx) b p)
+  close ctx b (Rec p) = Rec (close (incrLevelCtx ctx) b p)
+
+instance Alpha p => Alpha (TRec p)
+
+-- | Constructor for recursive patterns.
+rec :: Alpha p => p -> Rec p
+rec p = Rec (close (patternCtx initialCtx) p p)
+
+-- | Destructor for recursive patterns.
+unrec :: Alpha p => Rec p -> p
+unrec (Rec p) = open (patternCtx initialCtx) p p
diff --git a/src/Unbound/Generics/LocallyNameless/Subst.hs b/src/Unbound/Generics/LocallyNameless/Subst.hs
--- a/src/Unbound/Generics/LocallyNameless/Subst.hs
+++ b/src/Unbound/Generics/LocallyNameless/Subst.hs
@@ -57,6 +57,7 @@
 import Unbound.Generics.LocallyNameless.Embed
 import Unbound.Generics.LocallyNameless.Bind
 import Unbound.Generics.LocallyNameless.Rebind
+import Unbound.Generics.LocallyNameless.Rec
 
 -- | See 'isVar'
 data SubstName a b where
@@ -175,3 +176,7 @@
 instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)
 
 instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)
+
+instance (Subst c p) => Subst c (Rec p)
+
+instance (Alpha p, Subst c p) => Subst c (TRec p)
diff --git a/test/PropOpenClose.hs b/test/PropOpenClose.hs
new file mode 100644
--- /dev/null
+++ b/test/PropOpenClose.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
+module PropOpenClose (test_openClose) where
+
+import Control.Applicative (Applicative(..), (<$>))
+import Data.Monoid (Any(..))
+import Data.Typeable (Typeable)
+import GHC.Generics (Generic)
+
+import Test.QuickCheck
+import Test.Tasty (testGroup, TestTree)
+import Test.Tasty.QuickCheck (testProperty)
+
+import Unbound.Generics.LocallyNameless
+import Unbound.Generics.LocallyNameless.Internal.Fold (foldMapOf, toListOf)
+
+----------------------------------------
+-- Property testing utilities
+
+isFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool
+isFreeIn = elementOf fv
+  where
+    elementOf l = anyOf l . (==)
+    anyOf l f = getAny . foldMapOf l (Any . f)
+
+notFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool
+notFreeIn v = not . isFreeIn v
+
+(=~=) :: (Alpha a, Show a) => a -> a -> Property
+x =~= y = counterexample (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)
+
+(/~@) :: (Typeable a, Alpha b, Show b) => Name a -> b -> Property
+v /~@ t = counterexample (show v ++ " is free in " ++ show t) (v `notFreeIn` t)
+
+-- Wrapper around 'Name a' that has an Arbitrary instance that generates free names.
+-- Note that this doesn't guarantee /freshness/.  The name may clash with some other one.
+-- But it will never be a bound name.
+newtype FreeName a = FreeName {getFreeName :: Name a}
+                     deriving (Show)
+
+instance Arbitrary (FreeName a) where
+  arbitrary = do
+    s <- listOf1 (elements ['a'..'z'])
+    n <- arbitrary
+    return $ FreeName $ makeName s n
+  shrink = const []
+
+----------------------------------------
+-- example data structure, with no bound names.
+
+data T a = Leaf !a
+         | V !(Name (T a))
+         | B !(T a) !(T a)
+         deriving (Show, Typeable, Generic)
+
+instance (Typeable a, Alpha a) => Alpha (T a)
+
+instance Arbitrary a => Arbitrary (T a) where
+  arbitrary =
+    oneof
+    [
+      Leaf <$> arbitrary
+    ,(V . getFreeName) <$> arbitrary
+    , B <$> arbitrary <*> arbitrary
+    ]
+
+-- generator that picks out one of the free variables of a tree
+arbVarsOf :: (Alpha a, Typeable a) => T a -> Gen (Name (T a))
+arbVarsOf t =
+  let vs = toListOf fv t
+  in  elements vs
+
+-- spec for free variables of a tree.
+-- fvSpec :: Traversal' (T a) (Name (T a))
+fvSpec :: Applicative f => (Name (T a) -> f (Name (T a))) -> T a -> f (T a)
+fvSpec f t =
+  case t of
+   Leaf {} -> pure t
+   V v -> V <$> f v
+   B t1 t2 -> B <$> fvSpec f t1 <*> fvSpec f t2
+
+----------------------------------------
+-- Properties
+
+-- every tree is alpha-equivalent to itself
+prop_refl :: T Int -> Property
+prop_refl x = x =~= x
+
+-- generic fv gives the same answer as fvSpec
+prop_fv_spec :: T Int -> Property
+prop_fv_spec t = toListOf fv t === toListOf fvSpec t
+  
+-- if a name is already free opening it has no effect
+prop_open_idempotent :: T Int -> Property
+prop_open_idempotent t =
+  forAll (arbVarsOf t) $ \v -> open initialCtx v t =~= t
+
+-- if you close over a variable, then it is no longer free.
+prop_close_binds :: T Int -> Property
+prop_close_binds t =
+  (not $ null $ toListOf fvAny t) ==>
+  forAll (arbVarsOf t) $ \v -> v /~@ close initialCtx v t
+
+----------------------------------------
+-- Test group
+
+test_openClose :: TestTree
+test_openClose =
+  testGroup "QuickCheck properties"
+  [
+    testProperty "reflexivity" prop_refl
+  , testProperty "fv specification" prop_fv_spec
+  , testProperty "open idempotency" prop_open_idempotent
+  , testProperty "closing binds variables" prop_close_binds
+  ]
diff --git a/test/TinyLam.hs b/test/TinyLam.hs
new file mode 100644
--- /dev/null
+++ b/test/TinyLam.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, FlexibleContexts #-}
+module TinyLam where
+
+import GHC.Generics (Generic)
+import Data.Typeable (Typeable)
+
+import Control.Applicative (Applicative(..))
+import Control.Monad.Reader
+import Data.Monoid (Monoid(..))
+import qualified Data.List 
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Unbound.Generics.LocallyNameless
+
+
+type Var = Name Expr
+
+data ArithOp = ArithOp String (Int -> Int -> Int)
+             deriving (Typeable, Generic)
+
+instance Show ArithOp where
+  show (ArithOp f _) = f
+
+data Expr = V Var
+          | I Int
+          | Arith ArithOp Expr Expr
+          | Lam Fun
+          | App Expr Expr
+          | If0 Expr Expr Expr
+          | Letrec (Bind (Rec (Var, Embed Fun)) Expr)
+          deriving (Typeable, Generic, Show)
+
+newtype Fun = Fun (Bind Var Expr)
+            deriving (Typeable, Generic, Show)
+
+instance Eq Expr where
+  (==) = aeq
+
+instance Eq Fun where
+  (==) = aeq
+
+-- leaf instance for ArithOp
+instance Alpha ArithOp where
+  aeq' _ctx (ArithOp s1 _) (ArithOp s2 _) = s1 == s2
+  fvAny' _ctx _nfn x = pure x
+  close _ctx _b x = x
+  open _ctx _b x = x
+  isPat _ = mempty
+  isTerm _ = True
+  nthPatFind _ = Left
+  namePatFind _ _ = Left 0
+
+  swaps' _ctx _p x = x
+  freshen' _ctx x = return (x, mempty)
+  lfreshen' _ctx x cont = cont x mempty
+
+instance Alpha Expr
+instance Alpha Fun
+
+type Env = [(Var, Value)]
+
+data Value = VI !Int
+           | VClo !Env !Fun
+           deriving (Eq, Show) 
+
+
+emptyEnv :: Env
+emptyEnv = []
+
+extendEnv :: Var -> Value -> Env -> Env
+extendEnv x v rho = (x,v) : rho
+
+env :: MonadReader Env m => m Env
+env = ask
+
+lookupV :: MonadReader Env m => Var -> m Value
+lookupV x = env >>= \rho ->
+  case Data.List.lookup x rho of
+   Just v -> return v
+   Nothing -> error $ "unbound variable " ++ show x
+
+eval :: (Fresh m, MonadReader Env m) => Expr -> m Value
+eval (V x) = lookupV x
+eval (I i) = return $ VI i
+eval (Lam f) = env >>= \rho -> return (VClo rho f)
+eval (App e1 e2) = do
+  v1 <- eval e1
+  case v1 of
+   (VClo rho (Fun bnd)) -> do
+     v2 <- eval e2
+     (x, e3) <- unbind bnd
+     local (const $ extendEnv x v2 rho) $ eval e3
+   _ -> error ("expected a function, but got " ++ show v1)
+eval (Arith (ArithOp _ op) e1 e2) = do
+  v1 <- eval e1
+  v2 <- eval e2
+  case (v1, v2) of
+   (VI n1, VI n2) -> return $ VI (op n1 n2)
+   _ -> error ("expected pair of ints, but got " ++ show v1
+               ++ " and " ++ show v2)
+eval (If0 e1 e2 e3) = do
+  v1 <- eval e1
+  case v1 of
+   VI 0 -> eval e2
+   VI _ -> eval e3
+   _ -> error ("expected int, but got " ++ show v1)
+eval (Letrec bnd) = do
+  (r, ebody) <- unbind bnd
+  rho0 <- ask
+  let (f, Embed fun) = unrec r
+      -- N.B. knot tying
+      rho = extendEnv f vclo rho0
+      vclo = VClo rho fun
+  local (extendEnv f vclo) $ eval ebody
+
+runEval :: Expr -> Value
+runEval e = runReader (runFreshMT (eval e)) emptyEnv
+
+ex_f :: Int -> Expr
+ex_f n = let
+  (/*/) = Arith (ArithOp "*" (*))
+  (/-/) = Arith (ArithOp "-" (-))
+  fact = s2n "fact"
+  x = s2n "x"
+  body = If0 (V x)
+         {-then-} (I 1)
+         {-else-} (V x
+                   /*/ 
+                   App (V fact) (V x /-/ I 1))
+  factfun = Fun (bind x body)
+  in Letrec $ bind (rec (fact, Embed factfun))
+     (App (V fact) (I n))
+
+test_ex_f0 :: TestTree
+test_ex_f0 =
+  testCase "eval (fact 0) = 1"
+  $ assertEqual "" (runEval (ex_f 0)) (VI 1)
+
+test_ex_f5 :: TestTree
+test_ex_f5 =
+  testCase "eval (fact 5) = 120"
+  $ assertEqual "" (runEval (ex_f 5)) (VI 120)
+
+test_tinyLam :: TestTree
+test_tinyLam =
+  testGroup "tinyLam"
+  [ test_ex_f0
+  , test_ex_f5
+  ]
diff --git a/test/test-main.hs b/test/test-main.hs
--- a/test/test-main.hs
+++ b/test/test-main.hs
@@ -4,9 +4,14 @@
 
 import TestCalc
 import TestParallelReduction
+import PropOpenClose
+import TinyLam
 
+main :: IO ()
 main = defaultMain $ testGroup "unboundGenerics"
        [
          test_calc
        , test_parallelReduction
+       , test_openClose
+       , test_tinyLam
        ]
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.1
+version:             0.0.2
 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
@@ -42,6 +42,7 @@
                        Unbound.Generics.LocallyNameless.Operations
                        Unbound.Generics.LocallyNameless.Unsafe
                        Unbound.Generics.LocallyNameless.Internal.Fold
+                       Unbound.Generics.LocallyNameless.Rec
                        Unbound.Generics.PermM
                        Unbound.Generics.LocallyNameless.Subst
   -- other-modules:       
@@ -62,10 +63,14 @@
                        TestCalc
                        ParallelReduction
                        TestParallelReduction
+                       PropOpenClose
+                       TinyLam
   build-depends:       base,
                        mtl,
                        tasty,
                        tasty-hunit,
+                       tasty-quickcheck,
+                       QuickCheck >= 2.7 && < 3,
                        unbound-generics
   hs-source-dirs:      test
   default-language:    Haskell2010