🐈

関数型言語の型推論② Algorithm M

2022/11/25に公開約5,100字

関数型言語の型推論 ① Hindley-Milner 型システムに引き続き、本稿では Damas-Milner 型システムの別の型推論アルゴリズムである Algorithm M を説明する。

Algorithm M は[Lee & Yi,1998]らによって、Algorithm W のいくつかの問題点を解決するために導入されたアルゴリズムである。
Algorithm M の特徴は以下の通り。

  • Algorithm W が、ボトムアップ、すなわち文脈自由であるのに対し、Algorithm M はトップダウンで、文脈依存である。[Lee & Yi,1998]
  • 型付けができない項を受け取ったときは、Algorithm M は Algorithm W より早く停止する。[Lee & Yi,1998]
  • Algorithm W の推論関数の型が、型環境\times項 \rightarrow 置換\times 型であるのに対し、Algorithm M の推論関数の型は、型環境\times項\times型 \rightarrow 置換である。つまり、型の情報が余分に付く。
  • これにより、Algorithm M では型情報が内部に伝播されるため、エラー表示が Algorithm W より分かりやすくなる。[Jones,2005]

本稿は、「関数型言語の型推論 ①」で制作したコードを修正する形で Algorithm M の実装をする。
筆者が Haskell で実装したコードはこちら
https://github.com/ksrky/type-inference/tree/master/src/algorithmM

続き

実装

Algorithm W の実装も Algorithm M の実装も以下のファイルからなる。

  • Syntax.hs: 構文(項、型)、型環境
  • Monad.hs: 推論モナド
  • Subst.hs: 置換
  • Unify.hs: 単一化
  • Infer.hs: 型推論
  • Main.hs: エントリポイント

コードを修正すると行っても、この内変更が必要なのは Infer.hs のみである。

Infer.hs で必要となる関数は以下の通り。Tau型の処理に推論モードと検査モードがあるのが algorithmW からの変更点である。

algorithmW/Infer.hs
inferType :: MonadFail m => Term -> m Type -- 型推論のエントリポイント
inferTau :: MonadFail m => Term -> Infer m Tau -- Tauの型推論
checkTau :: MonadFail m => Term -> Tau -> Infer m Subst -- Tauの型検査 
inferSigma :: MonadFail m => Term -> Infer m Sigma -- Sigmaの型推論

-- algorithmWと変更なし
instantiate :: Monad m => Sigma -> Infer m Tau
generalize :: Monad m => Tau -> Infer m Sigma

以下が[Lee & Yi,1998]で示されている、Algorithm M の形式的な定義である。

この関数Mを直接コードに落とし込むとcheckTauのようになる。

algorithmM/Infer.hs
checkTau :: MonadFail m => Term -> Tau -> Infer m Subst
checkTau (TmLit LUnit) exp_ty = unify exp_ty (TyCon TUnit)
checkTau (TmVar n) exp_ty = do
        sigma <- lookupEnv n
        tau <- instantiate sigma
        unify exp_ty tau
checkTau (TmApp fun arg) exp_ty = do
        arg_ty <- newTyVar
        s1 <- checkTau fun (TyFun arg_ty exp_ty)
        s2 <- applyEnv s1 $ checkTau arg (apply s1 arg_ty)
        return $ s2 `compose` s1
checkTau (TmAbs var body) exp_ty = do
        var_ty <- newTyVar
        body_ty <- newTyVar
        s1 <- unify exp_ty (TyFun var_ty body_ty)
        s2 <- applyEnv s1 $ extendEnv var (apply s1 var_ty) $ checkTau body (apply s1 body_ty)
        return $ s2 `compose` s1
checkTau (TmLet var rhs body) exp_ty = do
        var_ty <- newTyVar
        s1 <- checkTau rhs var_ty
        s2 <- applyEnv s1 $ do
                var_sigma <- generalize (apply s1 var_ty)
                extendEnv var var_sigma $ checkTau body (apply s1 exp_ty)
        return $ s2 `compose` s1

TmLet の場合は下のように書いたほうがシンプルになるだろう。

algorithmM/Infer.hs
checkTau (TmLet var rhs body) exp_ty = do
        var_ty <- inferSigma rhs
        extendEnv var var_ty $ checkTau body exp_ty

推論モードでは、まずはじめに型変数を生成し、checkTau で生成された置換を適用して、推論された型を返す。

algorithmM/Infer.hs
inferTau :: MonadFail m => Term -> Infer m Tau
inferTau t = do
        exp_ty <- newTyVar
        s <- checkTau t exp_ty
        return $ apply s exp_ty

テスト

algorithmM/Main.hs
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 LUnit) (TmApp (TmVar "f") (TmVar "x"))) -- \f -> let x = () in f x
        , TmAbs "x" (TmApp (TmLit LUnit) (TmVar "x")) -- \x -> () x
        ]
出力
TyAll [1] (TyFun (TyVar 1) (TyVar 1))
TyAll [3,4] (TyFun (TyFun (TyVar 3) (TyVar 4)) (TyFun (TyVar 3) (TyVar 4)))
TyAll [2] (TyFun (TyFun (TyCon TUnit) (TyVar 2)) (TyVar 2))
algorithmM: user error (Cannot unify type: 'TyFun (TyVar 3) (TyVar 2)' with 'TyCon TUnit')

Algorithm W の出力と見比べると、より多くの型変数が生成されていることが分かる。

補足

Algorithm M において、推論モードと検査モードをうまく使い分けることによって、構文に型注釈のある言語の型推論も扱いやすくなる。これは、双方向型推論(Bidirectional type inference)にもつながるアイデアである。詳しくは、[Jones,2005]の Section 4.7 を見よ。今後のブログでは Algorithm M をベースとして、副作用のある推論アルゴリズムと、任意階の多相型の型推論を解説する予定である。

また、Algorithm M は置換を逐次計算するアルゴリズムだが、[Diehl,2016]は置換を計算せず、制約集合を記録しておき、あとからまとめて置換を計算する方法(Constraint Generation と呼んでいる)を提示している。このアルゴリズムでは、型環境が Reader に、制約集合が Writer に、ユニークな数値が State に対応するため、Infer モナドに RWS モナドを使うことができる。

参考文献

Discussion

ログインするとコメントできます