diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,7 @@
+# Revision history for binder
+
+## version 0
+
+### 0.1 -- 2023-10-04
+
+Initial release.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2023 Keito Kajitani
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/binder.cabal b/binder.cabal
new file mode 100644
--- /dev/null
+++ b/binder.cabal
@@ -0,0 +1,70 @@
+cabal-version:      3.0
+name:               binder
+version:            0.1
+synopsis:           Variable binding for abstract syntax tree
+description:
+    binder is purely functional implementation of Ocaml's
+    <https://github.com/rlepigre/ocaml-bindlib bindlib>.
+    It follows the style of higher-order abstract syntax,
+    and offers the representation of abstract syntax tree.
+license:            MIT
+license-file:       LICENSE
+author:             Keito Kajitani <ijaketak@gmail.com>
+maintainer:         Keito Kajitani <ijaketak@gmail.com>
+copyright:          (c) 2023 Keito Kajitani
+homepage:           https://github.com/ijaketak/binder
+category:           Data
+build-type:         Simple
+tested-with:
+      GHC == 9.2.8
+    , GHC == 9.4.7
+    , GHC == 9.6.3
+extra-doc-files:    CHANGELOG.md
+-- extra-source-files:
+
+source-repository head
+    type:     git
+    location: https://github.com/ijaketak/binder
+
+source-repository this
+    type:     git
+    location: https://github.com/ijaketak/binder
+    tag:      0.1
+
+common depends
+    build-depends:
+          containers < 0.8
+        , text < 2.2
+        , transformers < 0.7
+
+common warnings
+    ghc-options: -Wall
+
+library
+    import:           depends, warnings
+    exposed-modules:
+          Data.Binder
+    -- other-modules:
+    -- other-extensions:
+    build-depends:
+          base < 4.19
+        , lens < 5.3
+    hs-source-dirs:   src
+    default-language: Haskell2010
+
+test-suite binder-test
+    import:           depends, warnings
+    default-language: Haskell2010
+    other-modules:
+          Binder1Spec
+        , Binder2Spec
+    -- other-extensions:
+    type:             exitcode-stdio-1.0
+    hs-source-dirs:   test
+    main-is:          Spec.hs
+    build-depends:
+          base < 4.19
+        , binder
+        , hspec < 2.12
+    build-tool-depends:
+          hspec-discover:hspec-discover < 2.12
diff --git a/src/Data/Binder.hs b/src/Data/Binder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binder.hs
@@ -0,0 +1,255 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-|
+Module      : Data.Binder
+Description : Variable binding for abstract syntax tree
+Copyright   : (c) 2023 Keito Kajitani
+License     : MIT
+Maintainer  : Keito Kajitani <ijaketak@gmail.com>
+
+binder is purely functional implementation of Ocaml's bindlib.
+It follows the style of higher-order abstract syntax,
+and offers the representation of abstract syntax tree.
+-}
+module Data.Binder
+-- * Preliminaries
+  ( MonadNumbering(..)
+-- * Variable and Box
+  , Var
+  , Box
+  , MkFree(..)
+-- ** Variable
+  , var'Key
+  , var'Name
+  , var'Box
+  , nameOf
+  , boxVar
+  , newVar
+  , isClosed
+  , occur
+-- ** Box
+  , unbox
+  , box
+  , apBox
+  , boxApply
+  , boxApply2
+  , boxApply3
+  , boxApply4
+  , boxPair
+  , boxTriple
+  , boxT
+-- * Variable binding
+  , Binder
+  , binder'Name
+  , binder'Body
+  , subst
+  , buildBinder
+  , bind
+  , unbind
+  , eqBinder
+  , boxBinder
+  ) where
+
+import Control.Lens
+import Data.Kind (Type)
+import qualified Data.Map.Lazy as M
+import Data.Maybe (fromJust)
+import Data.Text (Text)
+import Unsafe.Coerce
+
+-- | Numbering monad.
+class (Monad m, Ord (Numbering m)) => MonadNumbering m where
+  type Numbering m :: Type
+  numbering :: m (Numbering m)
+
+-- | Representation of variable
+--   for abstract syntax tree type @a@
+--   with base numbering monad @m@.
+data Var m a = Var
+  { _var'Key :: !(Numbering m)
+  , _var'Body :: VarBody m a
+  }
+data VarBody m a = VarBody
+  { _varBody'Name :: Text
+  , _varBody'Box :: Box m a
+  }
+-- | Representation of under-construction things
+--   having type @a@ and containing variables.
+data Box m a
+  = Box'Closed a
+  | Box'Env (EnvVar m) (Closure m a)
+
+-- | Typeclass for free variable constructor.
+class MkFree m a where
+  mkFree :: Var m a -> a
+
+data AnyVar m = forall a. MkFree m a => AnyVar (Var m a)
+type EnvVar m = M.Map (Numbering m) (AnyVar m)
+data AnyMkFree m = forall a. MkFree m a => AnyMkFree a
+type EnvMkFree m = M.Map (Numbering m) (AnyMkFree m)
+newtype Closure m a = Closure { unClosure :: (EnvMkFree m) -> a }
+
+instance Functor (Closure m) where
+  fmap f cla = Closure $ f . unClosure cla
+
+instance Applicative (Closure m) where
+  pure a = Closure $ const a
+  clf <*> cla = Closure $ \env -> unClosure clf env $ unClosure cla env
+
+instance MonadNumbering m => Eq (Var m a) where
+  Var x _ == Var y _ = x == y
+
+instance MonadNumbering m => Ord (Var m a) where
+  Var x _ `compare` Var y _ = x `compare` y
+
+$(makeLenses ''Var)
+$(makeLenses ''VarBody)
+
+
+var'Name :: Lens' (Var m a) Text
+var'Name = var'Body . varBody'Name
+var'Box :: Lens' (Var m a) (Box m a)
+var'Box = var'Body . varBody'Box
+
+instance Show (Var m a) where
+  showsPrec n x = showsPrec n $ x ^. var'Name
+instance Show (VarBody m a) where
+  showsPrec n x = showsPrec n $ x ^. varBody'Name
+instance Show (AnyVar m) where
+  showsPrec n (AnyVar x) = showsPrec n $ x ^. var'Name
+
+-- | The name of variable.
+nameOf :: Var m a -> Text
+nameOf x = x ^. var'Name
+
+-- | Smart constructor for 'Box'.
+boxVar :: Var m a -> Box m a
+boxVar x = x ^. var'Box
+
+-- | Create a new variable with given name.
+newVar :: forall m a. (MkFree m a, MonadNumbering m) => Text -> m (Var m a)
+newVar name = do
+  i <- numbering
+  let x = let b = Box'Env
+                (M.singleton i $ AnyVar x)
+                (Closure $ \env ->
+                  let f (AnyMkFree y) = unsafeCoerce y
+                   in f $ fromJust $ M.lookup i env)
+           in Var i $ VarBody name b
+  return x
+
+
+-- | 'Box' is closed if it exposes no free variables.
+isClosed :: Box m a -> Bool
+isClosed Box'Closed{} = True
+isClosed Box'Env{} = False
+
+-- | Check if the variable occurs in the box.
+occur :: MonadNumbering m => Var m a -> Box m b -> Bool
+occur _ (Box'Closed _) = False
+occur v (Box'Env vs _) = M.member (v ^. var'Key) vs
+
+
+instance Functor (Box m) where
+  fmap f (Box'Closed a) = Box'Closed (f a)
+  fmap f (Box'Env vs ta) = Box'Env vs (f <$> ta)
+
+instance (MonadNumbering m) => Applicative (Box m) where
+  pure = Box'Closed
+  Box'Closed f <*> Box'Closed a = Box'Closed (f a)
+  Box'Closed f <*> Box'Env va ta = Box'Env va (f <$> ta)
+  Box'Env vf tf <*> Box'Closed a = Box'Env vf (appClosure tf a)
+   where
+    appClosure clf x = Closure $ \env -> unClosure clf env x
+  Box'Env vf tf <*> Box'Env va ta = Box'Env (M.union vf va) (tf <*> ta)
+
+-- | Pick out and complete the construction of @a@.
+unbox :: forall m a. Box m a -> a
+unbox (Box'Closed t) = t
+unbox (Box'Env env cl) = unClosure cl $ f <$> env
+ where
+  f (AnyVar x) = AnyMkFree @m $ mkFree x
+
+box :: MonadNumbering m => a -> Box m a
+box = pure
+apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b
+apBox = (<*>)
+boxApply :: (a -> b) -> Box m a -> Box m b
+boxApply = fmap
+boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c
+boxApply2 f ta tb = f <$> ta <*> tb
+boxApply3 :: MonadNumbering m => (a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d
+boxApply3 f ta tb tc = f <$> ta <*> tb <*> tc
+boxApply4 :: MonadNumbering m => (a -> b -> c -> d -> e) -> Box m a -> Box m b -> Box m c -> Box m d -> Box m e
+boxApply4 f ta tb tc td = f <$> ta <*> tb <*> tc <*> td
+boxPair :: MonadNumbering m => Box m a -> Box m b -> Box m (a, b)
+boxPair = boxApply2 (,)
+boxTriple :: MonadNumbering m => Box m a -> Box m b -> Box m c -> Box m (a, b, c)
+boxTriple = boxApply3 (,,)
+boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a)
+boxT = sequenceA
+
+
+-- | Variable binding.
+--   Essentially, @Binder a b@ means @a -> b@.
+data Binder a b = Binder
+  { _binder'Name :: Text
+  , _binder'Body :: a -> b
+  }
+
+$(makeLenses ''Binder)
+
+-- | Variable substitution.
+subst :: Binder a b -> a -> b
+subst b = b ^. binder'Body
+
+-- | unbinding
+unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)
+unbind b = do
+  x <- newVar $ b ^. binder'Name
+  return (x, subst b $ mkFree x)
+
+unbind2 :: (MkFree m a, MonadNumbering m)
+        => Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)
+unbind2 b1 b2 = do
+  x <- newVar $ b1 ^. binder'Name
+  let v = mkFree x
+  return (x, subst b1 v, subst b2 v)
+
+-- | Check if two bindings are equal.
+eqBinder :: (MkFree m a, MonadNumbering m)
+         => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool
+eqBinder eq f g = do
+  (_, t, u) <- unbind2 f g
+  eq t u
+
+
+-- | Smart constructor for 'Binder'.
+buildBinder :: Var m a -> (a -> b) -> Binder a b
+buildBinder x body = Binder (x ^. var'Name) body
+
+-- | binding
+bind :: (MkFree m a, MonadNumbering m)
+        => Var m a -> Box m b -> Box m (Binder a b)
+bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const t
+bind x (Box'Env vs t) =
+  let vs' = M.delete (x ^. var'Key) vs in if length vs' == 0
+    then Box'Closed $ buildBinder x $
+      \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyMkFree arg)
+    else Box'Env vs' $ Closure $
+      \ms -> buildBinder x $
+      \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyMkFree arg) ms
+
+boxBinder :: (MkFree m a, MonadNumbering m)
+          => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))
+boxBinder f b = do
+  (x, t) <- unbind b
+  ft <- f t
+  return $ bind x ft
diff --git a/test/Binder1Spec.hs b/test/Binder1Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Binder1Spec.hs
@@ -0,0 +1,147 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Binder1Spec where
+
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Trans.State.Strict (evalStateT, get, modify, StateT)
+import Data.Text (Text)
+import GHC.Generics hiding (S)
+import Prelude hiding (abs)
+import Test.Hspec
+
+import Data.Binder
+
+newtype S a = S { runS :: StateT Int IO a }
+  deriving
+  ( Generic
+  , Generic1
+  , Functor
+  , Applicative
+  , Monad
+  , MonadIO
+  )
+
+instance MonadNumbering S where
+  type Numbering S = Int
+  numbering = do
+    i <- S $ get
+    S $ modify succ
+    return i
+
+-- This example is stolen from the documentation of bindlib.
+-- https://github.com/rlepigre/ocaml-bindlib/blob/master/lib/bindlib.mli
+
+data Term
+  = Term'Var (Var S Term)
+  | Term'Abs (Binder Term Term)
+  | Term'App Term Term
+
+instance MkFree S Term where
+  mkFree = Term'Var
+
+var :: Var S Term -> Box S Term
+var = boxVar
+absRaw :: Box S (Binder Term Term) -> Box S Term
+absRaw = fmap Term'Abs
+abs :: Var S Term -> Box S Term -> Box S Term
+abs x t = absRaw $ bind x t
+app :: Box S Term -> Box S Term -> Box S Term
+app t u = Term'App <$> t <*> u
+boxTerm :: Term -> S (Box S Term)
+boxTerm (Term'Var x) = return $ var x
+boxTerm (Term'Abs b) = absRaw <$> boxBinder boxTerm b
+boxTerm (Term'App t u) = app <$> boxTerm t <*> boxTerm u
+
+eval :: Term -> Term
+eval t@(Term'App f a) = case eval f of
+  Term'Abs b -> eval (subst b a)
+  _ -> t
+eval t = t
+
+size :: Term -> S Int
+size (Term'Var _) = return 0
+size (Term'Abs b) = do
+  (_, t) <- unbind b
+  i <- size t
+  return $ succ i
+size (Term'App t u) = do
+  i <- size t
+  j <- size u
+  return $ succ $ i + j
+
+showTerm :: Term -> S Text
+showTerm (Term'Var x) = return $ nameOf x
+showTerm (Term'Abs b) = do
+  (x, t) <- unbind b
+  sh <- showTerm t
+  return $ "\\" <> nameOf x <> "." <> sh
+showTerm (Term'App t u) = do
+  sht <- showTerm t
+  shu <- showTerm u
+  return $ "(" <> sht <> ") (" <> shu <> ")"
+
+termIdentity, termFst, termDelta, termOmega :: S Term
+termIdentity = do
+  x <- newVar "x"
+  return $ unbox $ abs x $ var x
+termFst = do
+  x <- newVar "x"
+  y <- newVar "y"
+  return $ unbox $ abs x $ abs y $ var x
+termDelta = do
+  x <- newVar "x"
+  return $ unbox $ abs x $ app (var x) (var x)
+termOmega = do
+  delta <- box <$> termDelta
+  return $ unbox $ app delta delta
+
+spec :: Spec
+spec = do
+  describe "termIdentity" $ do
+    it "should be size 1" $ do
+      let r = 1
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termIdentity
+        size t
+    it "should be shown the intended text" $ do
+      let r = "\\x.x"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termIdentity
+        showTerm t
+  describe "termFst" $ do
+    it "should be size 2" $ do
+      let r = 2
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termFst
+        size t
+    it "should be shown the intended text" $ do
+      let r = "\\x.\\y.x"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termFst
+        showTerm t
+  describe "termDelta" $ do
+    it "should be size 2" $ do
+      let r = 2
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termDelta
+        size t
+    it "should be shown the intended text" $ do
+      let r = "\\x.(x) (x)"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termDelta
+        showTerm t
+  describe "termOmega" $ do
+    it "should be size 5" $ do
+      let r = 5
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termOmega
+        size t
+    it "should be shown the intended text" $ do
+      let r = "(\\x.(x) (x)) (\\x.(x) (x))"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- termOmega
+        showTerm t
diff --git a/test/Binder2Spec.hs b/test/Binder2Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Binder2Spec.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Binder2Spec where
+
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Trans.State.Strict (evalStateT, get, modify, StateT)
+import qualified Data.Map.Lazy as M
+import Data.Text (Text)
+import GHC.Generics hiding (S)
+import Test.Hspec
+
+import Data.Binder
+
+newtype S a = S { runS :: StateT Int IO a }
+  deriving
+  ( Generic
+  , Generic1
+  , Functor
+  , Applicative
+  , Monad
+  , MonadIO
+  )
+
+instance MonadNumbering S where
+  type Numbering S = Int
+  numbering = do
+    i <- S $ get
+    S $ modify succ
+    return i
+
+-- This example is stolen from the paper
+-- Abstract Representation of Binders in OCaml using the Bindlib Library.
+-- https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LFMTP2018.4
+
+data Ty
+  = Ty'Var (Var S Ty)
+  | Ty'Arr Ty Ty
+  | Ty'All (Binder Ty Ty)
+
+data Te
+  = Te'Var (Var S Te)
+  | Te'Abs Ty (Binder Te Te)
+  | Te'App Te Te
+  | Te'Lam (Binder Ty Te)
+  | Te'Spe Te Ty
+
+instance MkFree S Ty where
+  mkFree = Ty'Var
+instance MkFree S Te where
+  mkFree = Te'Var
+
+ty'Var :: Var S Ty -> Box S Ty
+ty'Var = boxVar
+ty'Arr :: Box S Ty -> Box S Ty -> Box S Ty
+ty'Arr a b = Ty'Arr <$> a <*> b
+ty'AllRaw :: Box S (Binder Ty Ty) -> Box S Ty
+ty'AllRaw = fmap Ty'All
+ty'All :: Var S Ty -> Box S Ty -> Box S Ty
+ty'All x t = ty'AllRaw $ bind x t
+
+te'Var :: Var S Te -> Box S Te
+te'Var = boxVar
+te'AbsRaw :: Box S Ty -> Box S (Binder Te Te) -> Box S Te
+te'AbsRaw a f = Te'Abs <$> a <*> f
+te'Abs :: Box S Ty -> Var S Te -> Box S Te -> Box S Te
+te'Abs a x t = te'AbsRaw a $ bind x t
+te'App :: Box S Te -> Box S Te -> Box S Te
+te'App t u = Te'App <$> t <*> u
+te'LamRaw :: Box S (Binder Ty Te) -> Box S Te
+te'LamRaw = fmap Te'Lam
+te'Lam :: Var S Ty -> Box S Te -> Box S Te
+te'Lam x t = te'LamRaw $ bind x t
+te'Spe :: Box S Te -> Box S Ty -> Box S Te
+te'Spe t a = Te'Spe <$> t <*> a
+
+boxTy :: Ty -> S (Box S Ty)
+boxTy (Ty'Var x) = return $ ty'Var x
+boxTy (Ty'Arr a b) = ty'Arr <$> boxTy a <*> boxTy b
+boxTy (Ty'All f) = ty'AllRaw <$> boxBinder boxTy f
+boxTe :: Te -> S (Box S Te)
+boxTe (Te'Var x) = return $ te'Var x
+boxTe (Te'Abs a f) = te'AbsRaw <$> boxTy a <*> boxBinder boxTe f
+boxTe (Te'App t u) = te'App <$> boxTe t <*> boxTe u
+boxTe (Te'Lam f) = te'LamRaw <$> boxBinder boxTe f
+boxTe (Te'Spe t a) = te'Spe <$> boxTe t <*> boxTy a
+
+hnf :: Te -> Te
+hnf (Te'App t u) = let v = hnf u in case hnf t of
+  Te'Abs _ b -> hnf $ subst b v
+  h -> Te'App h v
+hnf (Te'Spe t a) = case hnf t of
+  Te'Lam b -> hnf $ subst b a
+  h -> Te'Spe h a
+hnf t = t
+
+nf :: Te -> S Te
+nf (Te'Abs a f) = do
+  (x, t) <- unbind f
+  nt <- nf t
+  bt <- boxTe nt
+  return $ Te'Abs a $ unbox $ bind x bt
+nf (Te'App t u) = do
+  nt <- nf t
+  nu <- nf u
+  case nt of
+    Te'Abs _ f -> nf $ subst f u
+    _ -> return $ Te'App nt nu
+nf (Te'Lam f) = do
+  (x, t) <- unbind f
+  nt <- nf t
+  bt <- boxTe nt
+  return $ Te'Lam $ unbox $ bind x bt
+nf (Te'Spe t a) = do
+  nt <- nf t
+  case nt of
+    Te'Lam f -> nf $ subst f a
+    _ -> return $ Te'Spe nt a
+nf t = return t
+
+eqTy :: Ty -> Ty -> S Bool
+eqTy (Ty'Var x1) (Ty'Var x2) = return $ x1 == x2
+eqTy (Ty'Arr a1 b1) (Ty'Arr a2 b2) = do
+  ca <- eqTy a1 a2
+  cb <- eqTy b1 b2
+  return $ ca && cb
+eqTy (Ty'All f1) (Ty'All f2) = eqBinder eqTy f1 f2
+eqTy _ _ = return False
+
+type Ctxt = M.Map (Var S Te) Ty
+
+infer :: Ctxt -> Te -> S (Maybe Ty)
+infer ctxt (Te'Var x) = return $ M.lookup x ctxt
+infer ctxt (Te'Abs a f) = do
+  (x, t) <- unbind f
+  mtyt <- infer (M.insert x a ctxt) t
+  return $ Ty'Arr a <$> mtyt
+infer ctxt (Te'App t u) = do
+  mtyt <- infer ctxt t
+  case mtyt of
+    Just (Ty'Arr a b) -> do
+      mtyu <- infer ctxt u
+      case mtyu of
+        Just tyu -> do
+          e <- eqTy tyu a
+          return $ if e then Just b else Nothing
+        Nothing -> return Nothing
+    _ -> return Nothing
+infer ctxt (Te'Lam f) = do
+  (x, t) <- unbind f
+  mtyt <- infer ctxt t
+  case mtyt of
+    Just tyt -> do
+      bt <- boxTy tyt
+      return $ Just $ Ty'All $ unbox $ bind x bt
+    Nothing -> return Nothing
+infer ctxt (Te'Spe t a) = do
+  mtyt <- infer ctxt t
+  case mtyt of
+    Just (Ty'All f) -> return $ Just $ subst f a
+    _ -> return Nothing
+
+check :: Ctxt -> Te -> Ty -> S Bool
+check ctxt t a = do
+  mtyt <- infer ctxt t
+  case mtyt of
+    Just tyt -> eqTy tyt a
+    Nothing -> return False
+
+showTy :: Ty -> S Text
+showTy (Ty'Var x) = return $ nameOf x
+showTy (Ty'Arr a b) = do
+  sha <- showTy a
+  shb <- showTy b
+  return $ "(" <> sha <> ") => (" <> shb <> ")"
+showTy (Ty'All f) = do
+  (x, t) <- unbind f
+  sh <- showTy t
+  return $ "\\" <> nameOf x <> "." <> sh
+
+showTe :: Te -> S Text
+showTe (Te'Var x) = return $ nameOf x
+showTe (Te'Abs a f) = do
+  sha <- showTy a
+  (x, t) <- unbind f
+  sht <- showTe t
+  return $ "\\l " <> nameOf x <> ":" <> sha <> "." <> sht
+showTe (Te'App t u) = do
+  sht <- showTe t
+  shu <- showTe u
+  return $ "(" <> sht <> ") (" <> shu <> ")"
+showTe (Te'Lam f) = do
+  (x, t) <- unbind f
+  sh <- showTe t
+  return $ "\\L " <> nameOf x <> "." <> sh
+showTe (Te'Spe t a) = do
+  sht <- showTe t
+  sha <- showTy a
+  return $ "(" <> sht <> ") (" <> sha <> ")"
+
+type1, type2 :: S Ty
+term1 :: S Te
+type1 = do
+  x <- newVar "X"
+  y <- newVar "Y"
+  return $ unbox $ ty'Arr (ty'Var x) (ty'Var y)
+type2 = do
+  x <- newVar "X"
+  y <- newVar "Y"
+  let arr = ty'Arr (ty'Var x) (ty'Var y)
+  return $ unbox $ ty'All x $ ty'All y $ ty'Arr arr arr
+term1 = do
+  x <- newVar "X"
+  y <- newVar "Y"
+  f <- newVar "f"
+  a <- newVar "a"
+  let arr = ty'Arr (ty'Var x) (ty'Var y)
+  return $ unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $
+    te'App (te'Var f) (te'Var a)
+
+spec :: Spec
+spec = do
+  describe "type1" $ do
+    it "should be shown the intended text" $ do
+      let r = "(X) => (Y)"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- type1
+        showTy t
+  describe "type2" $ do
+    it "should be shown the intended text" $ do
+      let r = "\\X.\\Y.((X) => (Y)) => ((X) => (Y))"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- type2
+        showTy t
+  describe "term1" $ do
+    it "should be shown the intended text" $ do
+      let r = "\\L X.\\L Y.\\l f:(X) => (Y).\\l a:X.(f) (a)"
+      flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+        t <- term1
+        showTe t
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}