型推論ですー＞ω＜ 主にhttp://logic.cs.tsukuba.ac.jp/~kam/jikken/index.htmlを参考にさせていただきましたですー＞ω＜

tinf.hs

import Control.Monad.State

type Name = String
data Type =
  TInt|
  TBool|
  TVar Name|
  TFun Type Type deriving (Show, Eq)
data Expr =
  EInt Int|
  EBool Bool|
  EIf Expr Expr Expr|
  EVar Name|
  EFun Name Expr|
  EApp Expr Expr
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 e = evalStateT (tinf' [] e) 0