f# - Hindley Milner F# での型推論

Question

誰かが次の F# プログラムで段階的な型推論を説明できますか?

let rec sumList lst =
    match lst with
    | [] -> 0
    | hd :: tl -> hd + sumList tl

Hindley Milner の統一プロセスがどのように機能するかを段階的に見たいと思っています。

Answer 1

楽しいもの！

まず、sumList のジェネリック型を作成します。 x -> y

簡単な方程式を取得し t(lst) = xます。 t(match ...) = y

t(lst) = [a]ここで式を追加します。 (match lst with [] ...)

式は次のとおり b = t(0) = Intです。y = b

一致の結果は 0 になる可能性があるため、次のようになります。 c = t(match lst with ...) = b

2 番目のパターンから: t(lst) = [d]; t(hd) = e; t(tl) = f; f = [e]; t(lst) = t(tl); t(lst) = [t(hd)]

:の型 (ジェネリック型) を推測しhdます g = t(hd)。e = g

次に、 の型が必要なsumListので、今のところ意味のない関数型を取得します。 h -> i = t(sumList)

これで次のことがわかり h = fました。 t(sumList tl) = i

次に、加算から次のようになります Addable g。 Addable i; g = i; t(hd + sumList tl) = g

これで統合を開始できます。

t(lst) = t(tl) => [a] = f = [e] => a = e

t(lst) = x = [a] = f = [e];h = t(tl) = x

t(hd) = g = i /\ i = y => y = t(hd)

x = t(lst) = [t(hd)] /\ t(hd) = y => x = [y]

y = b = Int /\ x = [y] => x = [Int] => t(sumList) = [Int] -> Int

いくつかの些細な手順をスキップしましたが、それがどのように機能するかを理解できると思います。