functional-programming - ML での型式の導出

Question

全て、

以下の関数の型式を ML で導出したいと考えています。

fun f x y z = y (x z)

これで、同じように入力すると型式が生成されることがわかりました。しかし、私はこれらの値を手で導き出したいと思っています。

また、型式を導出する際の一般的な手順についても言及してください。

Answer 1

ほとんどのコンパイラでの実装とまったく同じように、可能な限り最も機械的な方法でこれを実行しようとします。

それを分解しましょう：

fun f x y z = y (x z)

これは基本的に次の砂糖です：

val f = fn x => fn y => fn z => y (x z)

いくつかのメタ構文型変数を追加しましょう（これらは実際のSML型ではなく、この例のためにホルダーを配置するだけです）。

val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T5

OK、これから制約のシステムの生成を開始できます。T5はfの最終的なリターンタイプです。今のところ、この関数全体の最終的な型を「TX」と呼ぶことにします。これは、いくつかの新しい未知の型変数です。

したがって、与えた例で制約を生成するのは関数適用です。表現の中の物の種類を教えてくれます。実際、私たちが持っている情報はそれだけです！

では、アプリケーションは何を教えてくれるのでしょうか？

上で割り当てた型変数を無視して、関数の本体を見てみましょう。

y (x z)

zは何にも適用されないので、以前に割り当てた型変数（T4）を調べて、それを型として使用します。

xはzに適用されますが、その戻り型はまだわからないので、そのための新しい型変数を生成し、先にx（T2）を割り当てた型を使用して制約を作成しましょう。

T2 = T4 -> T7

yは、（xz）の結果に適用されます。これをT7と呼びます。繰り返しになりますが、yの戻りタイプはまだわからないので、新しい変数を指定します。

T3 = T7 -> T8

また、yの戻り型が関数全体の戻り型であることもわかっています。以前に「T5」と呼んだので、制約を追加します。

T5 = T8

コンパクトにするために、これを少し理解し、関数によって返される関数があるという事実に基づいてTXの制約を追加します。これは、もう少し複雑なことを除いて、まったく同じ方法で導出できます。最終的にこの制約が発生することを確信していない場合は、演習としてこれを自分で行うことができれば幸いです。

TX = T2 -> T3 -> T4 -> T5

ここで、すべての制約を収集します。

val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T5
TX = T2 -> T3 -> T4 -> T5
T2 = T4 -> T7
T3 = T7 -> T8
T5 = T8

この連立方程式を解くには、最後の制約から始めて上に向かって、元の式と同様に、制約のシステムで左側を右側に置き換えます。

val f : TX = fn (x : T2) => fn (y : T3) => fn (z : T4) => y (x z) : T8
TX = T2 -> T3 -> T4 -> T8
T2 = T4 -> T7
T3 = T7 -> T8

val f : TX = fn (x : T2) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
TX = T2 -> (T7 -> T8) -> T4 -> T8
T2 = T4 -> T7

val f : TX = fn (x : T4 -> T7) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8
TX = (T4 -> T7) -> (T7 -> T8) -> T4 -> T8

val f : (T4 -> T7) -> (T7 -> T8) -> T4 -> T8 = fn (x : T4 -> T7) => fn (y : T7 -> T8) => fn (z : T4) => y (x z) : T8

さて、これは現時点では恐ろしいようです。現時点では、表現の全体が実際に座っている必要はありません。説明を明確にするためにそこにあるだけです。基本的に、シンボルテーブルには次のようなものがあります。

val f : (T4 -> T7) -> (T7 -> T8) -> T4 -> T8

最後のステップは、残っているすべての型変数を、私たちが知っていて愛している、より身近なポリモーフィック型に一般化することです。基本的に、これは単なるパスであり、最初の非バインド型変数を'aに、2番目を'bに置き換えます。

val f : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

あなたが見つけるだろうと私はかなり確信しているのは、あなたのSMLコンパイラがその用語に対しても提案するタイプです。私はこれを手作業でメモリから行ったので、どこかで何かを失敗した場合はお詫びします：p

この推論と型制約のプロセスの適切な説明を見つけるのは難しいと思いました。私はそれを学ぶために2冊の本を使用しました-AndrewAppelによる「MLでのModernCompilerImplementation」とPierceによる「TypesandProgrammingLanguages」。どちらも独立して私を完全に照らしているわけではありませんでしたが、2人の間で私はそれを理解しました。

Answer 2

何かの種類を判断するには、それが使用されているすべての場所を調べる必要があります。たとえば、が表示されている場合val h = hd l、それがリストであることがわかりl（hd引数としてリストを受け取るため）、のタイプがのリストでhあるタイプであることがわかりますl。hそれで、isのタイプとisaのタイプ（プレースホルダーはどこにあるか）を考えlてa listみましょう。aが表示されている場合は、がsであるval h2 = h*2ことを知っています。これは、intであるため、intを別のintと乗算でき、2つのintを乗算した結果がintになります。のタイプは前に言ったので、これは、を意味します。したがって、のタイプはです。hh2int2haaintlint list

それでは、あなたの機能に取り組みましょう：

評価される順序で式を考えてみましょう。最初にx z、を実行します。つまり、に適用xしzます。つまりx、は関数なので、タイプはa -> bです。関数の引数として与えられるのでz、型は。でなければなりませんa。そのためのタイプは、の結果タイプであるためx zです。bx

yの結果で呼び出されますx z。これyは、も関数であり、その引数タイプは結果タイプであるx、であるという意味ですb。だからyタイプがありb -> cます。繰り返しますが、式のタイプは、の結果タイプであるためy (x z)です。cy

これらはすべて関数内の式であるため、これ以上型を制限することはできません。したがって、、、およびの最も一般的な型はそれぞれx、yであり、式全体の型はです。z'a -> 'b'b -> 'c'a'c

これは、全体的なタイプfが('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

型がプログラムで推論される方法の説明については、Hindley-Milner型推論について読んでください。

Answer 3

型推論を説明するもう 1 つの方法は、すべての (サブ) 式とすべての (サブ) パターンに型変数が割り当てられることです。

次に、プログラム内の各構成には、その構成に関連する型変数を関連付ける方程式があります。

たとえば、プログラムに fx が含まれていて、'a1 が f の型変数、'a2 が x の型変数、'a3 が "f x" の型変数である場合、

この場合、アプリケーションは次の型の式になります: 'a1 = 'a2 -> 'a3

次に、型推論には基本的に、宣言の型方程式のセットを解くことが含まれます。ML の場合、これは統合を使用するだけで行われ、手動で行うのは非常に簡単です。