12

MarkJonesとOlegKiselyovのチュートリアルに従って、Hindley-Milner型推論アルゴリズムを実装しています。これらは両方とも、おおよその形式のタイプで「バインディングの適用」操作を行います

applyBindings :: TyEnv -> Type -> Type

これは、指定されたにtyvar -> tyバインディングを適用します。を呼び出すのを忘れることは私のコードでよくある間違いであることがわかりました。また、と同じ型を持っているため、Haskellの型システムから助けを得ることができません。型システムで次の不変条件を適用する方法を探しています。TyEnvTypeapplyBindingstyapplyBindings tyenv ty

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

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

-- | 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にはunification-fdにあります）。これにより、不変条件が適用されます。忘れるとapplyBindings、型エラーが発生します。

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

私が説明する線に沿った解決策、つまりとはapplyBindings異なるタイプを与える解決策はありconst idますか？実際のコンパイラーは、MarkとOlegのチュートリアルが使用するのと同じしゃれ（統合変数とオブジェクト言語型変数の間）を使用しますか？

4

1 に答える 1

5

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

  • 型チェッカーは、統合型変数とオブジェクト言語型変数の表現が異なる必要があります。

このバリエーションを実装するのは難しくありません。実際、GHCタイプチェッカーは少なくとも一度はこのように機能したと思います。論文「任意のランクタイプの実用的な型推論」を確認することをお勧めします。付録には、非常に役立つコードがたくさん含まれています。

于 2012-03-19T01:22:04.960 に答える