Zenn
🐈

型推論器の実装②　Algorithm M

2022/11/25に公開
Haskell
#
型推論
#
型理論
tech

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

Algorithm M は Algorithm W のいくつかの問題点を解決するために導入されたアルゴリズムである。これは長らく慣習的に用いられていたアルゴリズムであったが、[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

推論モードでは、まずはじめに型変数を生成し、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 は置換を逐次計算するアルゴリズムだが、[Diehl,2016]は置換を計算せず、制約集合を記録しておき、あとからまとめて置換を計算する方法（Constraint Generation と呼んでいる）を用いている。このアルゴリズムでは、型環境が Reader に、制約集合が Writer に、ユニークな数値が State に対応する。

参考文献

Discussion