Difference between call-by-value and call-by-name interpreter for the lambda calculus

Question

In another question, Bob presented the following interpreter for the untyped lambda calculus.

data Expr = Var String | Lam String Expr | App Expr Expr

data Value a = V a | F (Value a -> Value a)

interpret :: [(String, Value a)] -> Expr -> Value a
interpret env (Var x) = case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> v
interpret env (Lam x e) = F (\v -> interpret ((x, v):env) e)
interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> f (interpret env e2)

Ivan Zakharyaschev remarked that this interpreter is call-by-value due to F f -> f (interpret env e2). How would the implementation of a call-by-name interpreter be different from the one presented above?

Plotkin studied call-by-name and call-by-value strategies for evaluating the lambda calculus in the 1970s.

Answer 1

I don't think proper call-by-name is possible with the original data definition. F (Value a -> Value a) has Value a as argument, so we have no choice but to pass in some already interpreted value, and it'll be call-by-need under Haskell reduction behaviour.

We could modify the data definition:

data Value a = V a | F ((() -> Value a) -> Value a)

And also have the interpreter return explicit thunks:

interpret :: [(String, () -> Value a)] -> Expr -> () -> Value a
interpret env (Var x) = delay (case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> force v)
interpret env (Lam x e) = delay (F (\v -> force (interpret ((x, v):env) e)))
interpret env (App e1 e2) = delay (case force (interpret env e1) of
  V _ -> error "not a function"
  F f -> f (interpret env e2))

force :: (() -> a) -> a
force f = f ()
{-# NOINLINE force #-}

delay :: a -> () -> a
delay a () = a
{-# NOINLINE delay #-}

Now, instead of storing a thunk in the environment, we store a partial application object, and then evaluate it separately at different call sites.

force and delay are required to prevent GHC from floating out function bodies, thereby recovering sharing. Alternatively, one could compile with {-# OPTIONS -fno-full-laziness #-} and use simple lambdas and applications instead instead of the above machinery.