Simply typed lambda calculus interpreter in Haskell

lc.hs

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