Lambda calculus interpreter in Haskell

Question

This code is a representation of lambda calculus using an AST instead of text.

-- beta
-- (App (Abst var body) env) -> (Sub body var env)
-- eta
-- (Abst var (App body var')) -> body
-- alpha
-- (Sub (Var var) var env) -> env
-- (Sub (Var var') var env) -> (Var var')
-- (Sub (Abst var body) var env) -> (Abst var body)
-- (Sub (Abst var' body) var env) -> (Abst var' (Sub body var env))
-- (Sub (App a b) var env) -> (App (Sub a var env) (Sub b var env))

My goal is to represent the transformation rules listed here accurately and explicitly. This code is slower than many other interpreters, and if there is a way to make the code more efficient while still conveying the reduction rules clearly, that would be an improvement.

module Eval where
import Data.Maybe
import Data.Tuple
import Data.List
data Expr a
 = Var a
 | Abst a (Expr a)
 | App (Expr a) (Expr a)
 | Sub (Expr a) a (Expr a)
deriving (Eq, Show)
app :: (Eq a) => Expr a -> Expr a
app (App (Abst var body) env) = (Sub body var env)
app a = a
abst :: (Eq a) => Expr a -> Expr a
abst (Abst var (App body (Var var')))
 | var == var' = body
abst a = a
sub :: (Eq a) => Expr a -> Expr a
sub (Sub (Var var') var env)
 | var == var' = env
 | otherwise = (Var var')
sub (Sub (Abst var' body) var env)
 | var == var' = (Abst var body)
 | otherwise = (Abst var' (Sub body var env))
sub (Sub (App a b) var env) = (App (Sub a var env) (Sub b var env))
sub a = a
eval :: (Eq a) => Expr a -> Expr a
eval expr@(Var _) = expr
eval expr@(Abst a b) = abst (Abst a (eval b))
eval expr@(App a b) = app (App (eval a) (eval b))
eval expr@(Sub a b c) = sub (Sub (eval a) b (eval c))
evalWhile :: (Eq a) => Expr a -> Expr a
evalWhile a
 | a == b = a
 | otherwise = evalWhile b
where b = eval a

Here are a few applicative combinators for debugging.

s, k, i :: Expr String
i = Abst "x" (Var "x")
k = Abst "x" (Abst "y" (Var "x"))
s = Abst "x" (Abst "y" (Abst "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))

For instance:

λ> evalWhile (App (App (App s k) k) k)
Abst "x" (Abst "y" (Var "x"))

The eval function feels particularly awkward to me, as every type in Expr is preceded by it's equivalent function. Perhaps there is a better way to do this. The evalWhile function also seems like a poor way to check if we've reached normal form, though I have seen other code that does this. With memoization this might not be so bad.

I appreciate any feedback!

• Gurkenglas: var == var' <- Don't you need to substitute even if the names aren't equal? (\x -> x x) y becomes y y.
• stephenwebber: The step you are referring to is beta reduction (\x -> x x) y -> (x x)[x := y], while the var == var' check is part of alpha reduction. For example, ((\x -> y y) z) still reduces to (y y), because x /= y. Beta reduction can also be thought of as "let" introduction.
• Gurkenglas: You may be interested in the catamorphism package which allows you to write eval = expr id abst app sub.