From 807a0cb1eee837fe8750460fa90f14e57a15eaa6 Mon Sep 17 00:00:00 2001
From: James Martin <james@jtmar.me>
Date: Thu, 29 Aug 2019 20:46:42 -0700
Subject: [PATCH] Massive refactoring. This project is no longer "just an
 exercise". * Allows for multiple representations   * Evaluation strategies  
 * Type systems. * No longer just the untyped lambda calculus. * No longer
 "just an experiment".

---
 README.md                                     |  77 ++++++++++-
 app/Main.hs                                   |  11 +-
 jtm-lambda-calculus.cabal                     |  70 ++++++++++
 package.yaml                                  |  17 ++-
 src/LambdaCalculus/Combinators.hs             |   8 ++
 .../Evaluation/Optimal.hs}                    | 125 +++++++-----------
 src/LambdaCalculus/Parser.hs                  |  79 +++++++++++
 src/LambdaCalculus/Representation.hs          |  30 +++++
 .../Representation/AbstractSyntax.hs          |  76 +++++++++++
 .../Dependent/ReverseDeBruijn.hs              |  74 +++++++++++
 src/LambdaCalculus/Representation/Standard.hs |  18 +++
 src/UntypedLambdaCalculus/Parser.hs           |  95 -------------
 12 files changed, 491 insertions(+), 189 deletions(-)
 create mode 100644 jtm-lambda-calculus.cabal
 create mode 100644 src/LambdaCalculus/Combinators.hs
 rename src/{UntypedLambdaCalculus.hs => LambdaCalculus/Evaluation/Optimal.hs} (63%)
 create mode 100644 src/LambdaCalculus/Parser.hs
 create mode 100644 src/LambdaCalculus/Representation.hs
 create mode 100644 src/LambdaCalculus/Representation/AbstractSyntax.hs
 create mode 100644 src/LambdaCalculus/Representation/Dependent/ReverseDeBruijn.hs
 create mode 100644 src/LambdaCalculus/Representation/Standard.hs
 delete mode 100644 src/UntypedLambdaCalculus/Parser.hs

diff --git a/README.md b/README.md
index 82c644c..c56070b 100644
--- a/README.md
+++ b/README.md
@@ -1,10 +1,9 @@
-# untyped-lambda-calculus
-A simple implementation of the untyped lambda calculus as an exercise.
+# James Martin's Lambda Calculus
+An implementation of various type systems and evaluation strategies
+for the lambda calculus.
 
-This implementation lacks many features necessary to be useful,
-for example `let` bindings, built-in functions, binding free variables, or a good REPL.
-This project purely exists as an exercise and is not intended for general use.
-I will make useful programming languages in the future, but this is not one of them.
+This project is a work-in-progress, and currently lacks many essential features
+that would be necessary to be a useful programming language.
 
 ## Usage
 Type in your expression at the prompt: `>> `.
@@ -45,3 +44,69 @@ Since `\x. x` is the left identity of applications and application syntax is lef
 I (syntactically) permit unary and nullary applications so that `()` is `\x. x`, and `(x)` is `x`.
 
 On the same principle, the syntax of a lambda of no variables `\. e` is `e`.
