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!
var == var'
<- Don't you need to substitute even if the names aren't equal?(\x -> x x) y
becomesy y
.\$\endgroup\$eval = expr id abst app sub
.\$\endgroup\$