Simple CEK-style lambda calculus interpreter.

Lambda.hs

module Lambda where

-- https://www.youtube.com/watch?v=O0TgP7GKkSY
-- https://gist.github.com/pedrominicz/127ab01cec689cc3d69f32e6c4f758bb

data Term
  = App Term Term
  | Lam Term
  | Var Int
  deriving (Eq, Show)

shift :: Term -> Term
shift = go 0
  where
  go k (App m n) = App (go k m) (go k n)
  go k (Lam m) = Lam (go (k + 1) m)
  go k (Var x) = if x < k then Var x else Var (x + 1)

subst :: Term -> Term -> Term
subst = go 0
  where
  go k l (App m n) = App (go k l m) (go k l n)
  go k l (Lam m) = Lam (go (k + 1) (shift l) m)
  go k l (Var x) =
    case compare x k of
      LT -> Var x
      EQ -> l
      GT -> Var (x - 1)

data Stack
  = Top
  | Arg Term Stack
  | Fun Term Stack
  deriving Show

type State = (Term, Stack)

-- https://hackage.haskell.org/package/zippers-0.3.1/docs/src/Control.Zipper.Internal.html#farthest
farthest :: (a -> Maybe a) -> a -> a
farthest f = go
  where
  go a = maybe a go (f a)

step :: State -> Maybe State
step (App m n, s) = Just (m, Arg n s)
step (Lam m, Arg n s) = Just (subst n m, s)
step _ = Nothing

eval :: Term -> Term
eval m = fst $ farthest step (m, Top)

step' :: State -> Maybe State
step' (App m n, s) = Just (m, Arg n s)
step' (Lam m, Arg n s) = Just (n, Fun m s)
step' (Lam m, Fun n s) = Just (subst (Lam m) n, s)
step' _ = Nothing

eval' :: Term -> Term
eval' m = fst $ farthest step' (m, Top)

s, k :: Term
s = Lam (Lam (Lam (App (App (Var 2) (Var 0)) (App (Var 1) (Var 0)))))
k = Lam (Lam (Var 1))

omega :: Term
omega = App (Lam (App (Var 0) (Var 0))) (Lam (App (Var 0) (Var 0)))

-- https://cs.stackexchange.com/questions/101670/lambda-calculus-call-by-name-and-call-by-value-reduction
d, p :: Term
d = Lam (Lam (Var 0))
p = Lam (Lam (App (App (Var 1) (Var 0)) (Var 1)))

test :: Term
test = App (App p k) d

-- λ> eval (App (App s k) k)
-- Lam (App (App (Lam (Lam (Var 1))) (Var 0)) (App (Lam (Lam (Var 1))) (Var 0)))
-- λ> eval (App (App (App s k) k) (Var 0))
-- Var 0