diff --git a/abt.cabal b/abt.cabal
--- a/abt.cabal
+++ b/abt.cabal
@@ -1,15 +1,13 @@
 name:                abt
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            Abstract binding trees for Haskell
 description:         A Haskell port of the Carnegie Mellon ABT library (SML), with some improvements.
 license:             MIT
 license-file:        LICENSE
 author:              Jonathan Sterling
 maintainer:          jon@jonmsterling.com
--- copyright:
 category:            Language
 build-type:          Simple
--- extra-source-files:
 cabal-version:       >=1.10
 
 library
@@ -20,14 +18,12 @@
                        Abt.Class.Abt,
                        Abt.Types,
                        Abt.Types.Nat,
-                       Abt.Types.HList,
                        Abt.Types.View,
                        Abt.Concrete.LocallyNameless
                        Abt.Tutorial
-  -- other-modules:
-  -- other-extensions:
   build-depends:       base >=4.7 && <4.8,
-                       transformers,
-                       mtl
+                       vinyl >=0.5,
+                       transformers
+  ghc-options:         -Wall
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/src/Abt/Class/Abt.hs b/src/Abt/Class/Abt.hs
--- a/src/Abt/Class/Abt.hs
+++ b/src/Abt/Class/Abt.hs
@@ -10,28 +10,29 @@
 ) where
 
 import Abt.Types.Nat
-import Abt.Types.HList
 import Abt.Types.View
 import Abt.Class.Monad
 import Abt.Class.Show1
 
-import Control.Applicative
+import Control.Applicative hiding (Const)
+import Data.Vinyl
+import Data.Vinyl.Functor
 import qualified Data.List as L
 
 -- | The 'Abt' signature represents mediation between an arbitrary (possibly
--- nameless) term representaion, and a first-order one (the 'View'). Based on
+-- nameless) term representaion, and a simple one (the 'View'). Based on
 -- the (effectful) ismorphism @'into' / 'out'@ between representations, many
 -- operations can be defined generically for arbitrary operator sets, including
 -- substitution and aggregation of free variables.
 --
-class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o, o → t where
+class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o where
   -- | Convert a 'View' into a term.
   --
   into
     ∷ View v o n t
     → t n
 
-  -- | Convert a term into a first-order 'View'.
+  -- | Convert a term into a simple 'View'.
   --
   out
     ∷ MonadVar v m
@@ -51,13 +52,13 @@
     ∷ v
     → t n
     → t (S n)
-  v \\ e = into $ (v :\ e)
+  v \\ e = into $ v :\ e
 
   -- | Construct an operator term.
   --
   ($$)
     ∷ o ns
-    → HList t ns
+    → Rec t ns
     → t Z
   o $$ es = into $ o :$ es
   infixl 1 $$
@@ -74,12 +75,8 @@
     oe' ← out e'
     case oe' of
       V v' → return $ if v == v' then e else e'
-      v' :\ e'' → do
-        e''' ← subst e v e''
-        return $ v' \\ e'''
-      o :$ es → do
-        es' ← htraverse (subst e v) es
-        return $ o $$ es'
+      v' :\ e'' → (v' \\) <$> subst e v e''
+      o :$ es → (o $$) <$> subst e v `rtraverse` es
 
   -- | Instantiate the bound variable of an abstraction.
   --
@@ -105,9 +102,9 @@
       v :\ e' → do
         L.delete v <$>
           freeVars e'
-      o :$ es → do
-        concat <$>
-          homogenizeA freeVars es
+      _ :$ es →
+        fmap concat . sequence . recordToList $
+          Const . freeVars <<$>> es
 
   -- | Render a term into a human-readable string.
   --
@@ -119,10 +116,10 @@
     vu ← out e
     case vu of
       V v → return $ show v
-      v :\ e → do
-        e' ← toString e
-        return $ show v ++ "." ++ e'
+      v :\ e' → do
+        estr ← toString e'
+        return $ show v ++ "." ++ estr
       o :$ es → do
