2

型推論の問題

E > hd (cons 1 nil) : α0

タイピング環境で

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

統一問題で転送できますか?

どんな助けでも本当に感謝します!

4

1 に答える 1

2

まず、型変数の名前を変更して、式の変数が型付け環境の変数と衝突しないようにします。(あなたの例では、式が { 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

第三に、保持しなければならない型変数間の方程式のセットを生成します。これは、ボトムアップ、トップダウン、またはその他の方法で行うことができます。ヘーレン、バスティアンを参照してください。最高品質タイプのエラー メッセージ。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

型環境から同じ関数が 2 回使用された場合、cons へのすべての呼び出しが誤って同じ型を使用しないように、(上記の 2 番目のステップで) 統合する新しい型変数がさらに必要になることに注意してください。 . この部分をもっと明確に説明する方法がわかりません。申し訳ありません。hd と cons はそれぞれ 1 回しか使用されないため、ここでは簡単なケースです。

第 4 に、これらの方程式を統一すると、(間違いがなければ) 次のようになります。

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

幸いなことに、元の式のすべての部分式の型がわかりました。

(公正な警告、私はこれらの問題については自分自身がやや素人であり、タイプミスを犯したか、ここのどこかでうっかりだまされた可能性があります。)

于 2008-12-19T20:33:18.913 に答える