+
+## Roadmap
+### Complete
+* Type systems:
+  * Untyped
+* Representations:
+  * The syntax tree
+  * Reverse de Bruijn
+* Syntax:
+  * Basic syntax
+  * Let expressions
+* Evaluation strategies:
+  * Lazy (call-by-name to normal form)
+  
+### In-progress
+* Type systems:
+  * Simply typed
+* Representations:
+  * De Bruijn
+
+### Planned
+My ultimate goal is to develop this into a programming language
+that would at least theoretically be practically useful.
+I intend to do a lot more than this in the long run,
+but it's far enough off that I haven't nailed down the specifics yet.
+
+* Built-ins:
+  * Integers
+* Type systems:
+  * Hindley-Milner
+  * System F
+* Representations:
+  * A more conservative syntax tree that would allow for better error messages
+* Evaluation strategies:
+  * Complete laziness
+  * Optimal
+* Syntax:
+  * Top-level definitions
+  * Type annotations
+  * `let*`, `letrec`
+  * More syntax (parsing and printing) options:
+    * Also allow warnings instead of errors on disabled syntax.
+      * Or set a preferred printing style without warnings.
+      * Or print in an entirely different syntax than the input!
+    * Disable empty `application`: `()` no longer parses (as `\x. x`).
+      * Forbid single-term `application`: `(x)` no longer parses as `x`.
+    * Disable empty `variable-list`: `λ. x` no longer parses (as just `x`).
+    * Disable block arguments: `f λx. x` is no longer permitted; `f (λx. x)` must be used instead.
+      * Except for at the top level, where an unclosed lambda is always permitted.
+    * Configurable `variable-list` syntax:
+      * Mathematics style: One-letter variable names, no variable separators.
+      * Computer science style: Variable names separated by commas instead of spaces.
+    * Configurable `λ` syntax: any one of `λ`, `\`, or `^`, as I've seen all three in use.
+      * Currently, either `λ` or `\` is permitted, and it is impossible to disable either.
+    * Disable `let` expressions.
+    * Disable syntactic sugar entirely (never drop parentheses).
+    * Pedantic mode: forbid using more parentheses than necessary.
+    * Pedantic whitespace (e.g. forbid ` (  a    b c)`).
+  * Pretty-printing mode.
+  * Indentation-based syntax.
+* Features:
+  * A better REPL (e.g. the ability to edit the line buffer)
+  * The ability to import external files
+  * The ability to choose the type system or evaluation strategy
+  * Better error messages for parsing and typechecking
+  * Reduction stepping
diff --git a/app/Main.hs b/app/Main.hs
index a9b20ed..33e976f 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,9 +1,12 @@
 module Main where
 
 import Control.Monad (forever)
+import Data.Type.Nat (Nat (Z))
 import System.IO (hFlush, stdout)
-import UntypedLambdaCalculus (eval)
-import UntypedLambdaCalculus.Parser (parseExpr)
+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
@@ -12,6 +15,6 @@ prompt text = do
   getLine
 
 main :: IO ()
-main = forever $ parseExpr "stdin" <$> prompt ">> " >>= \case
+main = forever $ parse "stdin" <$> prompt ">> " >>= \case
   Left parseError -> putStrLn $ "Parse error: " ++ show parseError
-  Right expr -> do print expr; print $ eval expr
+  Right expr -> do print expr; print $ eval (convert expr :: Expression 'Z)
diff --git a/jtm-lambda-calculus.cabal b/jtm-lambda-calculus.cabal
new file mode 100644
index 0000000..6a2cf89
--- /dev/null
+++ b/jtm-lambda-calculus.cabal
@@ -0,0 +1,70 @@
+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 4595bf1..3653672 100644
--- a/package.yaml
+++ b/package.yaml
@@ -1,13 +1,13 @@
-name:                untyped-lambda-calculus
+name:                jtm-lambda-calculus
 version:             0.1.0.0
-github:              "jamestmartin/untyped-lambda-calculus"
+github:              "jamestmartin/lambda-calculus"
 license:             GPL-3
 author:              "James Martin"
 maintainer:          "james@jtmar.me"
 copyright:           "2019 James Martin"
-synopsis:            "A simple implementation of the untyped lambda calculus as an exercise."
+synopsis:            "Implementations of various Lambda Calculus evaluators and type systems."
 category:            LambdaCalculus
-description:         Please see the README on GitHub at <https://github.com/jamestmartin/untyped-lambda-calculus#readme>
+description:         Please see the README on GitHub at <https://github.com/jamestmartin/lambda-calculus#readme>
 
 extra-source-files:
 - README.md
@@ -32,14 +32,19 @@ default-extensions:
 
 dependencies:
 - base >= 4.7 && < 5
+# used for `recursion-schemes` histomorphisms
+- free >= 5.1 && < 6
 - mtl >= 2.2 && < 3
 - 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:
-  untyped-lambda-calculus-exe:
+  jtm-lambda-calculus-exe:
     main:                Main.hs
     source-dirs:         app
     ghc-options:
@@ -47,4 +52,4 @@ executables:
     - -rtsopts
     - -with-rtsopts=-N
     dependencies:
-    - untyped-lambda-calculus
+    - jtm-lambda-calculus
diff --git a/src/LambdaCalculus/Combinators.hs b/src/LambdaCalculus/Combinators.hs
new file mode 100644
index 0000000..a3531b1
--- /dev/null
+++ b/src/LambdaCalculus/Combinators.hs
@@ -0,0 +1,8 @@
+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/UntypedLambdaCalculus.hs b/src/LambdaCalculus/Evaluation/Optimal.hs
similarity index 63%
rename from src/UntypedLambdaCalculus.hs
rename to src/LambdaCalculus/Evaluation/Optimal.hs
index d8b432e..2a2b7d5 100644
--- a/src/UntypedLambdaCalculus.hs
+++ b/src/LambdaCalculus/Evaluation/Optimal.hs
@@ -1,45 +1,14 @@
-module UntypedLambdaCalculus where
+-- | !!!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 (Nat (Z, S), SNat (SZ, SS), SNatI, Plus, snat)
-
--- | 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 `Expr 'Z`.
-data Expr :: 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.
-  Lam :: Expr ('S n) -> Expr 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 Var`.
-  --
-  -- 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 :: Expr n -> Expr ('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.
-  Var :: Expr ('S n)
-  -- | Function application. The left side is the function, and the right side is the argument.
-  App :: Expr n -> Expr n -> Expr n
-  -- | A free expression is a symbolic placeholder which reduces to itself.
-  Free :: String -> Expr 'Z
-  Subst :: SNat n -> Expr m -> Expr ('S (Plus n m)) -> Expr (Plus n m)
-
-instance SNatI n => Show (Expr n) where
-  show expr = show' snat expr
-    where show' :: SNat n -> Expr n -> String
-          show' (SS n) Var         = show n
-          show' SZ     (Free name) = name
-          show' (SS n) (Drop body) = '?' : show' n body
-          show' n      (Lam body)  = "(\\" ++ show n ++ " " ++ show' (SS n) body ++ ")"
-          show' n      (App fe xe) = "(" ++ show' n fe ++ " " ++ show' n xe ++ ")"
+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'),
@@ -52,14 +21,14 @@ instance SNatI n => Show (Expr n) where
 -- 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 :: Expr n -> Maybe (Expr n)
+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 :: Expr n -> Bool
+isRedex :: Expression n -> Bool
 isRedex expr = isScopeRedex expr || isBetaRedex expr || isEtaRedex expr
 
 -- | Beta reduction describes how functions behave when applied to arguments.
@@ -69,9 +38,9 @@ isRedex expr = isScopeRedex expr || isBetaRedex expr || isEtaRedex expr
 -- 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 :: Expr n -> Maybe (Expr n)
-betaReduce (App (Lam fe) xe) = Just $ Subst SZ xe fe
--- (^) Aside: 'App' represents function application in the lambda calculus.
+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`,
@@ -79,18 +48,18 @@ betaReduce (App (Lam fe) xe) = Just $ Subst SZ xe fe
 betaReduce  _                = Nothing
 
 -- TODO: Document this.
-substitute :: Expr n -> Maybe (Expr n)
-substitute (Subst SZ     x Var)         = Just x
-substitute (Subst (SS _) _ Var)         = Just Var
-substitute (Subst SZ     x (Drop body)) = Just body
-substitute (Subst (SS n) x (Drop body)) = Just $ Drop $ Subst n x body
-substitute (Subst n      x (App fe xe)) = Just $ App (Subst n x fe) (Subst n x xe)
-substitute (Subst n      x (Lam body))  = Just $ Lam $ Subst (SS n) x body
+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 :: Expr n -> Bool
-isBetaRedex (App (Lam _) _) = True
+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".
@@ -105,18 +74,18 @@ isBetaRedex _               = False
 -- (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 :: Expr n -> Maybe (Expr n)
-etaReduce (Lam (App (Drop fe) Var)) = Just fe
+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 :: Expr n -> Bool
-isEtaRedex (Lam (App (Drop _) Var )) = True
+isEtaRedex :: Expression n -> Bool
+isEtaRedex (Abstraction (Application (Drop _) Variable )) = True
 isEtaRedex _                         = False
 
 -- | Eta-expansion, the inverse of 'etaReduce'.
-etaExpand :: Expr n -> Expr n
-etaExpand fe = Lam $ App (Drop fe) Var
+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.
@@ -147,34 +116,34 @@ etaExpand fe = Lam $ App (Drop fe) Var
 -- 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 :: Expr n -> Maybe (Expr n)
-scopeReduce (App (Drop fe) (Drop xe)) = Just $ Drop $ App fe xe
+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 `Lam (Drop body)` should be its own atomic unit.
+-- It feels like `Abstraction (Drop body)` should be its own atomic unit.
 -- Maybe I could consider a combinator-based representation,
--- where `Lam (Drop body)` is just the `K` combinator `K body`?
-scopeReduce (Lam (Drop (Drop body)))  = Just $ Drop $ Lam $ Drop body
+-- 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 :: Expr n -> Bool
-isScopeRedex (App (Drop _) (Drop _)) = True
-isScopeRedex (Lam (Drop (Drop _)))   = True
+isScopeRedex :: Expression n -> Bool
+isScopeRedex (Application (Drop _) (Drop _)) = True
+isScopeRedex (Abstraction (Drop (Drop _)))   = True
 isScopeRedex _                       = False
 
 -- | Scope-expansion, the left inverse of 'scopeReduce'.
-scopeExpand :: Expr n -> Maybe (Expr n)
-scopeExpand (Drop (App fe xe))       = Just $ App (Drop fe) (Drop xe)
-scopeExpand (Drop (Lam (Drop body))) = Just $ Lam $ Drop $ Drop body
-scopeExpand _                        = Nothing
+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 :: Expr n -> Bool
+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.
-  App fe xe -> isNormal fe && isNormal xe
-  Lam e     -> isNormal e
+  Application fe xe -> isNormal fe && isNormal xe
+  Abstraction e     -> isNormal e
   Drop e    -> isNormal e
   _         -> True
 
@@ -189,7 +158,7 @@ isNormal expr = not (isRedex expr) && case expr of
 -- the expression it is normalizing has a normal form.
 --
 -- I have chosen to use a normalizing reduction strategy.
-eval :: Expr n -> Expr n
+eval :: Expression n -> Expression n
 eval expr = case reduce innerReduced of
   Just e -> eval e
   -- The expression didn't make any progress,
@@ -200,7 +169,7 @@ eval expr = case reduce innerReduced of
   Nothing -> innerReduced
   where innerReduced = case expr of
           -- TODO: Factor out this recursive case (from 'isNormal' too).
-          App fe xe -> App (eval fe) (eval xe)
-          Lam e -> Lam (eval e)
+          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/Parser.hs b/src/LambdaCalculus/Parser.hs
new file mode 100644
index 0000000..5fdf1ed
--- /dev/null
+++ b/src/LambdaCalculus/Parser.hs
@@ -0,0 +1,79 @@
+module LambdaCalculus.Parser (parse) where
+
+import Control.Applicative (liftA2)
+import Control.Monad (void)
+import Text.Parsec hiding (parse)
+import qualified Text.Parsec as Parsec
+import Text.Parsec.String (Parser)
+import LambdaCalculus.Representation.AbstractSyntax
+
+-- | 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
+
+-- | 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
+
+-- | 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
+
+-- | A lambda abstraction.
+abstraction :: Parser Expression
+abstraction = do
+  char 'λ' <|> char '\\'    ; spaces
+  variables <- variableList ; spaces
+  char '.'                  ; spaces
+  body <- expression
+  return $ Abstraction variables body
+  where variableList :: Parser [String]
+        variableList = name `sepBy` spaces
+
+-- | 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
+
+-- | Parse a lambda calculus expression.
+parse :: SourceName -> String -> Either ParseError Expression
+parse = Parsec.parse (expression <* eof)
diff --git a/src/LambdaCalculus/Representation.hs b/src/LambdaCalculus/Representation.hs
new file mode 100644
index 0000000..7e39497
--- /dev/null
+++ b/src/LambdaCalculus/Representation.hs
@@ -0,0 +1,30 @@
+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
new file mode 100644
index 0000000..e755c1e
--- /dev/null
+++ b/src/LambdaCalculus/Representation/AbstractSyntax.hs
@@ -0,0 +1,76 @@
+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
new file mode 100644
index 0000000..d98f9b5
--- /dev/null
+++ b/src/LambdaCalculus/Representation/Dependent/ReverseDeBruijn.hs
@@ -0,0 +1,74 @@
+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
new file mode 100644
index 0000000..31aafe4
--- /dev/null
+++ b/src/LambdaCalculus/Representation/Standard.hs
@@ -0,0 +1,18 @@
+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/src/UntypedLambdaCalculus/Parser.hs b/src/UntypedLambdaCalculus/Parser.hs
deleted file mode 100644
index 53e642a..0000000
--- a/src/UntypedLambdaCalculus/Parser.hs
+++ /dev/null
@@ -1,95 +0,0 @@
-module UntypedLambdaCalculus.Parser (parseExpr) where
-
-import Control.Applicative (liftA2)
-import Control.Monad.Reader (Reader, runReader, withReader, asks)
-import Data.Type.Equality ((:~:)(Refl))
-import Data.Type.Nat
-import Data.Vec
-import Text.Parsec (SourceName, ParseError, (<|>), many, sepBy, letter, alphaNum, char, between, spaces, parse, string)
-import Text.Parsec.String (Parser)
-import UntypedLambdaCalculus (Expr (Free, Var, Lam, App, Drop))
-
-data Ast = AstVar String
-         | AstLam [String] Ast
-         | AstApp [Ast]
-         | AstLet String Ast Ast
-
--- | A variable name.
-name :: Parser String
-name = liftA2 (:) letter $ many alphaNum
-
--- | A variable expression.
-var :: Parser Ast
-var = AstVar <$> name
-
--- | Run parser between parentheses.
-parens :: Parser a -> Parser a
-parens = between (char '(') (char ')')
-
--- | A lambda expression.
-lam :: Parser Ast
-lam = do
-  vars <- between (char '\\') (char '.') $ name `sepBy` spaces
-  spaces
-  body <- app
-  return $ AstLam vars body
-
--- | An application expression.
-app :: Parser Ast
-app = AstApp <$> consumesInput `sepBy` spaces
-
-let_ :: Parser Ast
-let_ = do
-  string "let "
-  bound <- name
-  string " = "
-  -- we can't allow raw `app` or `lam` here
-  -- because they will consume the `in` as a variable.
-  val <- let_ <|> var <|> parens app
-  char ' '
-  spaces
-  string "in "
-  body <- app
-  return $ AstLet bound val body
-
--- | 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).
-consumesInput :: Parser Ast
-consumesInput = let_ <|> var <|> lam <|> parens app
-
-toExpr :: Ast -> Expr 'Z
-toExpr ast = runReader (toExpr' ast) VNil
-  -- TODO: This code is absolutely atrocious.
-  -- It is in dire need of cleanup.
-  where toExpr' :: SNatI n => Ast -> Reader (Vec n String) (Expr n)
-        toExpr' (AstVar name) = asks $ makeVar snat SZ
-          where makeVar :: SNat n -> SNat m -> Vec n String -> Expr (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
-        toExpr' (AstApp es) = asks $ thingy id es
-        toExpr' (AstLam [] body) = toExpr' body
-        toExpr' (AstLam (name:names) body) =
-          fmap Lam $ withReader (name :::) $ toExpr' $ AstLam names body
-        toExpr' (AstLet var val body) =
-          App <$> toExpr' (AstLam [var] body) <*> toExpr' val
-
-        thingy :: SNatI n => (Expr n -> Expr n) -> [Ast] -> Vec n String -> Expr n
-        thingy f []     _     = f $ Lam Var
-        thingy f (e:es) bound = thingy (flip App (runReader (toExpr' e) bound) . f) es bound
-
-        dropEm :: SNat m -> Expr n -> Expr (Plus m n)
-        dropEm SZ     e = e
-        dropEm (SS n) e = Drop $ dropEm n e
-
-        dropEm2 :: SNat n -> SNat m -> Expr ('S (Plus m n))
-        dropEm2 _ SZ = Var
-        dropEm2 n (SS m) = Drop $ dropEm2 n m
-          
--- | Since applications do not require parentheses and can contain only a single item,
--- | the `app` parser is sufficient to parse any expression at all.
-parseExpr :: SourceName -> String -> Either ParseError (Expr 'Z)
-parseExpr sourceName code = toExpr <$> parse app sourceName code