型推論機にlet式とパーサーを追加してみましたですー＞ω＜　適当遊んでみてくださいですー＞ω＜

tinf2.hs

{-# Language TemplateHaskell, QuasiQuotes, FlexibleContexts #-}
import Text.Peggy hiding (Expr, space)
import Control.Monad.State

type Name = String
data Type =
  TInt|
  TBool|
  TVar Name|
  TFun Type Type deriving (Show, Eq)
data Expr =
  EInt Integer|
  EBool Bool|
  EIf Expr Expr Expr|
  EVar Name|
  EFun Name Expr|
  EApp Expr Expr|
  ELet Name Expr Expr deriving (Show)
type TyEnv = [(String, Type)]
type TySubst = [(Name, Type)]

unify :: [(Type, Type)] -> Maybe TySubst
unify eqs = solve eqs []
  where
  solve [] th = Just th
  solve ((t1,t2):eqs) th
   |t1 == t2 = solve eqs th
   |otherwise = case (t1, t2) of
     (TFun t11 t12, TFun t21 t22) -> solve ((t11, t21):(t12, t22):eqs) th
     (TVar s, _)
      |occurs t1 t2 -> Nothing
      |otherwise -> solve (substEq [(s, t2)] eqs) (composeSubst [(s, t2)] th)
     (_, TVar s)
      |occurs t2 t1 -> Nothing
      |otherwise -> solve (substEq [(s, t1)] eqs) (composeSubst [(s, t1)] th)
     (_, _) -> Nothing

occurs :: Type -> Type -> Bool
occurs t1 (TFun t21 t22) = occurs t1 t21 || occurs t1 t22
occurs t1 t2 = t1 == t2

substTy :: TySubst -> Type -> Type
substTy _ TInt = TInt
substTy _ TBool = TBool
substTy st (TVar s) = f st s
  where
  f [] s' = TVar s'
  f ((s, t):st) s'
   |s == s' = t
   |otherwise = f st s'
substTy st (TFun t1 t2) = TFun (substTy st t1) (substTy st t2)

substEq :: TySubst -> [(Type, Type)] -> [(Type, Type)]
substEq st eqs = map (\(t1, t2)-> (substTy st t1, substTy st t2)) eqs

substTyEnv :: TySubst -> TyEnv -> TyEnv
substTyEnv st env = map (\(s, t) -> (s, substTy st t)) env

composeSubst :: TySubst -> TySubst -> TySubst
composeSubst st2 st1 = foldl (\st (s, t) -> case lookup s st of
  Just _ -> st
  Nothing -> (s, t):st) st2' st1
  where
  st2' = map (\(s, t) -> (s, substTy st1 t)) st2

newTVar :: StateT Int Maybe Type
newTVar = do
  n <- get
  put (n+1)
  return (TVar $ "'t" ++ show n)

tinf' :: TyEnv -> Expr -> StateT Int Maybe (TyEnv, Type, TySubst)
tinf' env (EInt _) = return (env, TInt, [])
tinf' env (EBool _) = return (env, TBool, [])
tinf' env (EVar s) = case lookup s env of
  Just t -> return (env, t, [])
  Nothing -> do
    tv <- newTVar
    return ((s, tv):env, tv, [])
tinf' env (EFun s e) = do
  tv <- newTVar
  let env' = (s, tv):env
  (env'', t, th) <- tinf' env' e
  let tv' = substTy th tv
  return (filter ((/=) s . fst) env'', TFun tv' t, th)
tinf' env (EApp e1 e2) = do
  (env', t1, th1) <- tinf' env e1
  (env'', t2, th2) <- tinf' env' e2
  t3 <- newTVar
  let t11 = substTy th2 t1
  th3 <- lift $ unify [(t11, TFun t2 t3)]
  let t3' = substTy th3 t3
  let env''' = substTyEnv th3 env''
  return (env''', t3', th3 +*+ th2 +*+ th1)
  where
  (+*+) = composeSubst
tinf' env (EIf c e1 e2) = do
  (env', tc, thc) <- tinf' env c
  thc' <- lift $ unify [(tc, TBool)]
  let env'' = substTyEnv thc' env'
  tv1 <- newTVar
  (env1, t1, th1) <- tinf' env'' e1
  (env2, t2, th2) <- tinf' env1 e2
  th3 <- lift $ unify [(tv1, t1),(tv1, t2)]
  let env2' = substTyEnv th3 env2
  let tv1' = substTy th3 tv1
  return (env2', tv1', th3 +*+ th2 +*+ thc')
  where
  (+*+) = composeSubst
tinf' env (ELet s e1 e2) = do
  (env', t1, th1) <- tinf' env e1
  let env'' = (s, t1):env'
  (env'', t2, th2) <- tinf' env'' e2
  return (env'', t2, composeSubst th2 th1)

tinf e = evalStateT (tinf' [] e) 0

[peggy|
space :: ()
 = [ \t\r] { () }

top :: Expr
  = expr !.

expr :: Expr
  = letExpr / funExpr / ifExpr / appExpr

letExpr :: Expr
  = "let" name "=" expr "in" expr { ELet $1 $2 $3 }

funExpr :: Expr
  = "fun" name "->" expr { EFun $1 $2 }
ifExpr :: Expr
  = "if" expr "then" expr "else" expr { EIf $1 $2 $3 }

appExpr :: Expr
  = appExpr value { EApp $1 $2}
  / value { $1 }

value :: Expr
  = "(" expr ")"
  / intValue { EInt $1 }
  / boolValue { EBool $1 }
  / name { EVar $1 }

intValue ::: Integer
  = [1-9] [0-9]* { read ($1 : $2) }

boolValue ::: Bool
  = "True" { True }
  / "False" { False }

name ::: String
  = !"fun" !"in" !"let" !"if" !"then" !"else" [a-z_] [a-zA-Z0-9]* { $1 : $2 }
|]

parseWith str = case parseString top "<parse>" str of
  Right expr -> tinf expr
  Left _ -> Nothing