I will present a Lambda Calculus interpreter in this post. It is an (almost) exact translation from the ML code in chapter 9 of ML for the Working Programmer by Lawrence C. Paulson. This program incorporates a parser to convert string to an internal represenation of lambda expression, a pretty printer to reconvert the internal represenation to a formatted string in a human-readable form, and two evaluation functions (lazy and strict respectively) to reduce a given lambda expression to its normal form.

Enjoy.

module Lci (

Lambda

,reader -- String -> Lambda

,pr -- Lambda -> String

,byValue -- Lambda -> Lambda

,byName -- Lambda -> Lambda

,evalV -- String -> Lambda

,evalN -- String -> Lambda

,tryV -- String -> IO ()

,tryN -- String -> IO ()

) where

-- Parser

import Text.ParserCombinators.Parsec

import qualified Text.ParserCombinators.Parsec.Token as T

import Text.ParserCombinators.Parsec.Language (emptyDef)

-- Pretty Printing

import qualified Text.PrettyPrint as PP

import Text.PrettyPrint (Doc, (<>), (<+>))

-- Environment

import qualified Data.Map as Map

import Data.Maybe

-------------------

-- Data

-------------------

data Lambda = Free String

| Bound Int

| Abs String Lambda

| App Lambda Lambda

deriving (Eq, Show, Read)

type Env = Map.Map String Lambda

-------------------

-- Parser

-------------------

abstract :: Int -> String -> Lambda -> Lambda

abstract i s (Free s') | s == s' = Bound i

| otherwise = Free s'

abstract _ _ (Bound i) = Bound i

abstract i s (Abs s' t) = Abs s' (abstract (i+1) s t)

abstract i s (App t1 t2) = App (abstract i s t1) (abstract i s t2)

-- Abstraction over several free variables

absList :: [String] -> Lambda -> Lambda

absList xs t = foldr (\x acc -> Abs x (abstract 0 x acc)) t xs

-- Application of t to several terms

appList :: Lambda -> [Lambda] -> Lambda

appList = foldl (\acc x -> App acc x)

-- Shift a term's non-local indices by i

shift :: Int -> Int -> Lambda -> Lambda

shift 0 _ u = u

shift i d u@(Free s) = u

shift i d u@(Bound j) = if j >= d then Bound (j+i) else Bound j

shift i d (Abs s t) = Abs s (shift i (d+1) t)

shift i d (App t1 t2) = App (shift i d t1) (shift i d t2)

-- Substitution for bound variable

subst :: Int -> Lambda -> Lambda -> Lambda

subst _ _ t@(Free _) = t

subst i u t@(Bound i') | i' <>

| i' == i = shift i 0 u

| otherwise = Bound (i' - 1) -- non-local to t

subst i u (Abs s t') = Abs s (subst (i+1) u t')

subst i u (App t1 t2) = App (subst i u t1) (subst i u t2)

-- Lexer & Parser

lexer :: T.TokenParser ()

lexer = T.makeTokenParser emptyDef

whiteSpace= T.whiteSpace lexer

lexeme = T.lexeme lexer

symbol = T.symbol lexer

parens = T.parens lexer

identifier= T.identifier lexer

p_term :: Parser Lambda

p_term = do{ symbol "^"

; ids <- many1 identifier

; symbol "."

; t <- p_term

; return $ absList ids t

}

<|> do{ t <- p_atom

; ts <- many p_atom

; return $ appList t ts

}

p_atom :: Parser Lambda

p_atom = do{ s <- identifier

; return $ Free s

}

<|> parens p_term

p_top :: Parser Lambda

p_top = do{ whiteSpace

; t <- p_term

; eof

; return t

}

reader :: String -> Lambda

reader input = case (parse p_top "" input) of

Left err -> error $ show err

Right x -> x

-------------------

-- Pretty Printing

-------------------

-- Free variables in a term

vars :: Lambda -> [String]

vars (Free s) = [s]

vars (Bound _) = []

vars (Abs s t) = vars t

vars (App t u) = vars t ++ vars u

-- Rename variable "a" to avoid clashes

rename bs a = if a `elem` bs then rename bs (a ++ "'") else a

-- Remove leading lambdas, return bound variable names

stripAbs t = strip [] t

where strip bs (Abs s t) =

let b = rename (vars t) s

in strip (b:bs) (subst 0 (Free b) t)

strip bs u = (reverse bs, u)

pr_term :: Lambda -> Doc

pr_term (Free s) = PP.text s

pr_term (Bound i) = PP.text "??UNMATCHED INDEX??"

pr_term t@(Abs _ _) =

let (b:bs, u) = stripAbs t

spaceJoin b z = " " ++ b ++ z

binder = "^" ++ b ++ (foldr spaceJoin ". " bs)

in PP.sep [PP.text binder, pr_term u]

pr_term t = PP.sep (pr_app t)

pr_app (App t u) = pr_app t ++ [PP.nest 1 (pr_atom u)]

pr_app t = [pr_atom t]

pr_atom (Free s) = PP.text s

pr_atom t = PP.nest 1 $ PP.parens $ pr_term t

pr :: Lambda -> String

pr = PP.render . pr_term

-------------------

-- Reduction

-------------------

eval (App t1 t2) =

case eval t1 of

(Abs a u) -> eval (subst 0 (eval t2) u)

t -> App t (eval t2)

eval t = t

byValue :: Lambda -> Lambda

byValue t = bodies (eval t)

where bodies (Abs a t) = Abs a (byValue t)

bodies (App t u) = App (bodies t) (bodies u)

bodies t = t

headNF (Abs a t) = Abs a (headNF t)

headNF (App t u) =

case headNF t of

(Abs a t') -> headNF (subst 0 u t')

u' -> App u' u

headNF t = t

byName :: Lambda -> Lambda

byName = args . headNF

where args (Abs a t) = Abs a (args t)

args (App t u) = App (args t) (byName u)

args t = t

-----------------------------------------

-- Standard Environment (Lambda Prelude)

-----------------------------------------

-- Substitution for free variables from environment

inst :: Env -> Lambda -> Lambda

inst env t@(Free s) = fromMaybe t (Map.lookup s env)

inst env t@(Bound i) = t

inst env (Abs s t') = Abs s (inst env t')

inst env (App t1 t2) = App (inst env t1) (inst env t2)

insertEnv :: Env -> (String, String) -> Env

insertEnv env (a, s) = Map.insert a (reader s) env

stdEnv = foldl insertEnv Map.empty [

-- booleans

("true", "^x y. x"), ("false", "^x y. y")

,("if", "^p x y. p x y")

-- pairs

,("pair", "^x y f. f x y")

,("fst", "^p. p true"), ("snd", "^p. p false")

]

-------------------

-- Evaluators

-------------------

evalWith :: (Lambda -> Lambda) -> Env -> String -> Lambda

evalWith fn env = fn . inst env . reader

evalV = evalWith byValue stdEnv

evalN = evalWith byName stdEnv

tryV = putStrLn . pr . evalV

tryN = putStrLn . pr . evalN