🤖

関数型言語の型推論① Hindley-Milner型システム

2022/11/25に公開約10,600字

Damas-Milner 型システム

Damas-Milner 型システムとは、一階の多相型を持つ、型の注釈を必要としないラムダ計算の型システムである。ブログタイトルでは、より一般的に使われる Hindley-Milner という名称を用いたが、本稿では Damas-Milner の名称を用いたい。というのも、本稿では Robin Milner と Luis Damas の共著論文"Principal type-schemes for functional programs"で示された、Algorithm W と呼ばれる型推論アルゴリズムを直接実装するからである。
Damas-Milner の型システムの具体的な実装が紹介されている文献としては、他に以下のようなものがある。

筆者が Haskell で実装したコードはこちら
https://github.com/ksrky/type-inference/tree/master/src/algorithmW

続き

1. 言語(The language)

項(Term)

通常多相ラムダ計算では、ラムダ抽象に型がついたり、型適用、型抽象が構文に必要となるが、Damas-Milner 型システムでは多相性を一階に限定しているためにそれらを省略できる。

この構文を Haskell プログラムに直すとすれば、以下のようになるだろう(基本型も扱えるようにリテラルを構文に追加したが、型システム全体に及ぼす影響はほとんど無い)。論文では「式(expression)」と呼んでいるが、個人的な好みの問題で、ここでは「項(term)」と呼ぶことにする。

algorithmW/Syntax.hs
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)

\tauは単相型(monotypes)と呼ばれ、型変数\alpha、基本型\iota、関数の型\tau \rightarrow \tauからなる。

\sigmaは型スキームであり、単相型\tauと全称型\forall \alpha . \,\sigmaからなる。
一階の多相型(polytypes)と型スキームの違いは、型スキームが量化された型変数が全て先頭にあるのに対して、一階の多相型は式中で量化されても良い点である。
例えば以下の型は一階の多相型ではあるが、型スキームではない。

T \rightarrow \forall a.a

ただ結局このような型も量化子を先頭に持ってきて、型スキームに還元できるので、型スキームだけを考えれば良い。よって実装上は、量化された型変数全てをリストとして扱って、\forall \alpha_1 \alpha_2 ... \alpha_n .\,\tauとしていいだろう。

algorithmW/Syntax.hs
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

TauSigmaはドキュメントのために導入されている。これが気持ち悪いのであれば、TypeからTyAllを消して、Scheme型を導入して、Typeに対する処理をSchemeに対しても行えば良い。具体的な実装は[Jones,1999]を参照せよ。

data Scheme = Forall [Uniq] Type

型変数を数値として扱っている理由は、型変数はプログラムによってのみ生成されるからである。数値として扱えば、フレッシュな名前の生成が不要になり、アルゴリズムそのものに焦点を当てられる。

2. 型環境(Type Environment)

型推論をするにあたって、ある変項がどのような型を持っているか記憶しておく環境が必要である。これは論文では Assumption と呼ばれている。

algorithmW/Syntax.hs
type Env =  M.Map Name Sigma

推論モナド(Inference monad)

モナドで環境を管理すると、より Haskell らしいプログラミングができる。

algorithmW/Monad.hs
newtype Infer m a = Infer {runInfer :: Env -> Uniq -> m (a, Uniq)}

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 モナドは環境を受け取るだけで、新しい環境を返さないため、クローズドな環境を作ることができる。
そのため、拡張された環境上で処理を実行する以下のような関数が便利である。

algorithmW/Monad.hs
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(図内ではA)と項t(図内ではe)が与えられたときに、規則を満たすような\sigmaを見つけるアルゴリズムは得られない。
加えて、規則 INST と GEN は特定の項の形に応じて用いられるわけではないため、どのタイミングでこれらの規則を適用すべきかが定かではない(構文主導でない)。
これらを解消する、Milner によって提案された型推論アルゴリズムが Algorithm W である。
Algorithm W は置換と単一化を用いるため、その説明から行う。

置換(Substitution)

置換Sとは、型変数\alphaから型\tauへのマッピングである。
型中の型変数に置換Sを適用するapplyと、置換を結合するcomposeも定義する。
[Diehl,2016]のコードを参考にした。

algorithmW/Subst.hs
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

また、型だけでなく、型環境に置換を適用することもあるので、以下の関数を用意する。

algorithmW/Monad.hs
applyEnv :: Monad m => Subst -> Infer m a -> Infer m a
applyEnv s = local $ M.map (apply s)

単一化(Unification)

単一化は型の組(T_1, T_2)が与えられると、S\,T_1S\,T_2が同一になるような置換Sを求めるアルゴリズムである。
単一化アルゴリズムは、以下のunify関数で表される。
コードは[Jones,2005]を参考にした。

algorithmW/Unify.hs
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は、X \mapsto X \rightarrow Xのような循環的な代入を含む置換を生成しないようにするために必要である。
ここで、ftvは型から自由変数を取り出す。

src/Subst.hs
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)のアルゴリズムを示している。
上記で示されている関数Wを以下のinferTauで表現する。

algorithmW/Infer.hs
inferTau :: MonadFail m => Term -> Infer m (Subst, Tau)

(i) 変項(TmVar)

環境に該当する変項があれば空の置換とその型を返し、なければエラーを返す。

algorithmW/Infer.hs
inferTau (TmVar n) = do
        sigma <- lookupEnv n
        tau <- instantiate sigma
        return (emptySubst, tau)

型を返す際、量化された型変数に自由変数を代入して、取り除く必要がある。
これが規則 INST であり、次の関数で表される。

algorithmW/Infer.hs
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

このとき、新しい名前を生成しなければならないため、どうしても大域的な情報が必要になる。そこで、Infer モナドにユニークな数値をもたせる

algorithmW/Monad.hs
newtype Infer m a = Infer {runInfer :: Env -> Uniq -> m (a, Uniq)}

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の定義上、生成された置換は常に新しい方から適用しなければならない。

algorithmW/Infer.hs
inferTau (TmApp fun arg) = do
        (s1, fun_ty) <- inferTau fun
        (s2, arg_ty) <- shiftEnv (apply s1) (inferTau arg)
        res_ty <- freshTyVar
        s3 <- unify (apply s2 fun_ty) (TyFun arg_ty res_ty)
        return (s3 `compose` s2 `compose` s1, apply s3 res_ty)

(iii) ラムダ式(TmAbs)

algorithmW/Infer.hs
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)

algorithmW/Infer.hs
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)

\bar{A}(\tau)は、\tau内の自由変数でありかつ、Aには含まれない型変数を量化して、型全体を型スキームにすることを表す。これは規則 GEN に対応する。

algorithmW/Infer.hs
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

型スキームの推論

最後に推論した型\tauを一般化して型スキーム\sigmaを得る。

algorithmW/Infer.hs
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. テスト

algorithmW/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 (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)')

参考文献

Discussion

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