-        es' ← homogenizeA toString es
+        es' ← sequence . recordToList $ Const . toString <<$>> es
         return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"
 
diff --git a/src/Abt/Class/HEq1.hs b/src/Abt/Class/HEq1.hs
--- a/src/Abt/Class/HEq1.hs
+++ b/src/Abt/Class/HEq1.hs
@@ -1,11 +1,19 @@
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE UnicodeSyntax #-}
 
 module Abt.Class.HEq1 where
 
+import Data.Vinyl
+
 -- | Uniform variant of 'Eq' for indexed types. This is different from
 -- 'Data.Functor.Eq1' in that it is properly kind polymorphic and crucially
 -- heterogeneous, and it places no constraint on the index.
 --
 class HEq1 f where
   (===) ∷ f i → f j → Bool
+
+instance HEq1 el ⇒ HEq1 (Rec el) where
+  RNil === RNil = True
+  (x :& xs) === (y :& ys) = x === y && xs === ys
+  _ === _ = False
diff --git a/src/Abt/Class/Show1.hs b/src/Abt/Class/Show1.hs
--- a/src/Abt/Class/Show1.hs
+++ b/src/Abt/Class/Show1.hs
@@ -8,7 +8,7 @@
 --
 class Show1 f where
   showsPrec1 ∷ Int → f i → ShowS
-  showsPrec1 i x = (show1 x ++)
+  showsPrec1 _ x = (show1 x ++)
 
   show1 ∷ f i → String
   show1 x = showsPrec1 0 x ""
diff --git a/src/Abt/Concrete/LocallyNameless.hs b/src/Abt/Concrete/LocallyNameless.hs
--- a/src/Abt/Concrete/LocallyNameless.hs
+++ b/src/Abt/Concrete/LocallyNameless.hs
@@ -8,13 +8,13 @@
 
 module Abt.Concrete.LocallyNameless
 ( Tm(..)
+, Tm0
 , Var(..)
 , varName
 , varIndex
 ) where
 
 import Abt.Types.Nat
-import Abt.Types.HList
 import Abt.Types.View
 import Abt.Class.HEq1
 import Abt.Class.Show1
@@ -22,6 +22,7 @@
 import Abt.Class.Monad
 
 import Control.Applicative
+import Data.Vinyl
 
 -- | A variable is a De Bruijn index, optionally decorated with a display name.
 data Var
@@ -70,14 +71,18 @@
   (\j' → Var n j')
     <$> i j
 
--- | Locally nameless terms with operators in @o@ at arity @n@.
+-- | Locally nameless terms with operators in @o@ at order @n@.
 --
 data Tm (o ∷ [Nat] → *) (n ∷ Nat) where
-  Free ∷ Var → Tm o Z
-  Bound ∷ Int → Tm o Z
+  Free ∷ Var → Tm0 o
+  Bound ∷ Int → Tm0 o
   Abs ∷ Tm o n → Tm o (S n)
-  App ∷ o ns → HList (Tm o) ns → Tm o Z
+  App ∷ o ns → Rec (Tm o) ns → Tm0 o
 
+-- | First order terms (i.e. terms not headed by abstractions).
+--
+type Tm0 o = Tm o Z
+
 instance HEq1 o ⇒ HEq1 (Tm o) where
   Free v1 === Free v2 = v1 == v2
   Bound m === Bound n = m == n
@@ -93,8 +98,8 @@
 shiftVar v n = \case
   Free v' → if v == v' then Bound n else Free v'
   Bound m → Bound m
-  Abs e → Abs (shiftVar v (n + 1) e)
-  App p es → App p $ hmap (shiftVar v n) es
+  Abs e → Abs $ shiftVar v (n + 1) e
+  App p es → App p $ rmap (shiftVar v n) es
 
 addVar
   ∷ Var
@@ -104,18 +109,18 @@
 addVar v n = \case
   Free v' → Free v'
   Bound m → if m == n then Free v else Bound m
