Meta-circular interpreter for lambda calculus in Haskell

Question

For learning purpose, I've written a simple lambda calculus interpreter (plus 'Add'). I would like it to be the cleanest and most idiomatic possible.

Bonus question: how would you use deriving (Show) for Val, just having to define show for Fun (Val -> Val)?

-- Lambda calculus interpreter example. import qualified Data.Map.Lazy as Map data Val = Num Integer | Fun (Val -> Val) | Wrong data Term = Cons Integer | Var String | Lam String Term | App Term Term | Add Term Term type Env = Map.Map String Val add :: Val -> Val -> Val add (Num x) (Num y) = Num (x+y) add _ _ = Wrong apply :: Val -> Val -> Val apply (Fun f) v = f v apply _ _ = Wrong instance Show Val where show (Num x) = show x show (Fun f) = "function" show Wrong = "Wrong" interp :: Term -> Env -> Val interp (Cons x) e = Num x interp (Var s) e = Map.findWithDefault Wrong s e -- Equivalent to: -- interp (Var s) e = maybe Wrong id (Map.lookup s e) interp (Lam s t) e = Fun (\v -> interp t (Map.insert s v e)) interp (App f t) e = apply (interp f e) (interp t e) interp (Add a b) e = add (interp a e) (interp b e) expr = App (Lam "x" (Add (Var "x") (Var "x"))) (Add (Cons 10) (Cons 11)) res = interp expr Map.empty main = putStrLn (show res) 

Answer 1

I wanted to give a more full answer, but I can't fully commit to it, so here are a few things:

• Instead of having Wrong built into the result type, you would rather want Maybe Val, or better yet, Either String Val or Either Error val, since there are multiple possible causes for failure.

• I'm a little skeptical about Fun (Val -> Val): This seems to serve two purposes:

  1. The final result of interp could be a lambda.

     Theoretically it must always be, but for a practical purpose, perhaps, you've decided that integers are different from functions. And that if one were to return a value that hasn't reduced to an integer, then rather produce a Haskell function that can resume evaluation later.

     The drawback is that you can't further transform the structure hidden away in a Fun (Val -> Val) in the same way as you can with a Term; you can only reduce it further using interp. For example, you can only pretty-print the result if it's an integer, or a failure.

  2. As an intermediate representation of a term being evaluated. But since any lambda reduction rule provides another term, Term should be an excellent intermediate representation.

• When you express an intermediate state as Fun (Val -> Val), it also contains an implicit Env, which is in some sense a reader monad pattern. Typically you might represent this with Control.Monad.Reader instead.

• I think keeping an Env might be neat - I've seen several examples of people building quite advanced lambda calculus interpreters that do this. But when I first thought how I'd make it myself, I thought of

  interp (App (Lam x body) arg) = subst x body arg interp (App (Var x) _arg) = Left ("Free variable " ++ show x) 

  since, if I encountered a Var x on the left-hand side of an application, I'd know that it hadn't been substituted by an outer reduction. But I'm not wise enough to say which is better here, that was just my first thought.

• I'd rename Cons to Num or Int: Cons seems a bit contrived for constant, and Const is a bit vague, since you really mean integer constant. But what constant is there about a lambda term? I mean, theoretically it could also be a function if the interpreter allowed it.

• If your intermediate representation was Term and not Val, and your interpreter was monadic (e.g. for handling errors) you could merge add into apply, since Add is just a special-case function application:

  interp (App (Lam x body) arg) = subst x body arg interp (App (Var x) _arg) = Left ("Free variable " ++ show x) interp (Add e1 e2) = add <$> interp e1 <*> interp e2 add (Int m) (Int n) = return (Int (m + n)) add x y = Left ("Cannot add non-integers " ++ show x ++ " and " ++ show y) 

  Pretty-printing m and n here is possible because Term's structure is not hidden within a Haskell -> function.

• You have two things that could be expressed in terms of monads: Making Env implicit using a reader monad, and handling errors using Either. This could be expressed as

  type Env = Map Var Term type Interpreter = Env -> Term -> Either String Term 

  or rather using Control.Monad.Trans.Reader:

  type Env = Map Var Term type Interpreter a = ReaderT Env (Either String) a 

  which is equivalent under the hood, but it means you can do stuff like:

  interp (Add e1 e2) = add <$> interp e1 <*> interp e2 

I don't care about alpha renaming

I'm not sure how to interpret this, but the following thought comes to mind:

It is idiomatic to model your data type as close to the domain, so the fact that Lam "x" (Var "y") passes type-check but can not evaluate (unless there's some kind of initial environment that catches free variables) is a problem. One way to address this I've seen is e.g. de Bruijn indexing as performed e.g. by James Fisher which is one way to say that he also doesn't care about alpha renaming by never having the need. One could even convert freely between one interpretation with variables and another without, depending on which representation is most convenient for a given purpose.