diff --git a/app/Main.hs b/app/Main.hs
index b4a077f..5405f64 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -3,7 +3,7 @@ module Main where
 import Control.Monad (forever)
 import System.IO (hFlush, stdout)
 import Text.Parsec (parse)
-import UntypedLambdaCalculus (eval, canonym)
+import UntypedLambdaCalculus (eval)
 import UntypedLambdaCalculus.Parser (expr)
 
 prompt :: String -> IO String
@@ -14,7 +14,7 @@ prompt text = do
 
 main :: IO ()
 main = forever $ do
-  expr <- parse expr "stdin" <$> prompt ">> "
-  case expr of
+  input <- expr "stdin" <$> prompt ">> "
+  case input of
     Left parseError -> putStrLn $ "Parse error: " ++ show parseError
-    Right expr -> print $ eval $ canonym expr
+    Right ast -> print $ eval ast
diff --git a/package.yaml b/package.yaml
index a129ff0..f3737e3 100644
--- a/package.yaml
+++ b/package.yaml
@@ -18,6 +18,7 @@ dependencies:
 - parsec >= 3.1 && < 4
 - recursion-schemes >= 5.1 && < 6
 - unordered-containers >= 0.2.10 && < 0.3
+- transformers >= 0.5.6 && < 0.6
 
 library:
   source-dirs: src
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
index 4ba2371..6229f28 100644
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses #-}
-module Data.Fin (Fin (Zero, Succ), finUp, toInt, pred, finRemove) where
+{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-}
+module Data.Fin (Fin (Zero, Succ), toInt, pred, finRemove) where
 
 import Data.Functor.Foldable (Base, Recursive, project, cata)
 import Data.Injection (Injection, inject)
@@ -14,17 +14,13 @@ data Fin n where
 
 type instance Base (Fin n) = Maybe
 
-instance (Nat n, Nat m, GTorEQ m n) => Injection (Fin n) (Fin m) where
-  inject = unsafeCoerce
-  
--- | Coerce a `Fin n` into a `Fin (Succ n)`.
-finUp :: Nat n => Fin n -> Fin (Succ n)
-finUp Zero = Zero
-finUp (Succ n) = Succ (finUp n)
+instance (Nat n) => Injection (Fin n) (Fin (Succ n)) where
+  inject Zero = Zero
+  inject (Succ n) = Succ (inject n)
 
 instance (Nat n) => Recursive (Fin n) where
   project Zero     = Nothing
-  project (Succ n) = Just $ finUp n
+  project (Succ n) = Just $ inject n
 
 instance (Nat n) => Eq (Fin n) where
   Zero == Zero = True
diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index 6f35cc7..12c209c 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -1,23 +1,27 @@
 {-# LANGUAGE GADTs, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}
-module Data.Vec (Vec (Empty, (:.)), (!.), elemIndexVec, vmap) where
+module Data.Vec (Vec (Empty, (:.)), (!.), elemIndexVec) where
 
 import Data.Fin (Fin (Zero, Succ))
 import Data.Type.Nat (Nat, Zero, Succ)
 
-data Vec a n where
-  Empty :: Vec a Zero
-  (:.)  :: Nat n => a -> Vec a n -> Vec a (Succ n)
+data Vec n a where
+  Empty :: Vec Zero a
+  (:.)  :: Nat n => a -> Vec n a -> Vec (Succ n) a
 
--- | Equivalent to fmap. It is impossible to implement Functor on Vec for stupid reasons.
-vmap :: (a -> b) -> Vec a n -> Vec b n
-vmap _ Empty     = Empty
-vmap f (x :. xs) = f x :. vmap f xs
+instance Nat n => Functor (Vec n) where
+  fmap _ Empty     = Empty
+  fmap f (x :. xs) = f x :. fmap f xs
 
-(!.) :: Nat n => Vec a n -> Fin n -> a
-(!.) (x :. _ ) Zero     = x
-(!.) (_ :. xs) (Succ n) = xs !. n
+instance Nat n => Foldable (Vec n) where
+  foldr _ base Empty     = base
+  foldr f base (x :. xs) = x `f` foldr f base xs
 
-elemIndexVec :: (Eq a, Nat n) => a -> Vec a n -> Maybe (Fin n)
+(!.) :: Nat n => Vec n a -> Fin n -> a
+(x :. _ ) !. Zero     = x
+(_ :. xs) !. (Succ n) = xs !. n
+_         !. _        = error "Impossible"
+
+elemIndexVec :: (Eq a, Nat n) => a -> Vec n a -> Maybe (Fin n)
 elemIndexVec _ Empty = Nothing
 elemIndexVec x (x' :. xs)
   | x == x'   = Just Zero
diff --git a/src/UntypedLambdaCalculus.hs b/src/UntypedLambdaCalculus.hs
index f218817..0e27883 100644
--- a/src/UntypedLambdaCalculus.hs
+++ b/src/UntypedLambdaCalculus.hs
@@ -1,19 +1,11 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
-module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), canonym, eval, normal, whnf) where
+{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, MultiParamTypeClasses #-}
+module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), eval) where
 
