NbE for untyped lambda calculus is very similar to eval-apply environment machine evaluation

EvalApplyNBE.hs

{-# language LambdaCase #-}

import Data.String
import Data.HashMap.Lazy (HashMap, (!))
import qualified Data.HashMap.Lazy as M

data Term = Var !String | !Term :$ !Term | Lam !String !Term deriving (Show)

instance IsString Term where
  fromString = Var . fromString
infixl 8 :$


-- NBE
--------------------------------------------------------------------------------

data Val = VVar !String | VApp !Val Val | VLam !String (Val -> Val)

eval :: HashMap String Val -> Term -> Val
eval e = \case
  Var v  -> e ! v
  f :$ x -> case (eval e f, eval e x) of
    (VLam v t, x) -> t x
    (f       , x) -> VApp f x
  Lam v t -> VLam v $ \val -> eval (M.insert v val e) t

quote :: Val -> Term
quote = \case
  VVar v   -> Var v
  VApp f x -> quote f :$ quote x
  VLam v f -> Lam v (quote (f (VVar v)))

nf :: Term -> Term
nf = quote . eval M.empty


-- Eval-apply environment machine
--------------------------------------------------------------------------------

type Env  = HashMap String Whnf
data Whnf = WVar !String | WApp !Whnf Whnf | WLam !String !Env !Term

eval' :: Env -> Term -> Whnf
eval' e = \case
  Var v  -> e ! v
  f :$ x -> case (eval' e f, eval' e x) of
    (WLam v e' t, x) -> eval' (M.insert v x e') t
    (f          , x) -> WApp f x
  Lam v t -> WLam v e t
    
quote' :: Whnf -> Term
quote' = \case
  WVar v     -> Var v
  WApp f x   -> quote' f :$ quote' x
  WLam v e t -> Lam v (quote' $ eval' (M.insert v (WVar v) e) t)

nf' :: Term -> Term
nf' = quote' . eval' M.empty