型推論器の実装① Hindley-Milner型システム
Damas-Milner 型システム
Damas-Milner 型システムとは、型の注釈を必要とせずに多相型を推論する、ラムダ計算の型システムである。ブログタイトルでは、より一般的に使われる Hindley-Milner という名称を用いたが、本稿では Damas-Milner の名称を用いたい。というのも、本稿では Robin Milner と Luis Damas による "Principal type-schemes for functional programs" で示されたアルゴリズムを直接実装するからである。
続き
1. 言語（The language）
項（Term）
通常多相ラムダ計算では、ラムダ抽象に型がついたり、型適用、型抽象が構文に必要となるが、Damas-Milner 型システムでは多相性を一階に限定しているためにそれらを省略できる。
この構文を Haskell プログラムに直すとすれば、以下のようになるだろう（基本型も扱えるようにリテラルを構文に追加したが、型システム全体に及ぼす影響はほとんど無い）。論文では「式（expression）」と呼んでいるが、個人的な好みで、ここでは「項（term）」と呼ぶことにする。
type Name = String
data Term
= TmLit Lit
| TmVar Name
| TmApp Term Term
| TmAbs Name Term
| TmLet Name Term Term
deriving (Eq, Show)
newtype Lit = LUnit deriving (Eq, Show)
型（Type）
厳密な意味での、一階の多相型と型スキームの違いは、型スキームが量化された型変数が全て先頭にあるのに対して、一階の多相型は式中で量化されても良い点である。
例えば以下の型は一階の多相型ではあるが、型スキームではない。
ただ結局このような型も量化子を先頭に持ってきて、型スキームに還元できるので、型スキームだけを考えれば良い。よって実装上は、量化された型変数全てをリストとして扱って、
data Type
= TyVar Uniq
| TyCon TyCon
| TyFun Tau Tau
| TyAll [Uniq] Tau
deriving (Eq, Show)
type Uniq = Int
data TyCon = UnitT deriving (Eq, Show)
type Tau = Type
type Sigma = Type
TauとSigmaはドキュメントのために導入されている。これが気持ち悪いのであれば、TypeからTyAllを消して、以下のように型スキームを別のデータ型に分離すればよい。具体的な実装は[1]が参考になる。
data Scheme = Forall [Uniq] Type
型変数はプログラムによってのみ生成されるため、とりあえず数値（Uniq）として扱っている。数値として扱えば、フレッシュな名前の生成が不要になり、アルゴリズムそのものに焦点を当てられる。
2. 型環境（Type Environment）
型推論をするにあたって、変数と型の組を記憶しておく環境が必要になる。
type Env = M.Map Name Sigma
推論モナド
モナドで環境を管理すると、より Haskell らしいプログラミングができる。
newtype Infer m a = Infer {runInfer :: Env -> Uniq -> m (a, Uniq)}
-- instanceの定義は省略
instance Monad m => Functor (Infer m)
instance Monad m => Applicative (Infer m)
instance Monad m => Monad (Infer m)
instance MonadFail m => MonadFail (Infer m)
instance MonadTrans Infer
instance Monad m => MonadReader Env (Infer m)
Uniqは新しい型変数を生成するために用いられるが、後で説明する。
実装上の Tips として、Envは State モナドではなく、Reader モナドとして扱うほうが良い。State モナドを使うと、変更された環境がその後も伝播してしまって、例えば let 式の本体を処理する前に環境を元に戻さなければならなくなる。一方で、Reader モナドは環境を受け取るだけで、新しい環境を返さないため、クローズドな環境を作ることができる。
そのため、拡張された環境上で処理を実行する以下のような関数が便利である。
extendEnv :: Monad m => Name -> Sigma -> Infer m a -> Infer m a
extendEnv x ty = local (M.insert x ty)
型環境から変数に対応する型を取り出す関数lookupEnvを定義する。
lookupEnv :: MonadFail m => Name -> Infer m Sigma
lookupEnv x = do
env <- ask
case M.lookup x env of
Just ty -> return ty
Nothing -> fail $ "Not in scope '" ++ x ++ "'"
3. 型推論（Type inference）
以下が論文で紹介されている推論規則である。
ただし、これだけでは型環境Env（図内ではTerm（図内では
加えて、規則 INST と GEN は特定の項の形に応じて用いられるわけではないため、どのタイミングでこれらの規則を適用すべきかが定かではない（構文主導でない）。
これらを解消する、Milner によって提案された型推論アルゴリズムが Algorithm W である。
Algorithm W は、代入と単一化という二つの道具を用いる。
代入（Substitution）
代入
型中の型変数に代入applyと、代入を結合するcomposeも定義する。
[Diehl,2016]のコードを参考にした。
type Subst = M.Map Uniq Tau
emptySubst :: Subst
emptySubst = M.empty
apply :: Subst -> Type -> Type
apply s t@(TyVar n) = M.findWithDefault t n s
apply _ (TyCon tc) = TyCon tc
apply s (TyFun ty1 ty2) = TyFun (apply s ty1) (apply s ty2)
apply s (TyAll ns ty) = TyAll ns $ apply (foldr M.delete s ns) ty
compose :: Subst -> Subst -> Subst
s1 `compose` s2 = M.map (apply s1) s2 `M.union` s1
また、型だけでなく、型環境に代入を適用することもあるので、以下の関数を用意する。
applyEnv :: Monad m => Subst -> Infer m a -> Infer m a
applyEnv s = local $ M.map (apply s)
単一化（Unification）
単一化は型の組
単一化アルゴリズムは、以下のunify関数で表される。
コードは[Jones,2005]を参考にした。
unify :: MonadFail m => Tau -> Tau -> Infer m Subst
unify (TyVar u) ty = unifyVar u ty
unify ty (TyVar u) = unifyVar u ty
unify (TyCon tc1) (TyCon tc2) | tc1 == tc2 = return emptySubst
unify (TyFun arg1 res1) (TyFun arg2 res2) = do
s1 <- unify arg1 arg2
s2 <- unify res1 res2
return (s2 `compose` s1)
unify ty1 ty2 = fail $ "Cannot unify type: '" ++ show ty1 ++ "' with '" ++ show ty2 ++ "'"
unifyVar :: MonadFail m => Uniq -> Tau -> Infer m Subst
unifyVar u ty
| ty == TyVar u = return emptySubst
| occursCheck u ty = fail $ "Infinite type: '" ++ show ty ++ "'"
| otherwise = return $ M.singleton u ty
occursCheck :: Uniq -> Tau -> Bool
occursCheck u ty = u `S.member` ftv ty
出現検査occursCheckは、
ここで、ftvは型から自由変数を取り出す。
ftv :: Type -> S.Set Uniq
ftv (TyVar n) = S.singleton n
ftv TyCon{} = S.empty
ftv (TyFun ty1 ty2) = ftv ty1 `S.union` ftv ty2
ftv (TyAll ns ty) = ftv ty `S.difference` S.fromList ns
Algorithm W
[Damas & Milner,1982]で紹介されている Algorithm W の定義は以下の通り。
上から順に、変数（TmVar）、適用（TmApp）、ラムダ式（TmAbs）、Let 式（TmLet）のアルゴリズムを示している。
上記で示されている関数inferTauで表現する。
inferTau :: MonadFail m => Term -> Infer m (Subst, Tau)
(i) 変数（TmVar）
環境に該当する変数があれば空の置換とその型を返し、なければエラーを返す。
inferTau (TmVar n) = do
sigma <- lookupEnv n
tau <- instantiate sigma
return (emptySubst, tau)
型を返す際、多相型を単相型に変換する必要がある。
これが規則 INST であり、次の関数で表される。
instantiate :: Monad m => Sigma -> Infer m Tau
instantiate (TyAll ns ty) = do
tvs <- mapM (const newTyVar) ns
let s = newSubst ns tvs
return $ apply s ty
instantiate ty = return ty
instantiate関数では、多相型から量化子を取り除き、新しい型変数を生成して束縛された型変数と置き換える。つまり、これらの新しく生成された型変数は自由変数となり、単一化によって具体化されるか、もし具体化されなければ冠頭で量化される。
このとき、newTyVarでは新しい名前（現時点ではUniqだが）を生成しなければならないため、どうしても大域的な情報が必要になる。そこで、Infer モナドにユニークな数値をもたせる
newtype Infer m a = Infer {runInfer :: Env -> Uniq -> m (a, Uniq)}
-- instanceの定義は省略
instance Monad m => MonadState Uniq (Infer m)
newTyVar :: Monad m => Infer m Type
newTyVar = do
u <- get
put (u + 1)
return $ TyVar u
(ii) 適用（TmApp）
上記の文章そのままなのでコードを見れば説明はいらないだろう。
ただし、composeの定義上、生成された置換は常に新しい方から適用しなければならない。
inferTau (TmApp fun arg) = do
(s1, fun_ty) <- inferTau fun
(s2, arg_ty) <- applyEnv s1 (inferTau arg)
res_ty <- newTyVar
s3 <- unify (apply s2 fun_ty) (TyFun arg_ty res_ty)
return (s3 `compose` s2 `compose` s1, apply s3 res_ty)
(iii) ラムダ式（TmAbs）
inferTau (TmAbs var body) = do
tv <- newTyVar
(s1, body_ty) <- extendEnv var tv (inferTau body)
return (s1, TyFun (apply s1 tv) body_ty)
(iv) Let 式（TmLet）
inferTau (TmLet var rhs body) = do
(s1, var_ty) <- inferTau rhs
(s2, body_ty) <- applyEnv s1 $ do
var_sigma <- generalize var_ty
extendEnv var var_sigma (inferTau body)
return (s2 `compose` s1, body_ty)
generalize :: Monad m => Tau -> Infer m Sigma
generalize ty = do
env <- ask
let ns = S.toList $ ftv ty `S.difference` ftvEnv env
return $ if null ns then ty else TyAll ns ty
型スキームの推論
最後に推論した型
inferSigma :: (MonadThrow m, MonadIO m) => Term -> Infer m Sigma
inferSigma t = do
(_, tau) <- inferTau t
generalize tau
inferType :: MonadFail m => Term -> m Type
inferType t = fst <$> runInfer (inferSigma t) emptyEnv 0
4. テスト
main :: IO ()
main = forM_ tests $ \t -> do
ty <- inferType t
print ty
tests :: [Term]
tests =
[ TmAbs "x" (TmVar "x") -- \x -> x
, TmAbs "f" (TmAbs "x" (TmApp (TmVar "f") (TmVar "x"))) -- \f x -> f x
, TmAbs "f" (TmLet "x" (TmLit (IntL 1)) (TmApp (TmVar "f") (TmVar "x"))) -- \f -> let x = 1 in f x
, TmAbs "x" (TmApp (TmLit (IntL 3)) (TmVar "x")) -- \x -> () x
]
TyAll [0] (TyFun (TyVar 0) (TyVar 0))
TyAll [1,2] (TyFun (TyFun (TyVar 1) (TyVar 2)) (TyFun (TyVar 1) (TyVar 2)))
TyAll [1] (TyFun (TyFun (TyCon TUnit) (TyVar 1)) (TyVar 1))
algorithmW: user error (Cannot unify type: 'TyCon TUnit' with 'TyFun (TyVar 0) (TyVar 1)')
参考文献
- Roger Hindley. (1969). The principle type-scheme of an object in combinatory logic.
- Robin Milner. (1978). A theory of type polymorphism in programming.
- Luis Damas, Robin Milner. (1982). Principal type-schemes for functional programs.
- Mark P. Jones. (1999). Typing Haskell in Haskell.
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields. (2005). Practical type inference for arbitrary-rank types.
- Stephen Diehl. (2016). Write you a Haskell.
-
Jones,1999 ↩︎
Discussion