A catamorphism-based interpreter and an abstract machine for the untyped lambda calculus

LC.hs

type Name = String

-- first-order syntax
data Tm
  = Var Name
  | Abs Name Tm
  | App Tm Tm
  deriving (Eq, Ord, Show)

type Env = [(Name, Val)]

-- values are higher-order abstract syntax. easy to interpret, hard to parse into or pretty-print ^_^;;
newtype Val = Closure { runClosure :: Val -> Maybe Val }

-- naïve interpreter
eval :: Env -> Tm -> Maybe Val
eval env (Var n)   = lookup n env
eval env (Abs n b) = pure $ Closure (\ v -> eval ((n, v) : env) b)
eval env (App f a) = join (runClosure <$> eval env f <*> eval env a)


-- expression functor, to eval as a catamorphism
data TmF a
  = VarF Name
  | AbsF Name a
  | AppF a a
  deriving (Eq, Functor, Ord, Show)

-- interpreter will evaluate expressions to /functions from env to values/, instead of to values directly
-- looks a teensy bit like denotational semantics if you squint
type Carrier = Env -> Maybe Val

-- quite similar to eval (above), but with no recursive calls
evalg :: TmF Carrier -> Carrier
evalg exp env = case exp of
  VarF n   -> lookup n env
  AbsF n b -> pure (Closure (\ v -> b ((n, v) : env)))
  AppF f a -> join (runClosure <$> f env <*> a env)

-- standard Fix/cata machinery
newtype Fix f = In { out :: f (Fix f) }

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = go where go = alg . fmap go  . out

-- putting it all together
evalCata :: Env -> Fix TmF -> Maybe Val
evalCata = flip (cata evalg)


-- this is a CK machine instead of a CEK machine cos I wasn’t sure how to work the env into the Clowns/Jokers–style approach
type Stack = [Frame]


-- the rest of this is pretty much the machine from the first page of /Clowns to the Left of Me, Jokers to the Right/ adapted to the untyped lambda calculus. I haven’t tried defining this interpreter as a catamorphism, mostly because of how it’s factored, and because tempus fugit.
data Frame
  = AppL Tm
  | AppR Val
  | AbsB

eval' :: Env -> Tm -> Maybe Val
eval' env e = load env e []

load :: Env -> Tm -> Stack -> Maybe Val
load env (Var n)   stk = lookup n env >>= \ v -> unload env v stk
load env (Abs n b) stk = unload env (Closure (\ v -> load ((n, v) : env) b stk)) (AbsB : stk)
load env (App a b) stk = load env a (AppL b : stk)

unload :: Env -> Val -> Stack -> Maybe Val
unload _   v []             = pure v
unload env f (AppL a : stk) = load env a (AppR f : stk)
unload env a (AppR f : stk) = runClosure f a >>= \ v -> unload env v stk
unload env c (AbsB   : stk) = unload env c stk