-  Abs e → Abs (addVar v (n + 1) e)
-  App p es → App p $ hmap (addVar v n) es
+  Abs e → Abs $ addVar v (n + 1) e
+  App p es → App p $ rmap (addVar v n) es
 
 instance Show1 o ⇒ Abt Var o (Tm o) where
   into = \case
     V v → Free v
-    v :\ e → Abs (shiftVar v 0 e)
+    v :\ e → Abs $ shiftVar v 0 e
     v :$ es → App v es
 
   out = \case
     Free v → return $ V v
-    Bound n → fail "bound variable occured in out"
+    Bound _ → fail "bound variable occured in out"
     Abs e → do
       v ← fresh
       return $ v :\ addVar v 0 e
diff --git a/src/Abt/Tutorial.hs b/src/Abt/Tutorial.hs
--- a/src/Abt/Tutorial.hs
+++ b/src/Abt/Tutorial.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE LambdaCase #-}
@@ -13,8 +14,9 @@
 import Abt.Concrete.LocallyNameless
 
 import Control.Applicative
-import Control.Monad.Trans
 import Control.Monad.Trans.State.Strict
+import Control.Monad.Trans.Maybe
+import Data.Vinyl
 
 -- | We'll start off with a monad in which to manipulate ABTs; we'll need some
 -- state for fresh variable generation.
@@ -59,14 +61,77 @@
   Ap === Ap = True
   _ === _ = False
 
--- | Check out the source to see this example term: note that number of
--- arguments and presence of abstractions is guaranteed by the types.  The
--- representation is not scope-safe (i.e. free variables are permitted), but
--- that's how we want it.
+-- | A monad transformer for small step operational semantics.
 --
-example ∷ M [Var]
-example = do
+newtype StepT m α
+  = StepT
+  { runStepT ∷ MaybeT m α
+  } deriving (Monad, Functor, Applicative, Alternative)
+
+-- | To indicate that a term is in normal form.
+--
+stepsExhausted
+  ∷ Applicative m
+  ⇒ StepT m α
+stepsExhausted = StepT . MaybeT $ pure Nothing
+
+instance MonadVar Var m ⇒ MonadVar Var (StepT m) where
+  fresh = StepT . MaybeT $ Just <$> fresh
+  named str = StepT . MaybeT $ Just <$> named str
+
+-- | A single evaluation step.
+--
+step
+  ∷ Tm0 Lang
+  → StepT M (Tm0 Lang)
+step tm =
+  out tm >>= \case
+    Ap :$ m :& n :& RNil →
+      out m >>= \case
+        Lam :$ xe :& RNil → xe // n
+        _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n
+          where
+            app a b = Ap $$ a :& b :& RNil
+    _ → stepsExhausted
+
+-- | The reflexive-transitive closure of a small-step operational semantics.
+--
+star
+  ∷ Monad m
+  ⇒ (α → StepT m α)
+  → (α → m α)
+star f a =
+  runMaybeT (runStepT $ f a) >>=
+    return a `maybe` star f
+
+-- | Evaluate a term to normal form
+--
+eval ∷ Tm0 Lang → Tm0 Lang
+eval = runM . star step
+
+-- | @λx.x@
+--
+identityTm ∷ M (Tm0 Lang)
+identityTm = do
   x ← fresh
-  y ← fresh
-  let tm = Lam $$ x \\ (Ap $$ var x :* var y :* Nil) :* Nil
-  freeVars tm
+  return $ Lam $$ (x \\ var x) :& RNil
+
+-- | @(λx.x)(λx.x)@
+--
+appTm ∷ M (Tm0 Lang)
+appTm = do
+  tm ← identityTm
+  return $ Ap $$ tm :& tm :& RNil
+
+-- | A demonstration of evaluating (and pretty-printing). Output:
+--
+-- @
+-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@2.\@2]
+-- @
+--
+main ∷ IO ()
+main = do
+  let mm = runM $ appTm >>= toString
+      mm' = runM $ appTm >>= toString . eval
+  print $ mm ++ " ~>* " ++ mm'
+
diff --git a/src/Abt/Types.hs b/src/Abt/Types.hs
--- a/src/Abt/Types.hs
+++ b/src/Abt/Types.hs
@@ -2,10 +2,8 @@
 --
 module Abt.Types
 ( module Abt.Types.Nat
-, module Abt.Types.HList
 , module Abt.Types.View
 ) where
 
 import Abt.Types.Nat
-import Abt.Types.HList
 import Abt.Types.View
diff --git a/src/Abt/Types/HList.hs b/src/Abt/Types/HList.hs
deleted file mode 100644
--- a/src/Abt/Types/HList.hs
+++ /dev/null
@@ -1,43 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UnicodeSyntax #-}
-
-module Abt.Types.HList
-( HList(..)
-, hmap
-, htraverse
-, homogenizeA
-) where
-
-import Control.Applicative
-import Abt.Class.HEq1
-
-data HList ∷ (κ → *) → [κ] → * where
-  Nil ∷ HList el '[]
-  (:*) ∷ el x → HList el xs → HList el (x ': xs)
-infixr 8 :*
-
-hmap ∷ (∀ x. f x → g x) → HList f xs → HList g xs
-hmap η = \case
-  Nil → Nil
-  x :* xs → η x :* hmap η xs
-
-htraverse ∷ Applicative h ⇒ (∀ x. f x → h (g x)) → HList f xs → h (HList g xs)
-htraverse η = \case
-  Nil → pure Nil
-  x :* xs → (:*) <$> η x <*> htraverse η xs
-
-homogenizeA ∷ Applicative h ⇒ (∀ x. el x → h α) → HList el xs → h [α]
-homogenizeA η = \case
-  Nil → pure []
-  x :* xs → (:) <$> η x <*> homogenizeA η xs
-
-instance HEq1 el ⇒ HEq1 (HList el) where
-  Nil === Nil = True
-  (x :* xs) === (y :* ys) = x === y && xs === ys
-  _ === _ = False
-
diff --git a/src/Abt/Types/View.hs b/src/Abt/Types/View.hs
--- a/src/Abt/Types/View.hs
+++ b/src/Abt/Types/View.hs
@@ -7,29 +7,36 @@
 
 module Abt.Types.View
 ( View(..)
+, View0
 , mapView
 ) where
 
 import Abt.Types.Nat
-import Abt.Types.HList
+import Data.Vinyl
 
 -- | @v@ is the type of variables; @o@ is the type of operators parameterized
--- by arities; @n@ is the "higher type" of the term (i.e. a term has @n=0@, a
--- single binding has @n=1@, etc.); @φ@ is the functor which interprets the
--- inner structure of the view.
+-- by arities; @n@ is the "higher type"/order of the term (i.e. a term has
+-- @n=0@, a single binding has @n=1@, etc.); @φ@ is the functor which
+-- interprets the inner structure of the view.
 --
 data View (v ∷ *) (o ∷ [Nat] → *) (n ∷ Nat) (φ ∷ Nat → *) where
-  V ∷ v → View v o Z φ
+  V ∷ v → View0 v o φ
   (:\) ∷ v → φ n → View v o (S n) φ
-  (:$) ∷ o ns → HList φ ns → View v o Z φ
+  (:$) ∷ o ns → Rec φ ns → View0 v o φ
 
+infixl 2 :$
+
+-- | First order term views.
+--
+type View0 v o φ = View v o Z φ
+
 -- | Views are a (higher) functor.
 --
 mapView
   ∷ (∀ j. φ j → ψ j) -- ^ a natural transformation @φ → ψ@
   → View v o n φ -- ^ a view at @φ@
   → View v o n ψ
-mapView eta = \case
+mapView η = \case
   V v → V v
-  v :\ e → v :\ eta e
-  o :$ es → o :$ hmap eta es
+  v :\ e → v :\ η e
+  o :$ es → o :$ rmap η es