Lameda Calculus evaluator

August 24, 2017

data Exp = Var Char
         | App Exp Exp
         | Lam Char Exp

instance Show Exp where
  show (Var c) = [c]
  show (App e1 e2) = "(" ++ (show e1) ++ " " ++ (show e2) ++ ")"
  show (Lam c e) = "(λ " ++ [c] ++ ". " ++ (show e) ++ ")"

substitute :: Char -> Exp -> Exp -> Exp
substitute param (Var c) arg
  | param == c = arg
  | otherwise = Var c
substitute param (App e1 e2) arg =
  App (substitute param e1 arg) (substitute param e2 arg)
substitute param (Lam ca ea) arg
  | param == ca = ea
  | otherwise = Lam ca (substitute param ea arg)


reduce :: Exp -> Exp
reduce (App (Lam c e1) e2) = reduce $ substitute c e1 e2
reduce (App e1 e2) = reduce $ App (reduce e1) e2
reduce (Lam c e) = Lam c (reduce e)
reduce (Var c) = Var c

main :: IO ()
main = do
  print $ reduce $ App (Lam 'x' (Var 'x'))
                       (Var 'y')
  print $ reduce $ App (Lam 'x' (Var 'x'))
                       (Lam 'y' (Lam 'z' (Var 'z')))
  print $ reduce $ App (App (Lam 'x' (Lam 'y' (Var 'x')))
                            (Lam 'a' (Var 'a'))
                       )
                       (App (Lam 'x' (App (Var 'x')
                                          (Var 'x')
                                     )
                            )
                            (Lam 'x' (App (Var 'x')
                                          (Var 'x')
                                     )
                            )
                       ) 

Demo

$ curl -s https://earldouglas.com/posts/lameda.md | codedown haskell | runhaskell
y
(λ y. (λ z. z))
(λ a. a)