Simplified the code, at the cost of removing type-level invariants.

package.yaml

@@ -16,7 +16,7 @@ dependencies:
 - base >= 4.7 && < 5
 - mtl >= 2.2 && < 3
 - parsec >= 3.1 && < 4
-- transformers >= 0.5.6 && < 0.6
+- recursion-schemes >= 5.1 && < 6
 
 library:
   source-dirs: src

src/Data/Fin.hs

@@ -1,48 +0,0 @@
-{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
-module Data.Fin (Fin (FZ, FS), toInt, coerceFin, pred, extract) where
-
-import Data.Nat (Nat (S))
-import Prelude hiding (pred)
-import Unsafe.Coerce (unsafeCoerce)
-
--- | A type with `n` inhabitants, or alternatively,
--- | a natural number less than the upper bound parameter.
-data Fin :: Nat -> * where
-  -- Fin Zero is uninhabited. Fin (Succ Zero) has one inhabitant.
-  FZ :: Fin ('S n)
-  FS :: Fin n -> Fin ('S n)
-
-instance Eq (Fin n) where
-  FZ   == FZ   = True
-  FS n == FS m = n == m
-  _    == _    = False
-
-instance Ord (Fin n) where
-  FZ   `compare` FZ   = EQ
-  FS _ `compare` FZ   = GT
-  FZ   `compare` FS _ = LT
-  FS n `compare` FS m = n `compare` m
-
-toInt :: Fin n -> Int
-toInt FZ     = 0
-toInt (FS n) = 1 + toInt n
-
-instance Show (Fin n) where
-  show = show . toInt
-
-coerceFin :: Fin n -> Fin ('S n)
-coerceFin FZ     = FZ
-coerceFin (FS n) = FS $ coerceFin n
-
-pred :: Fin ('S n) -> Maybe (Fin n)
-pred FZ     = Nothing
-pred (FS n) = Just n
-
--- | Match against an element in `Fin`, removing it from its domain.
-extract :: Fin ('S n) -> Fin ('S n) -> Maybe (Fin n)
-extract n m
-  | n == m = Nothing
-  | n >  m = pred n
-  -- I am convinced it is not possible to prove to the compiler
-  -- that this function is valid without `unsafeCoerce`.
-  | otherwise = Just $ unsafeCoerce n

src/Data/Nat.hs

@@ -1,3 +0,0 @@
-module Data.Nat (Nat (Z, S)) where
-
-data Nat = Z | S Nat

src/Data/Vec.hs

@@ -1,20 +0,0 @@
-{-# LANGUAGE GADTs, TypeOperators, DataKinds #-}
-module Data.Vec (Vec (Empty, (:.)), (!.), elemIndex) where
-
-import Data.Fin (Fin (FZ, FS))
-import Data.Nat (Nat (Z, S))
-
-data Vec n a where
-  Empty :: Vec 'Z a
-  (:.)  :: a -> Vec n a -> Vec ('S n) a
-
-(!.) :: Vec n a -> Fin n -> a
-(x :. _ ) !. FZ     = x
-(_ :. xs) !. (FS n) = xs !. n
-_         !. _      = error "Impossible"
-
-elemIndex :: Eq a => a -> Vec n a -> Maybe (Fin n)
-elemIndex _ Empty = Nothing
-elemIndex x (x' :. xs)
-  | x == x'   = Just FZ
-  | otherwise = FS <$> elemIndex x xs

src/UntypedLambdaCalculus.hs

@@ -1,72 +1,77 @@
-{-# LANGUAGE GADTs, FlexibleInstances, DataKinds #-}
-module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), eval) where
+{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, MultiWayIf #-}
+module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), ReaderAlg, eval, cataReader) where
 
-import Control.Monad.Reader (Reader, runReader, withReader, reader, asks)
-import Data.Fin (Fin (FZ, FS), extract, coerceFin)
+import Control.Monad.Reader (Reader, runReader, local, reader, ask)
+import Data.Bifunctor (bimap)
 import Data.Functor ((<&>))
-import Data.Nat (Nat (S, Z))
-import Data.Vec (Vec (Empty, (:.)), (!.))
+import Data.Functor.Foldable (Base, Recursive, cata)
+import Data.Functor.Foldable.TH (makeBaseFunctor)
 
 -- | A lambda calculus expression where variables are identified
 -- | by their distance from their binding site (De Bruijn indices).
-data Expr n = Free String
-            | Var (Fin n)
-            | Lam String (Expr ('S n))
-            | App (Expr n) (Expr n)
+data Expr = Free String
+          | Var Int
+          | Lam String Expr
+          | App Expr Expr
 
-coerceExpr :: Expr n -> Expr ('S n)
-coerceExpr (Free v)  = Free v
-coerceExpr (Var v)   = Var $ coerceFin v
-coerceExpr (Lam v e) = Lam v $ coerceExpr e
-coerceExpr (App f x) = App (coerceExpr f) (coerceExpr x)
+makeBaseFunctor ''Expr
 
-instance Show (Expr 'Z) where
-  show expr = runReader (show' expr) Empty
-    where show' :: Expr n -> Reader (Vec n String) String
-          show' (Free v)    = return v
-          show' (Var  v)    = reader (\vars -> vars !. v ++ ':' : show v)
-          show' (Lam  v e') = withReader (v :.) (show' e') <&>
-                           \body -> "(\\" ++ v ++ ". " ++ body ++ ")"
-          show' (App f' x') = do
-                             f <- show' f'
-                             x <- show' x'
-                             return $ "(" ++ f ++ " " ++ x ++ ")"
+type Algebra   f   a = f a ->          a
+type ReaderAlg f s a = Algebra f (Reader s a)
+
+cataReader :: Recursive r => ReaderAlg (Base r) s a -> s -> r -> a
+cataReader f initialState x = runReader (cata f x) initialState
+
+instance Show Expr where
+  show = cataReader alg []
+    where alg :: ReaderAlg ExprF [String] String
+          alg (FreeF v) = return v
+          alg (VarF  v) = reader (\vars -> vars !! v ++ ':' : show v)
+          alg (LamF  v e) = do
+            body <- local (v :) e
+            return $ "(\\" ++ v ++ ". " ++ body ++ ")"
+          alg (AppF f' x') = do
+            f <- f'
+            x <- x'
+            return $ "(" ++ f ++ " " ++ x ++ ")"
 
 -- | Determine whether the variable bound by a lambda expression is used in its body.
 -- | This is used in eta reduction, where `(\x. f x)` reduces to `f` when `x` is not bound in `f`.
-unbound :: Expr ('S n) -> Bool
-unbound expr = runReader (unbound' expr) FZ
-  where unbound' :: Expr ('S n) -> Reader (Fin ('S n)) Bool
-        unbound' (Free _)  = return True
-        unbound' (Var v)   = reader (/= v)
-        unbound' (App f x) = (&&) <$> unbound' f <*> unbound' x
-        unbound' (Lam _ e) = withReader FS $ unbound' e
+unbound :: Expr -> Bool
+unbound = cataReader alg 0
+  where alg :: ReaderAlg ExprF Int Bool
+        alg (FreeF _)  = return True
+        alg (VarF  v)  = reader (/= v)
+        alg (AppF f x) = (&&) <$> f <*> x
+        alg (LamF _ e) = local (+ 1) e
 
 -- | When we bind a new variable, we enter a new scope.
 -- | Since variables are identified by their distance from their binder,
 -- | we must increment them to account for the incremented distance,
 -- | thus embedding them into the new expression.
-embed :: Expr n -> Expr ('S n)
-embed   (Var v) = Var $ FS v
-embed o@(Lam _ _) = coerceExpr o
-embed   (Free x) = Free x
-embed   (App f x) = App (embed f) (embed x)
+embed :: Expr -> Expr
+embed (Var v)   = Var $ v + 1
+embed (App f x) = App (embed f) (embed x)
+embed x         = x
 
-subst :: Expr n -> Expr ('S n) -> Expr n
-subst value expr = runReader (subst' value expr) FZ
-  where subst' :: Expr n -> Expr ('S n) -> Reader (Fin ('S n)) (Expr n)
-        subst' _   (Free x)  = return $ Free x
-        subst' val (Var x)   = maybe val Var <$> asks (extract x)
-        subst' val (App f x) = App <$> subst' val f <*> subst' val x
-        subst' val (Lam v e) = Lam v <$> withReader FS (subst' (embed val) e)
+subst :: Expr -> Expr -> Expr
+subst val = cataReader alg (0, val)
+  where alg :: ReaderAlg ExprF (Int, Expr) Expr
+        alg (FreeF x)  = return $ Free x
+        alg (VarF x)   = ask <&> \(x', value) -> if
+          | x == x'   -> value
+          | x >  x'   -> Var $ x - 1
+          | otherwise -> Var x
+        alg (AppF f x) = App <$> f <*> x
+        alg (LamF v e) = Lam v <$> local (bimap (+ 1) embed) e 
 
 -- | Evaluate an expression to normal form.
-eval :: Expr n -> Expr n
+eval :: Expr -> Expr
 eval (App f' x) = case eval f' of
   -- Beta reduction.
   Lam _ e -> eval $ subst x e
   f -> App f (eval x)
-eval o@(Lam _ (App f (Var FZ)))
+eval o@(Lam _ (App f (Var 0)))
   -- Eta reduction. We know that `0` is not bound in `f`,
   -- so we can simply substitute it for undefined.
   | unbound f = eval $ subst undefined f

src/UntypedLambdaCalculus/Parser.hs

@@ -1,58 +1,63 @@
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, DataKinds #-}
 module UntypedLambdaCalculus.Parser (parseExpr) where
 
-import Control.Monad.Reader (ReaderT, runReaderT, withReaderT, mapReaderT, ask)
-import Control.Monad.Trans.Class (lift)
-import Data.List (foldl1')
-import Data.Nat (Nat (Z))
-import Data.Vec (Vec (Empty, (:.)), elemIndex)
-import Text.Parsec (Parsec, SourceName, ParseError, many, sepBy1, letter, alphaNum, char, between, (<|>), spaces, parse)
-import UntypedLambdaCalculus (Expr (Free, Var, Lam, App))
+import Control.Applicative (liftA2)
+import Control.Monad.Reader (local, asks)
+import Data.List (foldl1', elemIndex)
+import Data.Functor.Foldable.TH (makeBaseFunctor)
+import Text.Parsec (SourceName, ParseError, (<|>), many, sepBy1, letter, alphaNum, char, between, spaces, parse)
+import Text.Parsec.String (Parser)
+import UntypedLambdaCalculus (Expr (Free, Var, Lam, App), ReaderAlg, cataReader)
 
-type Parser s a = ReaderT s (Parsec String ()) a
+data Ast = AstVar String
+         | AstLam String Ast
+         | AstApp Ast Ast
+
+makeBaseFunctor ''Ast
 
 -- | A variable name.
-name :: Parsec String () String
-name = do
-  c <- letter
-  cs <- many alphaNum
-  return $ c : cs
+name :: Parser String
+name = liftA2 (:) letter $ many alphaNum
 
 -- | A variable expression.
-var :: Parser (Vec n String) (Expr n)
-var = do
-  varn <- lift name
-  bound <- ask
-  return $ maybe (Free varn) Var $ elemIndex varn bound
+var :: Parser Ast
+var = AstVar <$> name
 
 -- | Run parser between parentheses.
-parens :: Parsec String () a -> Parsec String () a
+parens :: Parser a -> Parser a
 parens = between (char '(') (char ')')
 
 -- | A lambda expression.
-lam :: Parser (Vec n String) (Expr n)
+lam :: Parser Ast
 lam = do
-  (lift $ between (char '\\') (char '.' >> spaces) $ name `sepBy1` spaces) >>= help
-  where help :: [String] -> Parser (Vec n String) (Expr n)
-        help []     = app
-        help (v:vs) = Lam v <$> withReaderT (v :.) (help vs)
+  vars <- between (char '\\') (char '.') $ name `sepBy1` spaces
+  spaces
+  body <- app
+  return $ foldr AstLam body vars
 
 -- | An application expression.
-app :: Parser (Vec n String) (Expr n)
-app = foldl1' App <$> mapReaderT (`sepBy1` spaces) safeExpr
-
-ll :: (Parsec String () a -> Parsec String () b -> Parsec String () c) -> Parser s a -> Parser s b -> Parser s c
-ll f p1 p2 = do
-  bound <- ask
-  lift $ f (runReaderT p1 bound) (runReaderT p2 bound)
+app :: Parser Ast
+app = foldl1' AstApp <$> safeExpr `sepBy1` spaces
 
 -- | An expression, but where applications must be surrounded by parentheses,
 -- | to avoid ambiguity (infinite recursion on `app` in the case where the first
 -- | expression in the application is also an `app`, consuming no input).
-safeExpr :: Parser (Vec n String) (Expr n)
-safeExpr = ll (<|>) var $ ll (<|>) lam $ mapReaderT parens (ll (<|>) lam app)
+safeExpr :: Parser Ast
+safeExpr = var <|> lam <|> parens (lam <|> app)
+
+toExpr :: Ast -> Expr
+toExpr = cataReader alg []
+  where
+    alg :: ReaderAlg AstF [String] Expr
+    alg (AstVarF varName) = do
+      bindingSite <- asks (elemIndex varName)
+      return $ case bindingSite of
+        Just index -> Var index
+        Nothing    -> Free varName
+    alg (AstLamF varName body) = Lam varName <$> local (varName :) body
+    alg (AstAppF f x) = App <$> f <*>x
 
 -- | 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 = parse (runReaderT app Empty) sourceName code
+parseExpr :: SourceName -> String -> Either ParseError Expr
+parseExpr sourceName code = toExpr <$> parse app sourceName code