Skip to content

Instantly share code, notes, and snippets.

@robrix
Created July 17, 2021 15:35
Show Gist options
  • Save robrix/5f85e7d3316ce01eb5a3cbc4418903d2 to your computer and use it in GitHub Desktop.
Save robrix/5f85e7d3316ce01eb5a3cbc4418903d2 to your computer and use it in GitHub Desktop.
A catamorphism-based interpreter and an abstract machine for the untyped lambda calculus
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment