Implementing a correct `let rec in` interpreter in Haskell with `eval` and `sub` semantics

Question

I'm implementing the toy fb-lang from the principles of programming language book. It's a small interpreted language that uses eval(uate) expression function and sub(stitute) variable with value function to process expressions.

The most challenging construct is the let rec in construct which makes it possible to define and interpret recursive functions. And this is where my implementation is failing.

The operation semantics for the recursive function (from the book) are as follows -

$$ \frac{\left.e_{2} \text { [Function } x \rightarrow e_{1}\left[\left(\text { Function } x->\text { Let } \operatorname{Rec} f x=e_{1} \operatorname{In} f x\right) / f\right] / f\right] \Rightarrow v}{\text { Let } \operatorname{Rec} f x=e_{1} \operatorname{In} e_{2} \Rightarrow v} $$

The logic as far as I've understood is to unroll one layer of the recursion, wrap it in a function and substitute where the recursive call was being made. You might want to take a look at pg 17 - Substitution and pg 21 - Operational Semantics from the linked book to get more context.

I have a recursive summation function as defined below. For some reason, that I've failed to debug, the subtract operation is not being performed, because of which the termination condition is never being hit.

f(x) = if x == 0 then 1 else x + f(x - 1)

The code is at Main.hs, the relevant function are eval, sub and the recursive expression is sumToNExample. Relevant snippets given below.

sub :: Ident -> Expr -> Expr -> Expr
sub var@(Ident x) new e = case e of
      EApp ex ex' -> case ex of
        (EVal (VFunc x ex)) ->
          if x == var
            then -- if the function parameter is substituted
            -- the function body is now a closed expression
            -- and the function call can replaced by it's body
              sub var new ex
            else -- substitute variables in the function body and the
            -- expression being applied to the function
              EApp (EVal $ VFunc x (sub var new ex)) (sub var new ex')
        -- substitute variables in both expressions
        _ -> EApp (sub var new ex) (sub var new ex')
      ELetRecIn f x ex ex' ->
        if x == var
          then -- if variable is same as variable of let rec in
          -- then do not substitute it in expression body
          -- because they are bound to the parameter and
          -- are not free variables
            ELetRecIn f x ex (sub var new ex')
          else ELetRecIn f x (sub var new ex) (sub var new ex')


eval :: Expr -> Value
eval ex = case ex of
  ELetRecIn f x ex ex' ->
    let unroll = sub f (EVal $ VFunc x (ELetRecIn f x ex (EApp (EVal $ VVar f) (EVal $ VVar x)))) ex
    newFunc = EVal $ VFunc x unroll
        nextCall = sub f newFunc ex'
     in eval nextCall

This is not an assignment, I'm just self-learning. I've spent hours of head-scratching. So any help with where I might have gone wrong, or any tooling suggestions that make it easy to walk through each step of eval function will be helpful.

Answer 1

Your definition of substitution is doing too much work for EApp.

(a b)[e/x] = a[e/x] b[e/x]

sub x e (EApp a b) = EApp (sub x e a) (sub x e b)

For substitution the only interesting cases should be variables and binders. EApp is neither, so apply sub to its fields and reconstruct the term, without any additional matching, let recursion handle that.