From 25658f370aaa7506edcf7adc17912a865af8ee51 Mon Sep 17 00:00:00 2001
From: James Martin <james@jtmar.me>
Date: Wed, 11 Dec 2019 18:29:28 -0800
Subject: [PATCH] Complexity was getting out of hand. Beginning a rewrite.
 Added tests.

---
 .gitignore                                    |   4 +-
 app/Main.hs                                   |  12 +-
 jtm-lambda-calculus.cabal                     |  70 -------
 package.yaml                                  |  43 ++---
 src/Data/Type/Nat.hs                          |  54 ------
 src/Data/Vec.hs                               |   8 -
 src/LambdaCalculus/Combinators.hs             |   8 -
 src/LambdaCalculus/Evaluation/Optimal.hs      | 175 ------------------
 src/LambdaCalculus/Expression.hs              | 137 ++++++++++++++
 src/LambdaCalculus/Parser.hs                  |  90 +++------
 src/LambdaCalculus/Representation.hs          |  30 ---
 .../Representation/AbstractSyntax.hs          |  76 --------
 .../Dependent/ReverseDeBruijn.hs              |  74 --------
 src/LambdaCalculus/Representation/Standard.hs |  18 --
 stack.yaml                                    |  65 +------
 stack.yaml.lock                               |   8 +-
 test/Spec.hs                                  |  58 ++++++
 17 files changed, 249 insertions(+), 681 deletions(-)
 delete mode 100644 jtm-lambda-calculus.cabal
 delete mode 100644 src/Data/Type/Nat.hs
 delete mode 100644 src/Data/Vec.hs
 delete mode 100644 src/LambdaCalculus/Combinators.hs
 delete mode 100644 src/LambdaCalculus/Evaluation/Optimal.hs
 create mode 100644 src/LambdaCalculus/Expression.hs
 delete mode 100644 src/LambdaCalculus/Representation.hs
 delete mode 100644 src/LambdaCalculus/Representation/AbstractSyntax.hs
 delete mode 100644 src/LambdaCalculus/Representation/Dependent/ReverseDeBruijn.hs
 delete mode 100644 src/LambdaCalculus/Representation/Standard.hs
 create mode 100644 test/Spec.hs

diff --git a/.gitignore b/.gitignore
index 14f516a..f8da417 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,3 @@
 .stack-work/