-import Control.Applicative (liftA2)
-import Control.Monad.Reader (Reader, runReader, ask, local, withReader, reader, asks)
-import Data.Fin (Fin (Zero, Succ), finUp, finRemove)
-import Data.Function (fix)
-import Data.Functor.Foldable (Base, Recursive, Corecursive, ListF (Nil, Cons), cata, embed, project)
-import Data.Functor.Foldable.TH (makeBaseFunctor)
-import Data.Injection (inject)
-import Data.Maybe (fromJust)
+import Control.Monad.Reader (Reader, runReader, withReader, reader, asks)
+import Data.Fin (Fin (Zero, Succ), finRemove)
+import Data.Injection (Injection, inject)
 import Data.Type.Nat (Nat, Succ, Zero)
-import Data.Vec (Vec (Empty, (:.)), (!.), vmap, elemIndexVec)
-import UntypedLambdaCalculus.Parser (Ast (AstVar, AstLam, AstApp))
-
-type Algebra f a = f a -> a
+import Data.Vec (Vec (Empty, (:.)), (!.))
 
 -- | A lambda calculus expression where variables are identified
 -- | by their distance from their binding site (De Bruijn indices).
@@ -22,17 +14,15 @@ data Expr n = Free String
             | Lam String (Expr (Succ n))
             | App (Expr n) (Expr n)
 
-makeBaseFunctor ''Expr
-
-exprUp :: Nat n => Expr n -> Expr (Succ n)
-exprUp (Free v) = Free v
-exprUp (Var v) = Var $ finUp v
-exprUp (Lam v e) = Lam v $ exprUp e
-exprUp (App f x) = App (exprUp f) (exprUp x)
+instance (Nat n) => Injection (Expr n) (Expr (Succ n)) where
+  inject (Free v)  = Free v
+  inject (Var v)   = Var $ inject v
+  inject (Lam v e) = Lam v $ inject e
+  inject (App f x) = App (inject f) (inject x)
 
 instance Show (Expr Zero) where
-  show x = runReader (alg x) Empty
-    where alg :: Nat n => Expr n -> Reader (Vec String n) String
+  show expr = runReader (alg expr) Empty
+    where alg :: Nat n => Expr n -> Reader (Vec n String) String
           alg (Free v)   = return v
           alg (Var  v)   = reader (\vars -> vars !. v ++ ':' : show v)
           alg (Lam  v e) = do
@@ -46,68 +36,40 @@ instance Show (Expr Zero) where
 -- | Determine whether the variable bound by a lambda expression is used in its body.
 -- | This is used in eta reduction, where `(\x. f x)` reduces to `f` when `x` is not bound in `f`.
 unbound :: Nat n => Expr (Succ n) -> Bool
-unbound x = runReader (alg x) Zero
+unbound expr = runReader (alg expr) Zero
   where alg :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) Bool
         alg (Free _)  = return True
         alg (Var v)   = reader (/= v)
         alg (App f x) = (&&) <$> alg f <*> alg x
         alg (Lam _ e) = withReader Succ $ alg e
 
