ヒンドリー・ミルナーアルゴリズム:型を使用してバインディングが確実に適用されるようにする

Question

のチュートリアルに従って、Hindley-Milner 型推論アルゴリズムを実装しています。 マーク・ジョーンズ そして オレグ・キセリョフ. 。これらは両方とも、おおよそ次のような形式の「バインディングの適用」操作を持っています。

applyBindings :: TyEnv -> Type -> Type

を適用するもの tyvar -> ty バインディング TyEnv 与えられたものに Type. 。コードで呼び出しを忘れるのはよくある間違いであることがわかりました applyBindings, Haskell の型システムの助けは得られません。 ty と同じタイプがあります applyBindings tyenv ty. 。型システムで次の不変式を強制する方法を探しています。

型推論を行う場合、「最終」結果を返す前にバインディングを適用する必要があります

単相オブジェクト言語の型推論を行う場合、wren ng thornton のコードで実装されているように、これを強制する自然な方法があります。 unification-fd パッケージ:2 つのデータ型を定義します Types:

-- | Types not containing unification variables
type Type = ...          -- (Fix TypeF) in wren's package

-- | Types possibly containing unification variables
type MutType = ...       -- (MutTerm IntVar TypeF) in wren's package

そして与える applyBindings タイプ

-- | Apply all bindings, returning Nothing if there are still free variables
-- otherwise just
applyBindings :: TyEnv -> MutType -> Maybe Type

(この関数は実際には freeze . applyBindings 統合FD内）。これにより、不変条件が強制されます - 忘れた場合 applyBindings, 、その場合、型エラーが発生します。

これは私が探している種類のソリューションですが、ポリモーフィズムを備えたオブジェクト言語用です。オブジェクト言語型には型変数がある可能性があるため、上記のアプローチは現状では適用されません。実際、バインディングを適用した後に変数が空いている場合は、戻りたくありません。 Nothing, ですが、これらの変数を一般化したいと考えています。

私が説明したような解決策はありますか?与えるもの applyBindings ～とは異なるタイプ const id?実際のコンパイラーは、Mark と Oleg のチュートリアルで使用されているのと同じ語呂合わせ (統一変数とオブジェクト言語の型変数の間) を使用しますか?

Answer 1

あなたが提案する解決策には他にも問題があるかもしれないと思うので、私はここで暗中模索していますが、少なくとも 1 つの問題には対処できます。

• 型チェッカーには次のものが必要です 違う の代表 統合型変数 そして オブジェクト言語の型変数.

このバリエーションの実装は難しくありません。実際、GHC タイプ チェッカーは少なくともかつてはこの方法で動作していたと思います。紙をチェックしてみるといいかもしれません 任意ランク型の実用的な型推論;付録には、非常に役立つコードがたくさん含まれています。