ヒンドレー・ミルナーの推論を聞きました

Question

私は、通常私が使用する言語でアルゴリズムWを実装することで、ヒンドレーミルナー型の推論を教えようとしています、Clojure。私はlet推論の問題に遭遇しています。私が何か間違っているのか、私が期待している結果がアルゴリズム以外のものを必要としているのかどうかはわかりません。

Num a => t -> a 

しかし、私はこれを取得する必要があります：

Num a => a -> a 

を、私はこれを取得

\a -> let b = a in b + 1 

：私はこのタイプを推測しようとした場合、Haskellの表記法を使用して、基本的に

、

もう一度、私は実際にClojureでこれをやっていますが、問題はClojure固有であるとは思わないので、私はHaskellの表記法を使っていますそれをもっと明確にする。私がハスケルでそれを試してみると、私は期待される結果を得る。

とにかく、私は例えば、機能のアプリケーションにすべてのletを変換することにより、その特定の問題を解決することができます：

\a -> (\b -> b + 1) a 

しかし、その後、私はlet多型を失います。私はHMの事前知識がないので、ここで何かが紛失しているのか、それともアルゴリズムがうまくいくのかということです。

EDIT誰でも同様の問題があり、私はそれを解決する方法不思議場合

、私はAlgorith W Step By Stepに従っていました。 2ページの最後には、「タイプのメソッドをリストに拡張することが時々役に立ちます。」それは私には必須の音ではなかったので、私はその部分をスキップして後で再訪することに決めました。

TypeEnvの機能を次のように直接Clojureに翻訳しました：(ftv (vals env))。 ftvをcondという形式で実装していたので、seqの句がないため、(vals env)の場合はnilと返されました。これはまさに静的型システムが捉えるように設計されたバグです。とにかく、envのマップに関するftvの句を(reduce set/union #{} (map ftv (vals env)))と改めただけです。

Answer 1

何が間違っているのかは分かりませんが、私はあなたのlet-generalisationが間違っていると思います。

用語を手動で入力してみましょう。

\a -> let b = a in b + 1 

まず、私たちは新鮮な型変数でaを関連付け、a :: t0は言います。

次に、b = aと入力します。 b :: t0も同様です。しかし

、これは重要なポイントである、我々ははb :: forall t0. t0にbの種類を一般べきではありません。これは、環境内で発生しないtyvarでしか一般化できないためです。a :: t0が存在するため、ここでは代わりにt0が環境内にあります。

一般化すれば、一般的なタイプのbが得られます。 aおよびbのタイプは無関係であるため、b+1はb+1 :: forall t0. Num t0 => t0になり、全体の用語はforall t0 t1. Num t1 => t0 -> t1になります。t0はt1にアルファ変換できます。