--- | Convert an Ast into an Expression where all variables have canonical, unique names.
--- | Namely, bound variables are identified according to their distance from their binding site
--- | (i.e. De Bruijn indices).
-canonym :: Ast -> Expr Zero
-canonym x = runReader (alg x) Empty
-  where alg :: Nat n => Ast -> Reader (Vec String n) (Expr n)
-        alg (AstVar v)   = maybe (Free v) Var <$> elemIndexVec v <$> ask
-        alg (AstLam v e) = Lam v <$> withReader (v :.) (alg e)
-        alg (AstApp n m) = App <$> alg n <*> alg m
-
 -- | When we bind a new variable, we enter a new scope.
 -- | Since variables are identified by their distance from their binder,
--- | we must increment them to account for the incremented distance.
-introduceBindingInExpr :: Nat n => Expr n -> Expr (Succ n)
-introduceBindingInExpr (Var v) = Var $ Succ v
-introduceBindingInExpr o@(Lam _ _) = exprUp o
-introduceBindingInExpr (Free x) = Free x
-introduceBindingInExpr (App f x) = App (introduceBindingInExpr f) (introduceBindingInExpr x)
-
-intoEta :: Nat n => Expr (Succ n) -> Expr n
-intoEta x = runReader (intoEta' x) Zero
-  where intoEta' :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n)
-        intoEta' (Free x) = return $ Free x
-        intoEta' (Var x) = Var <$> fromJust <$> asks (finRemove x)
-        intoEta' (App f x) = App <$> intoEta' f <*> intoEta' x
-        intoEta' (Lam v e) = Lam v <$> withReader Succ (intoEta' e)
+-- | we must increment them to account for the incremented distance,
+-- | thus embedding them into the new expression.
+embed' :: Nat n => Expr n -> Expr (Succ n)
+embed' (Var v) = Var $ Succ v
+embed' o@(Lam _ _) = inject o
+embed' (Free x) = Free x
+embed' (App f x) = App (embed' f) (embed' x)
 
 subst :: Nat n => Expr n -> Expr (Succ n) -> Expr n
-subst val x = runReader (subst' val x) Zero
+subst value expr = runReader (subst' value expr) Zero
   where subst' :: Nat n => Expr n -> Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n)
         subst' _   (Free x)  = return $ Free x
         subst' val (Var x)   = maybe val Var <$> asks (finRemove x)
         subst' val (App f x) = App <$> subst' val f <*> subst' val x
-        subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (introduceBindingInExpr val) e)
+        subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (embed' val) e)
 
--- | Evaluate a variable to normal form.
+-- | Evaluate an expression to normal form.
 eval :: Nat n => Expr n -> Expr n
 eval (App f' x) = case eval f' of
+  -- Beta reduction.
   Lam _ e -> eval $ subst x e
   f -> App f (eval x)
 eval o@(Lam _ (App f (Var Zero)))
-  | unbound f = eval $ intoEta f
+  -- Eta reduction. We know that `0` is not bound in `f`,
+  -- so we can simply substitute it for undefined.
+  | unbound f = eval $ subst undefined f
   | otherwise = o
 eval o = o
-
--- | Is an expression in normal form?
-normal :: Nat n => Expr n -> Bool
-normal (App (Lam _ _) _) = False
-normal (Lam _ (App f (Var Zero))) = unbound f
-normal (App f x) = normal f && normal x
-normal _ = True
-
--- | Is an expression in weak head normal form?
-whnf :: Nat n => Expr n -> Bool
-whnf (App (Lam _ _) _) = False
-whnf (Lam _ (App f (Var Zero))) = unbound f
-whnf (App f _) = whnf f
-whnf _ = True
diff --git a/src/UntypedLambdaCalculus/Parser.hs b/src/UntypedLambdaCalculus/Parser.hs
index 6fdb370..9b2aa60 100644
--- a/src/UntypedLambdaCalculus/Parser.hs
+++ b/src/UntypedLambdaCalculus/Parser.hs
@@ -1,82 +1,71 @@
 {-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
-module UntypedLambdaCalculus.Parser ( Ast (AstVar, AstLam, AstApp)
-                                    , AstF (AstVarF, AstLamF, AstAppF)
-                                    , expr
-                                    ) where
+module UntypedLambdaCalculus.Parser (expr) where
 
-import Data.Functor.Foldable (cata)
-import Data.Functor.Foldable.TH (makeBaseFunctor,)
+import Control.Applicative (liftA)
+import Control.Monad.Reader (ReaderT, runReaderT, withReaderT, mapReaderT, ask)
+import Control.Monad.Trans.Class (lift)
+import Data.Functor (void)
 import Data.List (foldl1')
-import Text.Parsec
-import Text.Parsec.String
+import Data.Type.Nat (Nat, Zero )
+import Data.Vec (Vec (Empty, (:.)), elemIndexVec)
+import Text.Parsec hiding (Empty)
+import Unsafe.Coerce (unsafeCoerce)
+import UntypedLambdaCalculus (Expr (Free, Var, Lam, App))
 
--- | The abstract syntax tree of lambda calculus.
-data Ast = AstVar String
-         | AstLam String Ast
-         | AstApp Ast Ast
-         | AstLet String Ast Ast
-
-makeBaseFunctor ''Ast
-
-instance Show Ast where
-  show = cata alg
-    where alg (AstVarF v)   = v
-          alg (AstLamF v e) = "(\\" ++ v ++ ". " ++ e ++ ")"
-          alg (AstAppF f x) = "(" ++ f ++ " " ++ x ++ ")"
-
-somespaces :: Parser ()
-somespaces = skipMany1 space
+type Parser s a = ReaderT s (Parsec String ()) a
 
 -- | A variable name.
-name :: Parser String
+name :: Parsec String () String
 name = do
   c <- letter
   cs <- many alphaNum
   return $ c : cs
 
 -- | A variable expression.
-var :: Parser Ast
-var = AstVar <$> name
+var :: Nat n => Parser (Vec n String) (Expr n)
+var = do
+  varn <- lift name
+  bound <- ask
+  return $ maybe (Free varn) Var $ elemIndexVec varn bound
 
 -- | Run parser between parentheses.
-parens :: Parser a -> Parser a
-parens = between (char '(') (char ')')
-
-let_ :: Parser Ast
-let_ = do
-  string ".let"
-  somespaces
-  v <- name
-  somespaces
-  char '='
-  somespaces
-  x <- safeExpr
-  somespaces
-  string ".in"
-  e <- expr
-  return $ AstApp (AstLam v e) x
+parens :: Parsec String () a -> Parsec String () a
+parens p = do
+  _ <- char '('
+  x <- p
+  _ <- char ')'
+  return x
 
 -- | A lambda expression.
-lam :: Parser Ast
+lam :: Nat n => Parser (Vec n String) (Expr n)
 lam = do
-  char '\\'
-  vars <- name `sepBy1` spaces
-  char '.'
-  spaces
-  body <- expr
-  return $ foldr AstLam body vars
+  vars <- lift $ do
+    _ <- char '\\'
+    vars <- name `sepBy1` spaces
+    _ <- char '.'
+    spaces
+    return vars
+  help vars
+  where help :: Nat n => [String] -> Parser (Vec n String) (Expr n)
+        help []     = app
+        help (v:vs) = Lam v <$> withReaderT (v :.) (help vs)
 
 -- | An application expression.
-app :: Parser Ast
-app = foldl1' AstApp <$> sepBy1 safeExpr spaces
+app :: Nat n => Parser (Vec n String) (Expr n)
+app = foldl1' App <$> mapReaderT (`sepBy1` spaces) safeExpr
+
+ll :: (Parsec String () a -> Parsec String () b -> Parsec String () c) -> Parser s a -> Parser s b -> Parser s c
+ll f p1 p2 = do
+  bound <- ask
+  lift $ f (runReaderT p1 bound) (runReaderT p2 bound)
 
 -- | An expression, but where applications must be surrounded by parentheses,
 -- | to avoid ambiguity (infinite recursion on `app` in the case where the first
 -- | expression in the application is also an `app`, consuming no input).
-safeExpr :: Parser Ast
-safeExpr = var <|> lam <|> parens (lam <|> app)
+safeExpr :: Nat n => Parser (Vec n String) (Expr n)
+safeExpr = ll (<|>) var $ ll (<|>) lam $ mapReaderT parens (ll (<|>) lam app)
 
 -- | Since applications do not require parentheses and can contain only a single item,
 -- | the `app` parser is sufficient to parse any expression at all.
-expr :: Parser Ast
-expr = app
+expr :: SourceName -> String -> Either ParseError (Expr Zero)
+expr sourceName code = parse (runReaderT app Empty) sourceName code