3
\$\begingroup\$

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!

\$\endgroup\$
3
  • \$\begingroup\$var == var' <- Don't you need to substitute even if the names aren't equal? (\x -> x x) y becomes y y.\$\endgroup\$CommentedAug 27, 2016 at 15:03
  • \$\begingroup\$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.\$\endgroup\$CommentedAug 27, 2016 at 16:16
  • \$\begingroup\$You may be interested in the catamorphism package which allows you to write eval = expr id abst app sub.\$\endgroup\$CommentedAug 27, 2016 at 23:52

0

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.