Skip to content

Instantly share code, notes, and snippets.

@darkf

darkf/lc.hs

Created Mar 5, 2014
Embed
What would you like to do?
Simply typed lambda calculus interpreter in Haskell
import Data.Maybe (fromJust)
data Type = IntTy
| ArrowTy Type Type
deriving (Show, Eq)
data Term = Const Int
| Var String
| Abs String Type Term
| App Term Term
deriving (Show, Eq)
typeof :: [(String, Type)] -> Term -> Type
typeof _ Const{} = IntTy
typeof e (Var x) = fromJust (lookup x e)
typeof e (Abs arg ty t) = ArrowTy ty (typeof ((arg, ty):e) t)
typeof e (App t arg) =
let ArrowTy ty ret = typeof e t in
if typeof e arg /= ty then
error "argument type mismatch"
else ret
substitute :: String -> Term -> Term -> Term
substitute v x (Var v') | v' == v = x
substitute v x (Abs arg ty t) = Abs arg ty (substitute v x t)
substitute v x (App t arg) = App (substitute v x t) arg
substitute _ _ t = t
eval :: [(String, Term)] -> Term -> Term
eval _ (Const x) = Const x
eval _ x@Abs{} = x
eval e (Var x) = Const (let Const v = fromJust (lookup x e) in v)
eval e (App (Abs arg _ t) x) = substitute arg x t
eval e (App t x) = eval e (App (eval e t) x)
main = do
let i = Abs "x" IntTy (Var "x")
let programI = App i (Const 42)
print $ typeof [] i
print $ typeof [] programI
print $ typeof [] programI
print $ eval [] programI
putStrLn "-- K --"
-- \x.\y.x
let k = Abs "x" IntTy $ Abs "y" IntTy (Var "x")
-- (k 1337) 12
let programK = App (App k (Const 42)) (Const 12)
print $ typeof [] k
print $ typeof [] programK
print $ eval [] programK
print $ eval [] $ App (App k k) k
putStrLn "-- S --"
-- \x.\y.\z. xz (yz)
-- note: types are dummies, because lazy. let's assume we're untyped :D
let s = Abs "x" IntTy $ Abs "y" IntTy $ Abs "z" IntTy $
App (App (Var "x") (Var "z")) (App (Var "y") (Var "z"))
let kksk = App (App s k) (App s k)
let programS = App (App k k) (App s k)
print $ eval [] programS
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment