CEK-style lambda calculus interpreter.

CEK.hs

{-# LANGUAGE GADTs #-}

-- http://matt.might.net/articles/cek-machines
-- https://www.cs.ru.nl/~freek/courses/tt-2011/papers/parigot.pdf

module CEK where

import Data.Void

data Expr a
    = Var a
    | Lam (Expr (Maybe a))
    | App (Expr a) (Expr a)
    deriving Show

data Value where
    Closure :: Show a => Expr (Maybe a) -> Env a -> Value

type Env a = a -> Value

data Kont where
    Top :: Kont
    Arg :: Show a => Expr a -> Env a -> Kont -> Kont
    Fun :: Show a => Expr (Maybe a) -> Env a -> Kont -> Kont

data State where
    State :: Show a => Expr a -> Env a -> Kont -> State

instance Show State where
    show (State c e k) = show c

start :: Expr Void -> State
start c = State c absurd Top

step :: State -> State
step s@(State c e k) = case c of
    Var v -> case e v of
        Closure c e -> State (Lam c) e k
    Lam c -> case k of
        Top -> s
        Arg c' e' k' -> State c' e' (Fun c e k')
        Fun c' e' k' -> State c' (maybe (Closure c e) e') k'
    App c c' -> State c e (Arg c' e k)

final :: State -> Bool
final (State (Lam c) e Top) = True
final _                     = False

eval :: State -> State
eval = until final step

s :: Expr Void
s = Lam (Lam (Lam (App (App (Var (Just (Just Nothing))) (Var Nothing)) (App (Var (Just Nothing)) (Var Nothing)))))

k :: Expr Void
k = Lam (Lam (Var (Just Nothing)))

-- eval . start $ App (App (App s k) k) k