-untyped-lambda-calculus.cabal
-*~
\ No newline at end of file
+*.cabal
+*~
diff --git a/app/Main.hs b/app/Main.hs
index 33e976f..a1cf093 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,12 +1,10 @@
+{-# LANGUAGE LambdaCase #-}
 module Main where
 
 import Control.Monad (forever)
-import Data.Type.Nat (Nat (Z))
+import LambdaCalculus.Expression (lazyEval)
+import LambdaCalculus.Parser (parseExpression)
 import System.IO (hFlush, stdout)
-import LambdaCalculus.Evaluation.Optimal (eval)
-import LambdaCalculus.Parser (parse)
-import LambdaCalculus.Representation (convert)
-import LambdaCalculus.Representation.Dependent.ReverseDeBruijn (Expression)
 
 prompt :: String -> IO String
 prompt text = do
@@ -15,6 +13,6 @@ prompt text = do
   getLine
 
 main :: IO ()
-main = forever $ parse "stdin" <$> prompt ">> " >>= \case
+main = forever $ parseExpression <$> prompt ">> " >>= \case
   Left parseError -> putStrLn $ "Parse error: " ++ show parseError
-  Right expr -> do print expr; print $ eval (convert expr :: Expression 'Z)
+  Right expr -> print $ lazyEval expr
diff --git a/jtm-lambda-calculus.cabal b/jtm-lambda-calculus.cabal
deleted file mode 100644
index 6a2cf89..0000000
--- a/jtm-lambda-calculus.cabal
+++ /dev/null
@@ -1,70 +0,0 @@
-cabal-version: 1.12
-
--- This file has been generated from package.yaml by hpack version 0.31.2.
---
--- see: https://github.com/sol/hpack
---
--- hash: 26600940e6acf0bd4e6fbb02d188b88fd368836effa5ea0427f7a4d5cd792669
-
-name:           jtm-lambda-calculus
-version:        0.1.0.0
-synopsis:       Implementations of various Lambda Calculus evaluators and type systems.
-description:    Please see the README on GitHub at <https://github.com/jamestmartin/lambda-calculus#readme>
-category:       LambdaCalculus
-homepage:       https://github.com/jamestmartin/lambda-calculus#readme
-bug-reports:    https://github.com/jamestmartin/lambda-calculus/issues
-author:         James Martin
-maintainer:     james@jtmar.me
-copyright:      2019 James Martin
-license:        GPL-3
-license-file:   LICENSE
-build-type:     Simple
-extra-source-files:
-    README.md
-
-source-repository head
-  type: git
-  location: https://github.com/jamestmartin/lambda-calculus
-
-library
-  exposed-modules:
-      Data.Type.Nat
-      Data.Vec
-      LambdaCalculus.Combinators
-      LambdaCalculus.Evaluation.Optimal
-      LambdaCalculus.Parser
-      LambdaCalculus.Representation
-      LambdaCalculus.Representation.AbstractSyntax
-      LambdaCalculus.Representation.Dependent.ReverseDeBruijn
-      LambdaCalculus.Representation.Standard
-  other-modules:
-      Paths_jtm_lambda_calculus
-  hs-source-dirs:
-      src
-  default-extensions: BlockArguments DataKinds DeriveFoldable DeriveFunctor DeriveTraversable FlexibleInstances FunctionalDependencies GADTs KindSignatures LambdaCase MultiParamTypeClasses PolyKinds Rank2Types TemplateHaskell TypeFamilies TypeOperators
-  build-depends:
-      base >=4.7 && <5
-    , free >=5.1 && <6
-    , mtl >=2.2 && <3
-    , parsec >=3.1 && <4
-    , recursion-schemes >=5.1 && <6
-    , unordered-containers >=0.2.10 && <0.3
-  default-language: Haskell2010
-
-executable jtm-lambda-calculus-exe
-  main-is: Main.hs
-  other-modules:
-      Paths_jtm_lambda_calculus
-  hs-source-dirs:
-      app
-  default-extensions: BlockArguments DataKinds DeriveFoldable DeriveFunctor DeriveTraversable FlexibleInstances FunctionalDependencies GADTs KindSignatures LambdaCase MultiParamTypeClasses PolyKinds Rank2Types TemplateHaskell TypeFamilies TypeOperators
-  ghc-options: -threaded -rtsopts -with-rtsopts=-N
-  build-depends:
-      base >=4.7 && <5
-    , free >=5.1 && <6
-    , jtm-lambda-calculus
-    , mtl >=2.2 && <3
-    , parsec >=3.1 && <4
-    , recursion-schemes >=5.1 && <6
-    , unordered-containers >=0.2.10 && <0.3
-  default-language: Haskell2010
diff --git a/package.yaml b/package.yaml
index 3653672..8ca770c 100644
--- a/package.yaml
+++ b/package.yaml
@@ -12,39 +12,16 @@ description:         Please see the README on GitHub at <https://github.com/jame
 extra-source-files:
 - README.md
 
-default-extensions:
-- BlockArguments
-- DataKinds
-- DeriveFoldable
-- DeriveFunctor
-- DeriveTraversable
-- FlexibleInstances
-- FunctionalDependencies
-- GADTs
-- KindSignatures
-- LambdaCase
-- MultiParamTypeClasses
-- PolyKinds
-- Rank2Types
-- TemplateHaskell
-- TypeFamilies
-- TypeOperators
-
 dependencies:
-- base >= 4.7 && < 5
-# used for `recursion-schemes` histomorphisms
-- free >= 5.1 && < 6
-- mtl >= 2.2 && < 3
+- base >= 4.12 && < 5
 - parsec >= 3.1 && < 4
-- recursion-schemes >= 5.1 && < 6
-# HashSet used to hold the set of free variables
 - unordered-containers >= 0.2.10 && < 0.3
 
 library:
   source-dirs: src
 
 executables:
-  jtm-lambda-calculus-exe:
+  jtm-lambda-calculus:
     main:                Main.hs
     source-dirs:         app
     ghc-options:
@@ -53,3 +30,19 @@ executables:
     - -with-rtsopts=-N
     dependencies:
     - jtm-lambda-calculus
+
+tests:
+  jtm-lambda-calculus-test:
+    main: Spec.hs
+    source-dirs: test
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - jtm-lambda-calculus
+    - generic-random >= 1.2 && < 2
+    - QuickCheck >= 2.13 && < 3
+    - tasty >= 1.2 && < 2
+    - tasty-hunit >= 0.10 && < 0.11
+    - tasty-quickcheck >= 0.10.1 && < 0.11
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
deleted file mode 100644
index ee7aed3..0000000
--- a/src/Data/Type/Nat.hs
+++ /dev/null
@@ -1,54 +0,0 @@
--- | I would rather depend on the `fin` package than export my own Nat type,
--- but I couldn't figure out how to write substitution with their definition of SNat,
--- because it uses `SNatI n =>` instead of `SNat n ->` in the recursive case,
--- and `withSNat` and `snat` were both providing ambigous type variables and all that.
--- If anyone could fix it for me, I would gladly accept a PR.
-module Data.Type.Nat where
-
-import Data.Type.Equality ((:~:)(Refl))
-import Numeric.Natural (Natural)
-
-data Nat = Z | S Nat
-
-instance Show Nat where
-  show = show . natToNatural
-
-data SNat :: Nat -> * where
-  SZ :: SNat 'Z
-  SS :: SNat n -> SNat ('S n)
-
-instance Show (SNat n) where
-  show = show . snatToNatural
-
-type family Plus (n :: Nat) (m :: Nat) = (sum :: Nat) where
-  Plus Z      m = m
-  Plus ('S n) m = 'S (Plus n m)
-
-class               SNatI (n :: Nat) where snat :: SNat n
-instance            SNatI 'Z         where snat = SZ
-instance SNatI n => SNatI ('S n)     where snat = SS snat
-
-natToNatural :: Nat -> Natural
-natToNatural Z     = 0
-natToNatural (S n) = 1 + natToNatural n
-
-snatToNat :: forall n. SNat n -> Nat
-snatToNat SZ     = Z
-snatToNat (SS n) = S $ snatToNat n
-
-snatToNatural :: forall n. SNat n -> Natural
-snatToNatural = natToNatural . snatToNat
-
-plusZero :: SNat n -> Plus n 'Z :~: n
--- trivial: Z + n = n by definition of equality,
--- and in this case n = Z and thus Z + Z = Z.
-plusZero SZ     = Refl
--- if n + Z = n, then S n + Z = S n.
-plusZero (SS n) = case plusZero n of Refl -> Refl
-
-plusSuc :: SNat n -> SNat m -> Plus n ('S m) :~: 'S (Plus n m)
--- trivial: Z + n = n by definition of equality,
--- and in this case n = S m, and thus Z + S m = S m.
-plusSuc SZ     _ = Refl
--- if n + S m = S (n + m), then S n + S m = S (S n + m).
-plusSuc (SS n) m = case plusSuc n m of Refl -> Refl
diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
deleted file mode 100644
index 64f5a1d..0000000
--- a/src/Data/Vec.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-module Data.Vec where
-
-import Data.Type.Nat
-
--- | See the documentation of 'Data.Type.Nat' to see why I don't just depend on the `vec` package.
-data Vec :: Nat -> * -> * where
-  VNil  :: Vec 'Z a
-  (:::) :: a -> Vec n a -> Vec ('S n) a
diff --git a/src/LambdaCalculus/Combinators.hs b/src/LambdaCalculus/Combinators.hs
deleted file mode 100644
index a3531b1..0000000
--- a/src/LambdaCalculus/Combinators.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-module LambdaCalculus.Combinators where
-
-import LambdaCalculus.Representation (IsExpr, fromStandard)
-import LambdaCalculus.Representation.Standard
-
--- | The `I` combinator, representing the identify function `λx. x`.
-i :: IsExpr expr => expr
-i = fromStandard $ Abstraction "x" $ Variable "x"
diff --git a/src/LambdaCalculus/Evaluation/Optimal.hs b/src/LambdaCalculus/Evaluation/Optimal.hs
deleted file mode 100644
index 2a2b7d5..0000000
--- a/src/LambdaCalculus/Evaluation/Optimal.hs
+++ /dev/null
@@ -1,175 +0,0 @@
--- | !!!IMPORTANT!!!
--- This module is a WORK IN PROGRESS.
--- It DOES NOT YET IMPLEMENT OPTIMAL EVALUATION.
--- It currently implements *lazy* evaluation with the reverse de bruijn syntax,
--- and my end goal is to make it support optimal evaluation,
--- but currently it is not even close.
-module LambdaCalculus.Evaluation.Optimal where
-
-import Control.Applicative ((<|>))
-import Data.Type.Nat
-import LambdaCalculus.Representation.Dependent.ReverseDeBruijn
-
--- | The meaning of expressions is defined by how they can be reduced.
--- There are three kinds of reduction: beta-reduction ('betaReduce'),
--- which defines how applications interact with lambda abstractions;
--- eta-reduction ('etaReduce'), which describes how lambda abstractions interact with applications;
--- and a new form, which I call scope-reduction ('scopeReduce'),
--- which describes how 'Drop' scope delimiters propogate through expressions.
---
--- This function takes an expression and either reduces it,
--- or, if there is no applicable reduction rule, returns nothing.
--- The lack of an applicable reduction rule does not necessarily mean
--- that an expression is irreducible: see 'evaluate' for more information.
-reduce :: Expression n -> Maybe (Expression n)
--- Note: there are no expressions which are reducible in multiple ways.
--- Only one of these cases can apply at once.
-reduce expr = scopeReduce expr <|> substitute expr <|> betaReduce expr <|> etaReduce expr
-
--- | A subexpression to which a reduction step may be applied is called a "redex",
--- short for "reducible expression".
-isRedex :: Expression n -> Bool
-isRedex expr = isScopeRedex expr || isBetaRedex expr || isEtaRedex expr
-
--- | Beta reduction describes how functions behave when applied to arguments.
--- To reduce a function application, you simply 'substitute` the parameter into the function body.
---
--- Beta reduction is the fundamental computation step of the lambda calculus.
--- Only this rule is necessary for the lambda calculus to be turing-complete;
--- the other reductions merely define *equivalences* between expressions,
--- so that every expression has a canonical form.
-betaReduce :: Expression n -> Maybe (Expression n)
-betaReduce (Application (Abstraction fe) xe) = Just $ Substitution SZ xe fe
--- (^) Aside: 'Application' represents function application in the lambda calculus.
--- Haskell convention would be to name the function `f` and the argument `x`,
--- but that often collides with Haskell functions and arguments,
--- so instead I will be calling them `fe` and `xe`,
--- where the `e` stands for "expression".
-betaReduce  _                = Nothing
-
--- TODO: Document this.
-substitute :: Expression n -> Maybe (Expression n)
-substitute (Substitution SZ     x Variable)         = Just x
-substitute (Substitution (SS _) _ Variable)         = Just Variable
-substitute (Substitution SZ     x (Drop body)) = Just body
-substitute (Substitution (SS n) x (Drop body)) = Just $ Drop $ Substitution n x body
-substitute (Substitution n      x (Application fe xe)) = Just $ Application (Substitution n x fe) (Substitution n x xe)
-substitute (Substitution n      x (Abstraction body))  = Just $ Abstraction $ Substitution (SS n) x body
-substitute _                            = Nothing
-
--- | A predicate determining whether a subexpression would allow a beta-reduction step.
-isBetaRedex :: Expression n -> Bool
-isBetaRedex (Application (Abstraction _) _) = True
-isBetaRedex _               = False
-
--- | For any expression `f`, `f` is equivalent to `\x. ?f x`, a property called "eta-equivalence".
--- The conversion between these two forms is called "eta-conversion",
--- with the conversion from `f` to `\x. ?f x` being called "eta-expansion",
--- and its inverse (from `\x. ?f x` to `f`) being called "eta-reduction".
---
--- This rule is not necessary for the lambda calculus to express computation;
--- that's the purpose of 'betaReduce'; rather, it expresses the idea of "extensionality",
--- which in general describes the principles that judge objects to be equal
--- if they have the same external properties
--- (from within the context of the logical system, i.e. without regard to representation).
--- In the context of functions, this would mean that two functions are equal
--- if and only if they give the same result for all arguments.
-etaReduce :: Expression n -> Maybe (Expression n)
-etaReduce (Abstraction (Application (Drop fe) Variable)) = Just fe
-etaReduce _                         = Nothing
-
--- | A predicate determining whether a subexpression would allow an eta-reduction step.
-isEtaRedex :: Expression n -> Bool
-isEtaRedex (Abstraction (Application (Drop _) Variable )) = True
-isEtaRedex _                         = False
-
--- | Eta-expansion, the inverse of 'etaReduce'.
-etaExpand :: Expression n -> Expression n
-etaExpand fe = Abstraction $ Application (Drop fe) Variable
-
--- TODO: Scope conversion isn't a real conversion relationship!
--- 'scopeExpand' can only be applied a finite number of times.
--- That doesn't break the code, but I don't want to misrepresent it.
--- 'scopeExpand' is only the *left* inverse of 'scopeReduce',
--- not the inverse overall.
---
--- Alternatively, 'scopeExpand' could be defined on expressions with no sub-expressions.
--- That would make sense, but then 'scopeReduce' would also have to be defined like that,
--- which would make every reduction valid as well, meaning we can't use it in the same way
--- we use the other reduction, because it always succeeds, and thus every expression
--- could be considered reducible.
---
--- Perhaps delimiting scope should be external to the notion of an expression,
--- like how Thyer represented it in the "Lazy Specialization" paper
--- (http://thyer.name/phd-thesis/thesis-thyer.pdf).
---
--- In addition, it really doesn't fit in with the current scheme of reductions.
--- It doesn't apply to any particular constructor/eliminator relationship,
--- instead being this bizarre syntactical fragment instead of a real expression.
--- After all, I could have also chosen to represent the calculus
--- so that variables are parameterized by `Fin n` instead of being wrapped in stacks of 'Drop'.
---
--- I think this problem will work itself out as I work further on evaluation strategies
--- and alternative representations, but for now, it'll do.
--- | Scope-conversion describes how 'Drop'-delimited scopes propgate through expressions.
--- It expresses the idea that a variable is used in an expression
--- if and only if it is used in at least one of its sub-expressions.
---
--- Similarly to 'etaReduce', there is also define an inverse function, 'scopeExpand'.
-scopeReduce :: Expression n -> Maybe (Expression n)
-scopeReduce (Application (Drop fe) (Drop xe)) = Just $ Drop $ Application fe xe
--- TODO: I feel like there's a more elegant way to represent this.
--- It feels like `Abstraction (Drop body)` should be its own atomic unit.
--- Maybe I could consider a combinator-based representation,
--- where `Abstraction (Drop body)` is just the `K` combinator `K body`?
-scopeReduce (Abstraction (Drop (Drop body)))  = Just $ Drop $ Abstraction $ Drop body
-scopeReduce _                         = Nothing
-
--- | A predicate determining whether a subexpression would allow a scope-reduction step.
-isScopeRedex :: Expression n -> Bool
-isScopeRedex (Application (Drop _) (Drop _)) = True
-isScopeRedex (Abstraction (Drop (Drop _)))   = True
-isScopeRedex _                       = False
-
--- | Scope-expansion, the left inverse of 'scopeReduce'.
-scopeExpand :: Expression n -> Maybe (Expression n)
-scopeExpand (Drop (Application fe xe))         = Just $ Application (Drop fe) (Drop xe)
-scopeExpand (Drop (Abstraction (Drop body))) = Just $ Abstraction $ Drop $ Drop body
-scopeExpand _                                = Nothing
-
--- | An expression is in "normal form" if it contains no redexes (see 'isRedex').
-isNormal :: Expression n -> Bool
-isNormal expr = not (isRedex expr) && case expr of
-  -- In addition to this expression not being a redex,
-  -- we must check that none of its subexpressions are redexes either.
-  Application fe xe -> isNormal fe && isNormal xe
-  Abstraction e     -> isNormal e
-  Drop e    -> isNormal e
-  _         -> True
-
--- TODO: Finish the below documentation on reduction strategies. I got bored.
--- | Now that we have defined the ways in which an expression may be reduced ('reduce'),
--- we need to define a "reduction strategy" to describe in what order we will apply reductions.
--- Different reduction strategies have different performance characteristics,
--- and even produce different results.
---
--- One of the most important distinctions between strategies is whether they are "normalizing".
--- A normalising strategy will terminate if and only if
--- the expression it is normalizing has a normal form.
---
--- I have chosen to use a normalizing reduction strategy.
-eval :: Expression n -> Expression n
-eval expr = case reduce innerReduced of
-  Just e -> eval e
-  -- The expression didn't make any progress,
-  -- so we know that no further reductions can be applied here.
-  -- It must be blocked on something.
-  -- TODO: return why we stopped evaluating,
-  -- so we can avoid redundantly re-evaluating stuff if nothing changed.
-  Nothing -> innerReduced
-  where innerReduced = case expr of
-          -- TODO: Factor out this recursive case (from 'isNormal' too).
-          Application fe xe -> Application (eval fe) (eval xe)
-          Abstraction e -> Abstraction (eval e)
-          Drop e -> Drop (eval e)
-          x -> x
diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs
new file mode 100644
index 0000000..355671b
--- /dev/null
+++ b/src/LambdaCalculus/Expression.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE DeriveGeneric #-}
+module LambdaCalculus.Expression where
+
+import Data.List (elemIndex, find)
+import Data.Maybe (fromJust)
+import Data.HashSet (HashSet)
+import qualified Data.HashSet as HS
+import GHC.Generics (Generic)
+
+data Expression
+  = Variable String
+  | Application Expression Expression
+  | Abstraction String Expression
+  deriving (Eq, Generic)
+
+instance Show Expression where
+  show (Variable var) = var
+  show (Application ef ex) = "(" ++ show ef ++ " " ++ show ex ++ ")"
+  show (Abstraction var body) = "(^" ++ var ++ "." ++ show body ++ ")"
+
+-- | Free variables are variables which are present in an expression but not bound by any abstraction.
+freeVariables :: Expression -> HashSet String
+freeVariables (Variable variable) = HS.singleton variable
+freeVariables (Application ef ex) = freeVariables ef `HS.union` freeVariables ex
+freeVariables (Abstraction variable body) = HS.delete variable $ freeVariables body
+
+-- | Return True if the given variable is free in the given expression.
+freeIn :: String -> Expression -> Bool
+freeIn var1 (Variable var2) = var1 == var2
+freeIn var (Application ef ex) = var `freeIn` ef && var `freeIn` ex
+freeIn var1 (Abstraction var2 body) = var1 == var2 || var1 `freeIn` body
+
+-- | Bound variables are variables which are bound by any abstraction in an expression.
+boundVariables :: Expression -> HashSet String
+boundVariables (Variable _) = HS.empty
+boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
+boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
+
+-- | A closed expression is an expression with no free variables.
+-- Closed expressions are also known as combinators and are equivalent to terms in combinatory logic.
+closed :: Expression -> Bool
+closed = HS.null . freeVariables
+
+-- | Alpha-equivalent terms differ only by the names of bound variables,
+-- i.e. one can be converted to the other using only alpha-conversion.
+alphaEquivalent :: Expression -> Expression -> Bool
+alphaEquivalent = alphaEquivalent' [] []
+  where alphaEquivalent' :: [String] -> [String] -> Expression -> Expression -> Bool
+        alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2)
+          -- Two variables are alpha-equivalent if they are bound in the same location.
+          = bindingSite ctx1 v1 == bindingSite ctx2 v2
+        alphaEquivalent' ctx1 ctx2 (Application ef1 ex1) (Application ef2 ex2)
+          -- Two applications are alpha-equivalent if their components are alpha-equivalent.
+          = alphaEquivalent' ctx1 ctx2 ef1 ef2
+          && alphaEquivalent' ctx1 ctx2 ex1 ex2
+        alphaEquivalent' ctx1 ctx2 (Abstraction v1 b1) (Abstraction v2 b2)
+          -- Two abstractions are alpha-equivalent if their bodies are alpha-equivalent.
+          = alphaEquivalent' (v1 : ctx1) (v2 : ctx2) b1 b2
+
+        -- | The binding site of a variable is either the index of its binder
+        -- or, if it is unbound, the name of the free variable.
+        bindingSite :: [String] -> String -> Either String Int
+        bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx
+          where maybeToRight :: b -> Maybe a -> Either b a
+                maybeToRight default_ = maybe (Left default_) Right
+
+-- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression.
+substitute :: String -> Expression -> Expression -> Expression
+substitute var1 value unmodified@(Variable var2)
+  | var1 == var2 = value
+  | otherwise = unmodified
+substitute var value (Application ef ex)
+  = Application (substitute var value ef) (substitute var value ex)
+substitute var1 value unmodified@(Abstraction var2 body)
+  | var1 == var2 = unmodified
+  | otherwise = Abstraction var2' $ substitute var1 value $ alphaConvert var2 var2' body
+  where var2' = escapeName (freeVariables value) var2
+        alphaConvert oldName newName expr = substitute oldName (Variable newName) expr
+        -- | Generate a new name which isn't present in the set, based on the old name.
+        escapeName env name = fromJust $ find (not . free) names
+          where names = name : map ('\'' :) names
+                free = (`HS.member` env)
+
+-- | Returns True if the top-level expression is reducible by beta-reduction.
+betaRedex :: Expression -> Bool
+betaRedex (Application (Abstraction _ _) _) = True
+betaRedex _ = False
+
+-- | Returns True if the top-level expression is reducible by eta-reduction.
+etaRedex :: Expression -> Bool
+etaRedex (Abstraction var1 (Application ef (Variable var2)))
+  = var1 /= var2 || var1 `freeIn` ef
+etaRedex _ = False
+
+-- | In an expression in normal form, all reductions that can be applied have been applied.
+-- This is the result of applying eager evaluation.
+normal :: Expression -> Bool
+-- The expression is beta-reducible.
+normal (Application (Abstraction _ _) _) = False
+-- The expression is eta-reducible.
+normal (Abstraction var1 (Application fe (Variable var2)))
+  = var1 /= var2 || var1 `freeIn` fe
+normal (Application ef ex) = normal ef && normal ex
+normal _ = True
+
+-- | In an expression in weak head normal form, reductions to the function have been applied,
+-- but not all reductions to the parameter have been applied.
+-- This is the result of applying lazy evaluation.
+whnf :: Expression -> Bool
+whnf (Application (Abstraction _ _) _) = False
+whnf (Abstraction var1 (Application fe (Variable var2)))
+  = var1 /= var2 || var1 `freeIn` fe
+whnf (Application ef _) = whnf ef
+
+eval :: (Expression -> Expression) -> Expression -> Expression
+eval strategy = eval'
+  where eval' :: Expression -> Expression
+        eval' (Application ef ex) =
+          case ef' of
+            -- Beta-reduction
+            Abstraction var body -> eval' $ substitute var ex' body
+            _ -> Application ef' ex'
+          where ef' = eval' ef
+                ex' = strategy ex
+        eval' unmodified@(Abstraction var1 (Application ef (Variable var2)))
+          -- Eta-reduction
+          | var1 == var2 && not (var1 `freeIn` ef) = eval' ef
+          | otherwise = unmodified
+        eval' x = x
+
+-- | Reduce an expression to normal form.
+eagerEval :: Expression -> Expression
+eagerEval = eval eagerEval
+
+-- | Reduce an expression to weak head normal form.
+lazyEval :: Expression -> Expression
+lazyEval = eval id
diff --git a/src/LambdaCalculus/Parser.hs b/src/LambdaCalculus/Parser.hs
index 5fdf1ed..bf48197 100644
--- a/src/LambdaCalculus/Parser.hs
+++ b/src/LambdaCalculus/Parser.hs
@@ -1,79 +1,37 @@
-module LambdaCalculus.Parser (parse) where
+module LambdaCalculus.Parser (parseExpression) where
 
-import Control.Applicative (liftA2)
+import Control.Applicative ((*>))
 import Control.Monad (void)
-import Text.Parsec hiding (parse)
-import qualified Text.Parsec as Parsec
-import Text.Parsec.String (Parser)
-import LambdaCalculus.Representation.AbstractSyntax
+import LambdaCalculus.Expression (Expression (Variable, Application, Abstraction))
+import Text.Parsec hiding (spaces)
+import Text.Parsec.String
 
--- | Parse a keyword, unambiguously not a variable name.
-keyword :: String -> Parser ()
-keyword kwd = try $ do
-  void $ string kwd
-  -- TODO: rephrase this in terms of `extension`
-  notFollowedBy alphaNum
+spaces :: Parser ()
+spaces = void $ many1 space
 
--- | The extension of a variable name.
--- The first letter of a variable name must be a letter,
--- but the rest of the variable name may be more general.
-extension :: Parser String
-extension = many alphaNum
+variableName :: Parser String
+variableName = many1 letter
 
--- | A variable name, e.g. `x`, `foo`, `f2`, `fooBar27`.
-name :: Parser String
-name = do
-  notFollowedBy anyKeyword
-  liftA2 (:) letter extension
-  where
-    anyKeyword = choice $ map keyword keywords
-      where
-        -- | Keywords that are forbidden from use as variable names.
-        keywords = ["let", "in"]
-
--- | A variable expression.
 variable :: Parser Expression
-variable = Variable <$> name
+variable = Variable <$> variableName
+
+application :: Parser Expression
+application = foldl1 Application <$> sepBy1 applicationTerm spaces
+  where applicationTerm :: Parser Expression
+        applicationTerm = variable <|> abstraction <|> grouping
+          where grouping :: Parser Expression
+                grouping = between (char '(') (char ')') expression
 
--- | A lambda abstraction.
 abstraction :: Parser Expression
 abstraction = do
-  char 'λ' <|> char '\\'    ; spaces
-  variables <- variableList ; spaces
-  char '.'                  ; spaces
+  char '^'
+  names <- sepBy1 variableName spaces
+  char '.'
   body <- expression
-  return $ Abstraction variables body
-  where variableList :: Parser [String]
-        variableList = name `sepBy` spaces
+  pure $ foldr Abstraction body names
 
--- | A function application.
-application :: Parser Expression
-application = Application <$> applicationTerm `sepEndBy` spaces
-  where
-    -- | An application term is any expression which consumes input,
-    -- i.e. anything other than an ungrouped application.
-    applicationTerm :: Parser Expression
-    applicationTerm = let_ <|> variable <|> abstraction <|> grouping
-      where
-        -- | An expression grouped by parentheses.
-        grouping :: Parser Expression
-        grouping = between (char '(' >> spaces) (spaces >> char ')') expression
-
--- | A `let` expression.
-let_ :: Parser Expression
-let_ = do
-  keyword "let"       ; spaces
-  variable <- name    ; spaces
-  char '='            ; spaces
-  value <- expression ; spaces
-  string "in"         ; spaces
-  body <- expression
-  return $ Let variable value body
-
--- | Any expression.
 expression :: Parser Expression
-expression = application
+expression = abstraction <|> application <|> variable
 
--- | Parse a lambda calculus expression.
-parse :: SourceName -> String -> Either ParseError Expression
-parse = Parsec.parse (expression <* eof)
+parseExpression :: String -> Either ParseError Expression
+parseExpression = parse (expression <* eof) "input"
diff --git a/src/LambdaCalculus/Representation.hs b/src/LambdaCalculus/Representation.hs
deleted file mode 100644
index 7e39497..0000000
--- a/src/LambdaCalculus/Representation.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-module LambdaCalculus.Representation where
-
-import Data.Functor.Foldable (cata)
-import Data.HashSet (HashSet, singleton, union, delete)
-import LambdaCalculus.Representation.Standard
-
--- | `expr` is a representation of a /closed/ lambda calculus expression.
-class IsExpr expr where
-  -- | Convert an expression to the standard representation.
-  toStandard :: expr -> Expression
-
-  -- | Convert an expression from the standard representation.
-  fromStandard :: Expression -> expr
-
-  -- | Convert an expression from one representation to another.
-  convert :: IsExpr repr => expr -> repr
-  convert = fromStandard . toStandard
-
-  -- | Retrieve the free variables in an expression.
-  freeVariables :: expr -> HashSet String
-  freeVariables = freeVariables . toStandard
-
-instance IsExpr Expression where
-  toStandard    = id
-  fromStandard  = id
-  convert       = fromStandard
-  freeVariables = cata \case
-    VariableF name         -> singleton name
-    AbstractionF name body -> name `delete` body
-    ApplicationF fe xe     -> fe `union` xe
diff --git a/src/LambdaCalculus/Representation/AbstractSyntax.hs b/src/LambdaCalculus/Representation/AbstractSyntax.hs
deleted file mode 100644
index e755c1e..0000000
--- a/src/LambdaCalculus/Representation/AbstractSyntax.hs
+++ /dev/null
@@ -1,76 +0,0 @@
-module LambdaCalculus.Representation.AbstractSyntax where
-
-import Control.Comonad.Cofree (Cofree ((:<)))
-import Data.Functor.Foldable (cata, histo)
-import Data.Functor.Foldable.TH (makeBaseFunctor)
-import Data.List (foldl1')
-import LambdaCalculus.Combinators (i)
-import LambdaCalculus.Representation
-import qualified LambdaCalculus.Representation.Standard as Std
-
-data Expression = Variable String
-                | Abstraction [String] Expression
-                | Application [Expression]
-                -- | `let name = value in body`
-                | Let String Expression Expression
-
-makeBaseFunctor ''Expression
-
-instance Show Expression where
-  show = histo \case
-    VariableF name -> name
-    AbstractionF names (body :< _) -> "λ" ++ unwords names ++ ". " ++ body
-    -- TODO: this is a weird implementation of re-grouping variables,
-    -- to the degree that explicit recursion would probably be more clear.
-    -- Clean this up!
-    ApplicationF exprs -> unwords $ mapExceptLast regroup regroupApplication exprs
-    LetF name (value :< _) (body :< _)
-      -> "let " ++ name ++ " = " ++ value ++ " in " ++ body
-    where regroup (expr :< AbstractionF _ _) = group expr
-          regroup (expr :< LetF _ _ _)       = group expr
-          regroup expr                       = regroupApplication expr
-
-          regroupApplication (expr :< ApplicationF _) = group expr
-          regroupApplication (expr :< _)              = expr
-
-          group str = "(" ++ str ++ ")"
-
-          -- | Map the first function to all but the last element of the list,
-          -- and the last function to only the last element.
-          mapExceptLast :: (a -> b) -> (a -> b) -> [a] -> [b]
-          -- TODO: express this as a paramorphism
-          mapExceptLast _ _     []     = []
-          mapExceptLast _ fLast [x]    = [fLast x]
-          mapExceptLast f fLast (x:xs) = f x : mapExceptLast f fLast xs
-
-instance IsExpr Expression where
-  toStandard = cata \case
-    VariableF    name       -> Std.Variable name
-    -- We could technically just use `foldl' Std.Application i exprs`,
-    -- since that's the justification for allowing non-binary applications in the first place,
-    -- but we want expressions using only binary applications
-    -- to still generate the same expression,
-    -- not just beta-equivalent expressions.
-    ApplicationF []         -> i
-    ApplicationF [expr]     -> expr
-    ApplicationF exprs      -> foldl1' Std.Application exprs
-    AbstractionF names body -> foldr Std.Abstraction body names
-    LetF name value body    -> Std.Application (Std.Abstraction name body) value
-
-  -- Again with the intent of generating the canonical form for this representation,
-  -- we want to convert all left-nested applications into a list application;
-  -- similarly, we convert nested abstractions into a list of names,
-  -- and abstractions into `let`s when applicable.
-  fromStandard = histo \case
-    Std.VariableF name -> Variable name
-    -- `(\x. e) N` --> `let x = N in e`.
-    Std.ApplicationF (_ :< Std.AbstractionF name (body :< _)) (value :< _)
-      -> Let name value body
-    Std.ApplicationF (Application exprs :< _) (xe :< _)
-      -> Application $ exprs ++ [xe]
-    Std.ApplicationF (fe                :< _) (xe :< _)
-      -> Application [fe, xe]
-    Std.AbstractionF name (Abstraction names body :< _)
-      -> Abstraction (name : names) body
-    Std.AbstractionF name (body :< _)
-      -> Abstraction [name]         body
diff --git a/src/LambdaCalculus/Representation/Dependent/ReverseDeBruijn.hs b/src/LambdaCalculus/Representation/Dependent/ReverseDeBruijn.hs
deleted file mode 100644
index d98f9b5..0000000
--- a/src/LambdaCalculus/Representation/Dependent/ReverseDeBruijn.hs
+++ /dev/null
@@ -1,74 +0,0 @@
-module LambdaCalculus.Representation.Dependent.ReverseDeBruijn where
-
-import Control.Monad.Reader (Reader, runReader, withReader, asks)
-import Data.Type.Equality ((:~:)(Refl))
-import Data.Type.Nat
-import Data.Vec
-import LambdaCalculus.Representation
-import qualified LambdaCalculus.Representation.Standard as Std
-
--- | Expressions are parametrized by the depth of the variable bindings they may access.
--- An expression in which no variables are bound (a closed expression) is represented by `Expression 'Z`.
-data Expression :: Nat -> * where
-  -- | The body of a lambda abstraction may reference all of the variables
-  -- bound in its parent, in addition to a new variable bound by the abstraction.
-  Abstraction :: Expression ('S n) -> Expression n
-  -- | On the other hand, any sub-expression may choose to simply ignore
-  -- the variable bound by the lambda expression,
-  -- only referencing the variables bound in its parent instead.
-  --
-  -- For example, in the constant function `\x. \y. x`,
-  -- although the innermost expression *may* access the innermost binding (`y`),
-  -- it instead only accesses the outer one, `x`.
-  -- Thus the body of the expression would be `Drop Variable`.
-  --
-  -- Given the lack of any convention for how to write 'Drop',
-  -- I have chosen to write it as `?x` where `x` is the body of the drop.
-  Drop :: Expression n -> Expression ('S n)
-  -- | For this reason (see 'Drop'),
-  -- variables only need to access the innermost accessible binding.
-  -- To access outer bindings, you must first 'Drop' all of the bindings
-  -- in between the variable and the desired binding to access.
-  Variable :: Expression ('S n)
-  -- | Function application. The left side is the function, and the right side is the argument.
-  Application :: Expression n -> Expression n -> Expression n
-  -- | A free expression is a symbolic placeholder which reduces to itself.
-  Free :: String -> Expression 'Z
-  Substitution :: SNat n -> Expression m -> Expression ('S (Plus n m)) -> Expression (Plus n m)
-
-instance SNatI n => Show (Expression n) where
-  show expr = show' snat expr
-    where show' :: SNat n -> Expression n -> String
-          show' (SS n) Variable    = show n
-          show' SZ     (Free name) = name
-          show' (SS n) (Drop body) = '?' : show' n body
-          show' n      (Abstraction body)  = "(\\" ++ show n ++ " " ++ show' (SS n) body ++ ")"
-          show' n      (Application fe xe) = "(" ++ show' n fe ++ " " ++ show' n xe ++ ")"
-
-instance IsExpr (Expression 'Z) where 
-  fromStandard expr = runReader (fromStandard' expr) VNil
-    where fromStandard' :: SNatI n => Std.Expression -> Reader (Vec n String) (Expression n)
-          -- TODO: This code is absolutely atrocious.
-          -- It is in dire need of cleanup.
-          fromStandard' (Std.Variable name) = asks $ makeVar snat SZ
-            where makeVar :: SNat n -> SNat m -> Vec n String -> Expression (Plus m n)
-                  makeVar SZ     m VNil            = dropEm m $ Free name
-                  makeVar (SS n) m (var ::: bound) = case plusSuc m n of
-                    Refl
-                      | name == var -> dropEm2 n m
-                      | otherwise   -> makeVar n (SS m) bound
-
-                  dropEm :: SNat m -> Expression n -> Expression (Plus m n)
-                  dropEm SZ     e = e
-                  dropEm (SS n) e = Drop $ dropEm n e
-
-                  dropEm2 :: SNat n -> SNat m -> Expression ('S (Plus m n))
-                  dropEm2 _ SZ = Variable
-                  dropEm2 n (SS m) = Drop $ dropEm2 n m
-          fromStandard' (Std.Abstraction name body)
-            = fmap Abstraction $ withReader (name :::) $ fromStandard' body
-          fromStandard' (Std.Application fe xe)
-            = Application <$> fromStandard' fe <*> fromStandard' xe
-
-  -- TODO: Implement this. Important!
-  toStandard expr = undefined
diff --git a/src/LambdaCalculus/Representation/Standard.hs b/src/LambdaCalculus/Representation/Standard.hs
deleted file mode 100644
index 31aafe4..0000000
--- a/src/LambdaCalculus/Representation/Standard.hs
+++ /dev/null
@@ -1,18 +0,0 @@
-module LambdaCalculus.Representation.Standard where
-
-import Data.Functor.Foldable (cata)
-import Data.Functor.Foldable.TH (makeBaseFunctor)
-
-data Expression = Variable String
-                | Abstraction String Expression
-                | Application Expression Expression
-
-makeBaseFunctor ''Expression
-
-instance Show Expression where
-  -- For a more sophisticated printing mechanism,
-  -- consider converting to 'LambdaCalculus.Representation.AbstractSyntax.Expression' first.
-  show = cata \case
-    VariableF name -> name
-    AbstractionF name body -> "(λ" ++ name ++ ". " ++ body ++ ")"
-    ApplicationF fe xe -> "(" ++ fe ++ " " ++ xe ++ ")"
diff --git a/stack.yaml b/stack.yaml
index ea3f61f..3bda96a 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,66 +1,3 @@
-# This file was automatically generated by 'stack init'
-#
-# Some commonly used options have been documented as comments in this file.
-# For advanced use and comprehensive documentation of the format, please see:
-# https://docs.haskellstack.org/en/stable/yaml_configuration/
-
-# Resolver to choose a 'specific' stackage snapshot or a compiler version.
-# A snapshot resolver dictates the compiler version and the set of packages
-# to be used for project dependencies. For example:
-#
-# resolver: lts-3.5
-# resolver: nightly-2015-09-21
-# resolver: ghc-7.10.2
-#
-# The location of a snapshot can be provided as a file or url. Stack assumes
-# a snapshot provided as a file might change, whereas a url resource does not.
-#
-# resolver: ./custom-snapshot.yaml
-# resolver: https://example.com/snapshots/2018-01-01.yaml
-resolver: lts-14.1
-
-# User packages to be built.
-# Various formats can be used as shown in the example below.
-#
-# packages:
-# - some-directory
-# - https://example.com/foo/bar/baz-0.0.2.tar.gz
-#   subdirs:
-#   - auto-update
-#   - wai
+resolver: lts-14.17
 packages:
 - .
-# Dependency packages to be pulled from upstream that are not in the resolver.
-# These entries can reference officially published versions as well as
-# forks / in-progress versions pinned to a git hash. For example:
-#
-# extra-deps:
-# - acme-missiles-0.3
-# - git: https://github.com/commercialhaskell/stack.git
-#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
-#
-# extra-deps: []
-
-# Override default flag values for local packages and extra-deps
-# flags: {}
-
-# Extra package databases containing global packages
-# extra-package-dbs: []
-
-# Control whether we use the GHC we find on the path
-# system-ghc: true
-#
-# Require a specific version of stack, using version ranges
-# require-stack-version: -any # Default
-# require-stack-version: ">=2.1"
-#
-# Override the architecture used by stack, especially useful on Windows
-# arch: i386
-# arch: x86_64
-#
-# Extra directories used by stack for building
-# extra-include-dirs: [/path/to/dir]
-# extra-lib-dirs: [/path/to/dir]
-#
-# Allow a newer minor version of GHC than the snapshot specifies
-# compiler-check: newer-minor
diff --git a/stack.yaml.lock b/stack.yaml.lock
index be895e2..fc538c1 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -6,7 +6,7 @@
 packages: []
 snapshots:
 - completed:
-    size: 523448
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/1.yaml
-    sha256: 0045b9bae36c3bb2dd374c29b586389845af1557eea0423958d152fc500d4fbf
-  original: lts-14.1
+    size: 524799
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/17.yaml
+    sha256: 1d72b33c0fc048e23f4f18fd76a6ad79dd1d8a3c054644098a71a09855e40c7c
+  original: lts-14.17
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
index 0000000..9a78cf7
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,58 @@
+import Data.Char (isAlpha)
+import Generic.Random (genericArbitraryRec, uniform)
+import LambdaCalculus.Expression
+import LambdaCalculus.Parser
+import Test.QuickCheck
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+
+instance Arbitrary Expression where
+  arbitrary = genericArbitraryRec uniform
+
+dfi :: Expression
+dfi = Application d (Application f i)
+  where d = Abstraction "x" $ Application (Variable "x") (Variable "x")
+        f = Abstraction "f" $ Application (Variable "f") (Application (Variable "f") (Variable "y"))
+        i = Abstraction "x" $ Variable "x"
+
+ttttt :: Expression
+ttttt = Application (Application (Application f t) (Abstraction "x" (Variable "x"))) (Variable "y")
+  where t = Abstraction "f" $ Abstraction "x" $
+          Application (Variable "f") (Application (Variable "f") (Variable "x"))
+        f = Abstraction "T" $ Abstraction "f" $ Abstraction "x" $
+          Application (Application
+                        (Application (Variable "T")
+                         (Application (Variable "T")
+                          (Application (Variable "T")
+                           (Application (Variable "T")
+                            (Variable "T")))))
+                        (Variable "f"))
+          (Variable "x")
+
+prop_parseExpression_inverse :: Expression -> Bool
+prop_parseExpression_inverse expr' = Right expr == parseExpression (show expr)
+  where expr = legalizeVariables expr'
+        legalizeVariables (Variable var) = Variable $ legalVar var
+        legalizeVariables (Application ef ex) = Application (legalizeVariables ef) (legalizeVariables ex)
+        legalizeVariables (Abstraction var body) = Abstraction (legalVar var) $ legalizeVariables body
+        legalVar var = 'v' : filter isAlpha var
+
+
+main :: IO ()
+main = defaultMain $
+  testGroup "Tests"
+  [ testGroup "Evaluator tests"
+    [ testCase "DFI" $ eagerEval dfi @?= Application (Variable "y") (Variable "y")
+    , testCase "ttttt" $ eagerEval ttttt @?= Variable "y"
+    ]
+  , testGroup "Parser tests"
+    [ testGroup "Unit tests"
+      [ testCase "identity" $ parseExpression "^x.x" @?= Right (Abstraction "x" $ Variable "x")
+      , testCase "application shorthand" $ parseExpression "a b c d" @?= Right (Application (Application (Application (Variable "a") (Variable "b")) (Variable "c")) (Variable "d"))
+      , testCase "ttttt" $ parseExpression "(^T f x.(T (T (T (T T)))) f x) (^f x.f (f x)) (^x.x) y"
+          @?= Right ttttt
+      ]
+    , testProperty "parseExpression is the left inverse of show" prop_parseExpression_inverse
+    ]
+  ]