0

SML にこの式があり、最も一般的なタイプを見つける必要があります。コンパイラを実行すると、以下に示すものが表示されます。この関数だけでなく、教会の数字関数「2」などの他の関数の最も一般的なタイプを見つけるにはどうすればよいでしょうか。

val one = fn f => (fn x => f x)

これのタイプはなぜですか：

('a -> 'b) -> 'a -> 'b
4

2 に答える 2

2

あなたがすることは、Hindley–Milner型推論と呼ばれるプロセスを適用することです。

一般原則には、次の 3 つの手順が含まれます。

  1. まず、変数と式に未定の型( 'Z、'Y、など) を割り当てます。'X

    • 式が既に型を割り当てた変数を使用している場合は、それを使用します。たとえば、threeがすでに typeintにバインドされている場合、 では、が typeを持っval nine = three * threeていることがわかります。threeint
    • 式が、自明でない型スキームを既に割り当てた変数を使用する場合(つまり、多態的)、そのスキームを使用しますが、各型変数を未定の型に置き換えます。たとえば、firstが既に type'a * 'b -> 'aにバインドされている場合、 では、1 つに typeval firstOfFirst = fn quartet => first (first quartet)を割り当て、もう 1 つに type を割り当てます。first'Z * 'Y -> 'Z'X * 'W -> 'W
    • 式が新しくバインドされた変数 (fnまたはでスコープrec) を使用する場合、その変数のすべての出現はまったく同じ型でなければなりません — この時点ではポリモーフィズムは許可されません。たとえば、fn f => (f 1, f "one")（最終的に型エラーが発生します）では、最初にf単一の typeのすべての出現を割り当てます'Z。int -> 'Y(後でそれを と の両方に改良する必要があるため、型エラーが発生します。これらは矛盾しています。これは、標準 ML がファーストクラスのポリモーフィズムstring -> 'Yをサポートしていないためです。)

    あなたの例では、 typeとtypeval one = fn f => (fn x => f x)を割り当てることができます。f'Zx'Y

  2. 次に、型の統一を実行します。ここでは、一致する必要があるさまざまなサブ式の型のさまざまな部分を識別します。たとえば、fが typeを持ち、それが type'Z -> realを持っていることがわかっている場合、 が表示されている場合、 を と「統合」して、typeを持っていると結論付けることができます。iintf i'Zintfint -> real

    • 型の統一には非常に多くの詳細がありますが、それらはすべてあなたが想定しているものとほぼ同じだと思うので、ここでは触れません。

    あなたの例では、fが に適用されるためx、 と統合'Zして、型'Y -> ...を割り当てることになります。したがって、式は全体として type を持ちます。f'Y -> 'X('Y -> 'X) -> 'Y -> 'X

  3. 最後に、型の一般化を実行します。実行可能なすべての統合を実行したら (型についてできる限りのことを推測したら)、未確定の型をバインドされた型変数に安全に置き換えることができます。oneあなたの場合、型スキーム ∀ αβ を割り当てることができます。(α → β) → α → β (「すべてのタイプ α および β についてone、タイプ (α → β) → α → β」を意味する)。標準 ML 表記では、明示的な「∀ αβ」の部分は含めません。書くだけ('a -> 'b) -> 'a -> 'bです。

于 2015-02-19T18:38:14.503 に答える
1

私はあなたの質問をよく理解していないので、私はただ推測しています...

REPL で最初の教会の数字関数を定義すると:

val c0 = fn f => fn x => x
val c1 = fn f => fn x => f x
val c2 = fn f => fn x => f (f x)
val c3 = fn f => fn x => f (f (f x))
val c4 = fn f => fn x => f (f (f (f x)))

...そして、それらのタイプを見てください:

val c0 = fn : 'a -> 'b -> 'b
val c1 = fn : ('a -> 'b) -> 'a -> 'b
val c2 = fn : ('a -> 'a) -> 'a -> 'a
val c3 = fn : ('a -> 'a) -> 'a -> 'a
val c4 = fn : ('a -> 'a) -> 'a -> 'a

... 2 番目の関数の後に、型('a ->'a) -> 'a -> 'aが現れます。これはあなたが探している一般的なタイプですか？

最初の 2 つの関数の型が異なるのは、型推論アルゴリズムが最も一般的な型を選択するためです。そして、最初の関数'a -> 'b -> 'bは、 ('a -> 'a) -> 'a -> 'aとしてより一般的な型です。ただし、型注釈を使用して、いつでもコンパイラにヒントを与えることができます。

val c0 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => x
val c1 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => f x

...そして、すべての関数が同じタイプになるはずです。

于 2015-02-19T18:29:19.027 に答える