diff --git a/.travis.yml b/.travis.yml
new file mode 100644
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,1 @@
+language: haskell
diff --git a/Bound.hs b/Bound.hs
new file mode 100644
--- /dev/null
+++ b/Bound.hs
@@ -0,0 +1,22 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Bound
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Bound
+  ( module Bound.Var
+  , module Bound.Class
+  , module Bound.Scope
+  , module Bound.Term
+  ) where
+
+import Bound.Var
+import Bound.Class
+import Bound.Scope
+import Bound.Term
diff --git a/Bound/Class.hs b/Bound/Class.hs
new file mode 100644
--- /dev/null
+++ b/Bound/Class.hs
@@ -0,0 +1,34 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Bound.Class
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Bound.Class
+  ( Bound(..)
+  , (=<<<)
+  ) where
+
+infixl 1 >>>=
+
+-- | This may or may not be a monad transformer,
+--
+-- If it is, then you can use @m >>>= f = m >>= lift . f@
+--
+-- This is useful for types like expression lists, case alternatives,
+-- schemas, etc. that may not be expressions in their own right, but often
+-- contain one.
+
+class Bound t where
+  (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
+  -- default (>>>=) :: MonadTrans t, Monad f) => t f a -> (a -> f c) -> t f c
+  -- m >>>= f = m >>= lift . f
+
+infixr 1 =<<<
+(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
+(=<<<) = flip (>>>=)
diff --git a/Bound/Scope.hs b/Bound/Scope.hs
new file mode 100644
--- /dev/null
+++ b/Bound/Scope.hs
@@ -0,0 +1,147 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Bound.Scope
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Bound.Scope
+  ( Scope(..)
+  -- * Abstraction
+  , abstract, abstract1
+  -- * Instantiation
+  , instantiate, instantiate1
+  -- * Substitution
+  , splat
+  -- * Quotienting
+  , fromScope
+  , toScope
+  ) where
+
+import Data.Foldable
+import Data.Traversable
+import Control.Monad
+import Control.Monad.Trans.Class
+import Control.Applicative
+import Prelude.Extras
+import Bound.Class
+import Bound.Var
+
+-- | @Scope b f a@ is a an @f@ expression with bound variables in @b@, and free variables in @a@
+--
+-- This stores bound variables as their generalized de Bruijn representation,
+-- in that the succ's for variable ids are allowed to occur anywhere within the tree
+-- permitting /O(1)/ weakening and allowing more sharing opportunities. 
+-- Here the deBruijn 0 is represented by the 'B' constructor of 'Var', while the 
+-- de Bruijn 'succ' (which may be applied to an entire tree!) is handled by 'F'.
+--
+-- NB: equality and comparison quotient out the distinct 'F' placements allowed by 
+-- the choice of a generalized de Bruijn representation and return the same result as a traditional de Bruijn
+-- representation would.
+
+newtype Scope b f a = Scope { unscope :: f (Var b (f a)) }
+
+instance Functor f => Functor (Scope b f) where
+  fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a)
+
+-- | @toList@ is provides a list (with duplicates) of the free variables
+instance Foldable f => Foldable (Scope b f) where
+  foldMap f (Scope a) = foldMap (foldMap (foldMap f)) a
+
+instance Traversable f => Traversable (Scope b f) where
+  traverse f (Scope a) = Scope <$> traverse (traverse (traverse f)) a
+
+-- | The monad permits substitution on free variables, while preserving bound variables
+instance Monad f => Monad (Scope b f) where
+  return a = Scope (return (F (return a)))
+  Scope e >>= f = Scope $ e >>= \v -> case v of
+    B b -> return (B b)
+    F ea -> ea >>= unscope . f
+
+instance MonadTrans (Scope b) where
+  lift m = Scope (return (F m))
+
+instance (Monad f, Eq b, Eq1 f, Eq a) => Eq  (Scope b f a) where (==) = (==#)
+instance (Monad f, Eq b, Eq1 f)       => Eq1 (Scope b f)   where
+  a ==# b = liftM Lift2 (fromScope a) ==# liftM Lift2 (fromScope b)
+  -- a ==# b = mangleScope a ==# mangleScope b
+
+instance (Monad f, Ord b, Ord1 f, Ord a) => Ord  (Scope b f a) where compare = compare1
+instance (Monad f, Ord b, Ord1 f)        => Ord1 (Scope b f) where
+  compare1 a b = liftM Lift2 (fromScope a) `compare1` liftM Lift2 (fromScope b)
+  -- compare1 a b = compare1 (mangleScope a) (mangleScope b)
+
+mangleScope :: Functor f => Scope b f a -> f (Lift2 Var b (Lift1 f a))
+mangleScope (Scope a) = fmap (Lift2 . fmap Lift1) a
+{-# INLINE mangleScope #-}
+
+unmangleScope :: Functor f => f (Lift2 Var b (Lift1 f a)) -> Scope b f a
+unmangleScope a = Scope (fmap (fmap lower1 . lower2) a)
+{-# INLINE unmangleScope #-}
+
+
+instance (Functor f, Show b, Show1 f, Show a) => Show  (Scope b f a) where showsPrec = showsPrec1
+instance (Functor f, Show b, Show1 f)         => Show1 (Scope b f)   where
+  showsPrec1 d a = showParen (d > 10) $ showString "Scope " . showsPrec1 11 (mangleScope a)
+
+instance (Functor f, Read b, Read1 f, Read a) => Read  (Scope b f a) where readsPrec = readsPrec1
+instance (Functor f, Read b, Read1 f)         => Read1 (Scope b f) where
+  readPrec1 = liftM unmangleScope readPrec1
+
+instance Bound (Scope b) where
+  m >>>= f = m >>= lift . f
+
+-- | Capture some free variables in an expression to yield a Scope with bound variables
+abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
+abstract f e = Scope (liftM k e) where
+  k y = case f y of
+    Just z  -> B z
+    Nothing -> F (return y)
+{-# INLINE abstract #-}
+
+-- | Abstract over a single variable
+abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
+abstract1 a = abstract (\b -> if a == b then Just () else Nothing)
+{-# INLINE abstract1 #-}
+
+-- | Enter a scope, instantiating all bound variables
+instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
+instantiate k e = unscope e >>= \v -> case v of
+  B b -> k b
+  F a -> a
+{-# INLINE instantiate #-}
+
+-- | Enter a scope with one bound variable, instantiating it
+instantiate1 :: Monad f => f a -> Scope () f a -> f a
+instantiate1 e = instantiate (\ () -> e)
+{-# INLINE instantiate1 #-}
+
+
+-- | @fromScope@ quotients out the possible placements of F in Scope
+-- distributing them all to the leaves. This yields a traditional deBruijn
+-- indexing scheme for bound variables.
+--
+-- > fromScope . toScope = id
+-- > fromScope . toScope . fromScope = fromScope
+--
+-- @(toScope . fromScope)@ is idempotent
+fromScope :: Monad f => Scope b f a -> f (Var b a)
+fromScope (Scope s) = s >>= \v -> case v of
+  F e -> liftM F e
+  B b -> return (B b)
+{-# INLINE fromScope #-}
+
+toScope :: Monad f => f (Var b a) -> Scope b f a
+toScope e = Scope (liftM (fmap return) e)
+{-# INLINE toScope #-}
+
+-- | Perform substitution on both bound and free variables in a scope
+splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c
+splat f unbind s = unscope s >>= \v -> case v of
+  B b -> unbind b
+  F ea -> ea >>= f
+{-# INLINE splat #-}
diff --git a/Bound/Term.hs b/Bound/Term.hs
new file mode 100644
--- /dev/null
+++ b/Bound/Term.hs
@@ -0,0 +1,33 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Bound.Term
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Bound.Term
+  ( substitute
+  , isClosed
+  , closed
+  ) where
+
+import Data.Traversable
+import Data.Maybe (isJust)
+
+-- | @substitute p a w@ replaces the free variable @a@ with @p@ in @w@
+substitute :: (Monad f, Eq a) => f a -> a -> f a -> f a
+substitute p a w = w >>= \b -> if a == b then p else return b
+{-# INLINE substitute #-}
+
+-- | If a term has no free variables, you can freely change the type of free variables it uses
+closed :: Traversable f => f a -> Maybe (f b)
+closed = traverse (const Nothing)
+{-# INLINE closed #-}
+
+isClosed :: Traversable f => f a -> Bool
+isClosed = isJust . closed
+{-# INLINE isClosed #-}
diff --git a/Bound/Var.hs b/Bound/Var.hs
new file mode 100644
--- /dev/null
+++ b/Bound/Var.hs
@@ -0,0 +1,74 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Bound.Var
+-- Copyright   :  (C) 2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Bound.Var (Var(..)) where
+
+import Data.Foldable
+import Data.Traversable
+import Data.Monoid (mempty)
+import Data.Bifunctor
+import Data.Bifoldable
+import Data.Bitraversable
+import Control.Applicative
+import Control.Monad (ap)
+import Prelude.Extras
+import Text.Read
+
+-- | "I am not a number, I am a /free monad/!"
+--
+-- @Var b a@ represents variables that may either be "bound" (@B@) or "free" (@F@)
+data Var b a
+  = B b -- this is a bound variable
+  | F a -- this is a free variable
+  deriving (Eq,Ord,Show,Read)
+
+instance Functor (Var b) where
+  fmap _ (B b) = B b
+  fmap f (F a) = F (f a)
+
+instance Foldable (Var b) where
+  foldMap f (F a) = f a
+  foldMap _ _ = mempty
+
+instance Traversable (Var b) where
+  traverse f (F a) = F <$> f a
+  traverse _ (B b) = pure (B b)
+
+instance Applicative (Var b) where
+  pure = F
+  (<*>) = ap
+
+instance Monad (Var b) where
+  return = F
+  F a  >>= f = f a
+  B b >>= _ = B b
+
+instance Bifunctor Var where
+  bimap f _ (B b) = B (f b)
+  bimap _ g (F a) = F (g a)
+
+instance Bifoldable Var where
+  bifoldMap f _ (B b) = f b
+  bifoldMap _ g (F a) = g a
+
+instance Bitraversable Var where
+  bitraverse f _ (B b) = B <$> f b
+  bitraverse _ g (F a) = F <$> g a
+
+instance Eq2 Var   where (==##)     = (==)
+instance Ord2 Var  where compare2   = compare
+instance Show2 Var where showsPrec2 = showsPrec
+instance Read2 Var where readPrec2  = readPrec
+
+instance Eq b   => Eq1   (Var b) where (==#)      = (==)
+instance Ord b  => Ord1  (Var b) where compare1   = compare
+instance Show b => Show1 (Var b) where showsPrec1 = showsPrec
+instance Read b => Read1 (Var b) where readPrec1  = readPrec
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright 2012 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,7 @@
+#!/usr/bin/runhaskell
+> module Main (main) where
+
+> import Distribution.Simple
+
+> main :: IO ()
+> main = defaultMain
diff --git a/bound.cabal b/bound.cabal
new file mode 100644
--- /dev/null
+++ b/bound.cabal
@@ -0,0 +1,37 @@
+name:          bound
+category:      Language, Compilers/Interpreters
+version:       0.1
+license:       BSD3
+cabal-version: >= 1.6
+license-file:  LICENSE
+author:        Edward A. Kmett
+maintainer:    Edward A. Kmett <ekmett@gmail.com>
+stability:     experimental
+homepage:      http://github.com/ekmett/bound/
+bug-reports:   http://github.com/ekmett/bound/issues
+copyright:     Copyright (C) 2012 Edward A. Kmett
+synopsis:      Combinators for manipulating locally-nameless generalized de Bruijn terms
+description:   Combinators for manipulating locally-nameless generalized de Bruijn terms
+
+build-type:    Simple
+extra-source-files: .travis.yml examples/Simple.hs examples/Exp.hs
+
+source-repository head
+  type: git
+  location: git://github.com/ekmett/bound.git
+
+library
+  build-depends:
+    base           >= 4     && < 5,
+    bifunctors     >= 0.1.3 && < 0.2,
+    prelude-extras >= 0.2   && < 0.3,
+    transformers   >= 0.2   && < 0.4
+
+  exposed-modules:
+    Bound
+    Bound.Class
+    Bound.Scope
+    Bound.Term
+    Bound.Var
+
+  ghc-options: -Wall
diff --git a/examples/Exp.hs b/examples/Exp.hs
new file mode 100644
--- /dev/null
+++ b/examples/Exp.hs
@@ -0,0 +1,308 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeOperators #-}
+module Exp where
+
+
+import Data.Vector as Vector hiding ((++), map)
+import Data.List as List
+import Data.Foldable
+import Data.Traversable
+import Data.Monoid (Monoid(..))
+import Control.Monad
+import Control.Monad.Trans.Class
+import Control.Applicative
+import Prelude hiding (foldr)
+import Prelude.Extras
+import GHC.Prim (Constraint(..))
+import Unsafe.Coerce
+import Bound
+
+-- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")
+-- Let (fromList [Scope (Var (B 1)),Scope (Var (B 0) :@ Var (B 1))]) (Scope (Lam VarP (Scope (Var (B V) :@ Var (F (Var (B 1)))))))
+--
+-- ghc> lam (varp "x") (Var "x")
+-- ghc> lam (conp "Hello" [varp "x", wildp])) (Var "y")
+
+infixl 9 :@
+infixr 5 :>
+
+-- little orphan instances
+instance Show1 Vector where showsPrec1 = showsPrec
+instance Eq1 Vector where (==#) = (==)
+
+data Exp a
+  = Var a
+  | Exp a :@ Exp a
+  | forall (b :: Index). Lam (Pat b Exp a) (Scope (Path b) Exp a)
+  | Let (Vector (Scope Int Exp a)) (Scope Int Exp a)
+  -- | Case (Exp a) [Alt Exp a]
+
+data Alt f a = forall b. Alt (Pat b f a) (Scope (Path b) Exp a)
+
+data Index = VarI | WildI | AsI Index | ConI [Index]
+
+data Pat :: Index -> (* -> *) -> * -> * where
+  VarP  ::                             Pat VarI f a
+  WildP ::                             Pat WildI f a
+  AsP   :: Pat i f a                -> Pat (AsI i) f a
+  ConP  :: String    -> Pats bs f a -> Pat (ConI bs) f a
+  ViewP :: f a       -> Pat b f a   -> Pat b f a -- TODO: allow references to earlier variables
+
+data Pats :: [Index] -> (* -> *) -> * -> * where
+  NilP  :: Pats '[] f a
+  (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a
+
+data Path :: Index -> * where
+  V :: Path VarI
+  L :: Path (AsI a)
+  R :: Path a -> Path (AsI a)
+  C :: MPath as -> Path (ConI as)
+
+data MPath :: [Index] -> * where
+  H :: Path a   -> MPath (a ':as)
+  T :: MPath as -> MPath (a ':as)
+
+instance Functor Exp where
+  fmap = fmapDefault
+
+instance Foldable Exp where
+  foldMap = foldMapDefault
+
+instance Applicative Exp where
+  pure = Var
+  (<*>) = ap
+
+instance Traversable Exp where
+  traverse f (Var a)    = Var <$> f a
+  traverse f (x :@ y)   = (:@) <$> traverse f x <*> traverse f y
+  traverse f (Lam p e)  = Lam <$> traverse f p <*> traverse f e
+  traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e
+
+instance Monad Exp where
+  return         = Var
+  Var a    >>= f = f a
+  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
+  Lam p e  >>= f = Lam (p >>>= f) (e >>>= f)
+  Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f)
+ -- Case e as >>= f = Case (e >>= f) (fmap (>>>= f) as)
+
+instance Eq a => Eq (Exp a) where (==) = (==#)
+instance Eq1 Exp where
+  Var a     ==# Var b     = a == b
+  (a :@ b)  ==# (c :@ d)  = a ==# c && b ==# d
+  Lam ps a  ==# Lam qs b  = eqPat ps qs && a ==# unsafeCoerce b -- eqPat proves equal shape
+  Let as a  ==# Let bs b  = as == bs && a ==# b
+ -- Case e as ==# Case f bs = e ==# f && as == bs
+  _         ==# _         = False
+
+instance Show a => Show (Exp a) where showsPrec = showsPrec1
+instance Show1 Exp where
+  showsPrec1 d (Var a)    = showParen (d > 10) $ showString "Var " . showsPrec 11 a
+  showsPrec1 d (a :@ b)   = showParen (d > 9) $ showsPrec1 9 a . showString " :@ " . showsPrec1 10 b
+  showsPrec1 d (Lam ps b) = showParen (d > 10) $ showString "Lam " . showsPrec1 11 ps . showChar ' ' . showsPrec1 11 b
+  showsPrec1 d (Let bs b) = showParen (d > 10) $ showString "Let " . showsPrec1 11 bs . showChar ' ' . showsPrec1 11 b
+
+{-
+instance Eq1 f => Eq1 (Alt f) where
+  Alt p s ==# Alt q t = eqPat p q && s == unsafeCoerce t
+
+instance (Eq1 f, Eq a) => Eq (Alt f) where (==) = (==#)
+
+instance Show1 f => Show1 (Alt f) where
+  showsPrec d (Alt p s) = showsPrec d (Alt p s)
+-}
+
+
+-- * smart lam
+
+-- ** smart patterns
+
+data P a = forall b. P (Pat b Exp a) [a] (a -> Maybe (Path b))
+
+varp :: Eq a => a -> P a
+varp a = P VarP [a] (\v -> if a == v then Just V else Nothing)
+
+wildp :: P a
+wildp = P WildP [] (const Nothing)
+
+asp :: Eq a => a -> P a -> P a
+asp a (P p as f) = P (AsP p) (a:as) $ \v -> case f v of
+  Just b              -> Just (R b)
+  Nothing | a == v    -> Just L
+          | otherwise -> Nothing
+
+data Ps a = forall bs. Ps (Pats bs Exp a) [a] (a -> Maybe (MPath bs))
+
+conp :: String -> [P a] -> P a
+conp g ps = case go ps of
+  Ps qs as f -> P (ConP g qs) as (fmap C . f)
+  where
+    go :: [P a] -> Ps a
+    go [] = Ps NilP [] (const Nothing)
+    go (P p as f : xs) = case go xs of
+      Ps ps ass g -> Ps (p :> ps) (as ++ ass) $ \v ->
+        T <$> g v <|> H <$> f v
+
+-- * smart lam
+lam :: P a -> Exp a -> Exp a
+lam (P p _ f) t = Lam p (abstract f t)
+
+-- * smart let
+let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a
+let_ bs b = Let (Vector.fromList $ map (abstr . snd) bs) (abstr b)
+  where vs  = map fst bs
+        abstr = abstract (`List.elemIndex` vs)
+
+-- * Pat
+
+-- ** A Kind of Shape
+
+eqPat :: (Eq1 f, Eq a) => Pat b f a -> Pat b' f a -> Bool
+eqPat VarP        VarP        = True
+eqPat WildP       WildP       = True
+eqPat (AsP p)     (AsP q)     = eqPat p q
+eqPat (ConP g ps) (ConP h qs) = g == h  && eqPats ps qs
+eqPat (ViewP e p) (ViewP f q) = e ==# f && eqPat p q
+
+instance Eq1 f   => Eq1 (Pat b f)        where (==#) = eqPat
+instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eqPat
+
+instance Show1 f => Show1 (Pat b f) where showsPrec1 = showsPrec
+instance (Show1 f, Show a) => Show (Pat b f a) where
+  showsPrec _ VarP        = showString "VarP"
+  showsPrec _ WildP       = showString "WildP"
+  showsPrec d (AsP p)     = showParen (d > 10) $ showString "AsP " . showsPrec 11 p
+  showsPrec d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . showsPrec 11 ps
+  showsPrec d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . showsPrec1 11 e . showChar ' ' . showsPrec 11 p
+
+instance Functor f => Functor (Pat b f) where
+  fmap _ VarP = VarP
+  fmap _ WildP = WildP
+  fmap f (AsP p) = AsP (fmap f p)
+  fmap f (ConP g ps) = ConP g (fmap f ps)
+  fmap f (ViewP e p) = ViewP (fmap f e) (fmap f p)
+
+instance Foldable f => Foldable (Pat b f) where
+  foldMap f (AsP p)     = foldMap f p
+  foldMap f (ConP g ps) = foldMap f ps
+  foldMap f (ViewP e p) = foldMap f e `mappend` foldMap f p
+  foldMap _ _           = mempty
+
+instance Traversable f => Traversable (Pat b f) where
+  traverse _ VarP = pure VarP
+  traverse _ WildP = pure WildP
+  traverse f (AsP p) = AsP <$> traverse f p
+  traverse f (ConP g ps) = ConP g <$> traverse f ps
+  traverse f (ViewP e p) = ViewP <$> traverse f e <*> traverse f p
+
+instance Bound (Pat b) where
+  VarP      >>>= _ = VarP
+  WildP     >>>= _ = WildP
+  AsP p     >>>= f = AsP (p >>>= f)
+  ConP g ps >>>= f = ConP g (ps >>>= f)
+  ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)
+
+-- ** Pats
+
+
+eqPats :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Bool
+eqPats NilP      NilP      = True
+eqPats (p :> ps) (q :> qs) = eqPat p q && eqPats ps qs
+eqPats _         _         = False
+
+instance Eq1 f         => Eq1 (Pats bs f)   where (==#) = eqPats
+instance (Eq1 f, Eq a) => Eq  (Pats bs f a) where (==)  = eqPats
+
+instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1
+instance Show1 f => Show1 (Pats bs f) where
+  showsPrec1 _ NilP      = showString "NilP"
+  showsPrec1 d (p :> ps) = showParen (d > 5) $
+    showsPrec1 6 p . showString " :> " . showsPrec1 5 ps
+
+instance Functor f => Functor (Pats bs f) where
+  fmap _ NilP = NilP
+  fmap f (p :> ps) = fmap f p :> fmap f ps
+
+instance Foldable f => Foldable (Pats bs f) where
+  foldMap f (p :> ps) = foldMap f p `mappend` foldMap f ps
+  foldMap _ _    = mempty
+
+instance Traversable f => Traversable (Pats bs f) where
+  traverse f NilP = pure NilP
+  traverse f (p :> ps) = (:>) <$> traverse f p <*> traverse f ps
+
+instance Bound (Pats bs) where
+  NilP >>>= _ = NilP
+  (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f)
+
+
+-- ** Path into Pats
+
+eqMPath :: MPath is -> MPath js -> Bool
+eqMPath (H m) (H n) = eqPath m n
+eqMPath (T p) (T q) = eqMPath p q
+eqMPath _     _     = False
+instance Eq (MPath is) where (==) = eqMPath
+
+compareMPath :: MPath is -> MPath js -> Ordering
+compareMPath (H m) (H n) = comparePath m n
+compareMPath (H _) (T _) = LT
+compareMPath (T p) (T q) = compareMPath p q
+compareMPath (T _) (H _) = GT
+instance Ord (MPath is) where compare = compareMPath
+
+instance Show (MPath is) where
+  showsPrec d (H m) = showParen (d > 10) $ showString "H " . showsPrec 11 m
+  showsPrec d (T p) = showParen (d > 10) $ showString "T " . showsPrec 11 p
+
+-- instance Read (MPath is)
+
+-- ** Path into Pat
+
+
+eqPath :: Path i -> Path j -> Bool
+eqPath V     V     = True
+eqPath L     L     = True
+eqPath (R m) (R n) = eqPath m n
+eqPath (C p) (C q) = eqMPath p q
+eqPath _     _     = False
+
+instance Eq (Path i) where (==) = eqPath
+
+comparePath :: Path i -> Path j -> Ordering
+comparePath V     V     = EQ
+comparePath V     _     = LT
+comparePath L     V     = GT
+comparePath L     L     = EQ
+comparePath L     _     = LT
+comparePath (R _) V     = GT
+comparePath (R _) L     = GT
+comparePath (R m) (R n) = comparePath m n
+comparePath (R _) (C _) = LT
+comparePath (C p) (C q) = compareMPath p q
+comparePath (C _) _     = GT
+
+instance Ord (Path i) where
+  compare V     V     = EQ
+  compare L     L     = EQ
+  compare L     _     = LT
+  compare (R _) L     = GT
+  compare (R m) (R n) = compare m n
+  compare (C p) (C q) = compare p q
+
+instance Show (Path i) where
+  showsPrec _ V     = showString "V"
+  showsPrec _ L     = showString "L"
+  showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m
+  showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p
+
+
diff --git a/examples/Simple.hs b/examples/Simple.hs
new file mode 100644
--- /dev/null
+++ b/examples/Simple.hs
@@ -0,0 +1,52 @@
+module Simple where
+
+import Data.Foldable
+import Data.Traversable
+import Control.Monad
+import Control.Applicative
+import Prelude hiding (foldr)
+import Prelude.Extras
+import Bound
+
+-- \ x -> x
+-- ghci> lam "x" (Var "x")
+-- Lam (Var (Bound ()))
+
+-- \ x -> x y
+-- ghci> lam "x" (Var "x" :@ Var "y")
+-- Lam (Var (Bound ()) :@ Var (Free (Var "y")))
+
+-- \ y -> \x -> x y
+-- ghci> lam "y" (lam "x" (Var "x" :@ Var "y"))
+-- Lam (Lam (Var (Bound ()) :@ Var (Free (Var (Bound ())))))
+
+infixl 9 :@
+
+data Exp a = Var a | Exp a :@ Exp a | Lam (Scope () Exp a)
+  deriving (Eq,Ord,Show,Read)
+
+
+lam :: Eq a => a -> Exp a -> Exp a
+lam v b = Lam (abstract1 v b)
+
+instance Eq1 Exp      where (==#)      = (==)
+instance Ord1 Exp     where compare1   = compare
+instance Show1 Exp    where showsPrec1 = showsPrec
+instance Read1 Exp    where readsPrec1 = readsPrec
+instance Functor Exp  where fmap       = fmapDefault
+instance Foldable Exp where foldMap    = foldMapDefault
+
+instance Applicative Exp where
+  pure  = Var
+  (<*>) = ap
+
+instance Traversable Exp where
+  traverse f (Var a)  = Var <$> f a
+  traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y
+  traverse f (Lam e)  = Lam <$> traverse f e
+
+instance Monad Exp where
+  return         = Var
+  Var a    >>= f = f a
+  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
+  Lam e    >>= f = Lam (e >>>= f)