統一問題への型推論

Question

誰のアイデアを持っているか型推論の問題

E > hd (cons 1 nil) : α0

タイピング環境と

                E={
                   hd : list(α1 ) → α1 ,
                   cons : α2 → list(α2 ) → list(α2 ),
                   nil : list(α3 ),
                   1 : int
                }

統一問題に転送することができますか？

すべてのヘルプは本当にいただければ幸いです！

Answer 1

あなたの式の中の変数のいずれもタイピング環境の変数と衝突しないように、まず、型変数の名前を変更します。 （あなたの例では、これは既に発現リファレンス{A0}ために行われ、タイピング環境リファレンス{A1、A2、A3}

第二に、新しいタイプの変数を使用して、のようなものを生産する、あなたの表現内のすべての部分式の型の変数を作成します：

nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable

第三に、保持しなければならないタイプの変数間の方程式のセットを生成します。あなたは、トップダウンから、あるいは他の方法で、下から上にこれを行うことができます。 ヒーレン、Bastiaanを参照してください。最高品質の種類のエラーメッセージ。 2005年には、あなたは一つの方法または別のものを選択する理由に関する広範な詳細についてはを。このようなものになります。

a4 = list(a3) // = E(nil)
a5 = int // = E(1)
a6 = a2 -> list(a2) -> list(a2) // = E(cons)

// now it gets tricky, since we need to deal with application for the first time
a5 = a2 // first actual param of cons matches first formal param of cons
a4 = list(a2) // second actual param of cons matches type of second formal param of cons
a7 = list(a2) // result of (cons 1 nil) matches result type of cons with 2 params

a8 = list(a1) -> a1 // = E(hd)    

// now the application of hd
a7 = list(a1) // first actual param of hd matches type of first formal param of hd
a0 = a1 // result of hd (cons 1 nil) matches result type of hd with 1 param

同じ関数が二度タイプの環境から使用された場合に統一する短所が使用するために、我々は誤ってすべての呼び出しを行うことないように、我々は、（上記、第二段階で）多くの新しいタイプの変数を必要とすることを慎重に注意同じタイプ。私は申し訳ありませんが、より明確にこの部分を説明するかどうかはわかりません。 HDと短所がそれぞれ一度だけ使用されているので、ここでは簡単なケースである。

第四に、（私はミスを犯していない場合）、その結果、これらの式を統一ような何かます：

a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int

あなたが今、あなたの元の式中のすべての部分式のタイプを知って、喜べます。

（フェア警告、私は自分自身は、これらの問題に多少アマチュアのだ、と私はよくタイプミスをしたか、誤ってどこかにここにだまさことがあります。）