F#中的Hindley Milner类型推断 [英] Hindley Milner Type Inference in F#

问题描述

有人可以在下面的F#程序中逐步解释类型推断:

Can somebody explain step by step type inference in following F# program:

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

我特别想逐步了解辛德利·米尔纳(Hindley Milner)的统一过程是如何工作的.

I specifically want to see step by step how process of unification in Hindley Milner works.

推荐答案

有趣的东西！

首先，我们为sumList发明了一个通用类型: x -> y

First we invent a generic type for sumList: x -> y

并获得简单的方程式: t(lst) = x; t(match ...) = y

And get the simple equations: t(lst) = x; t(match ...) = y

现在添加方程式: t(lst) = [a]由于(match lst with [] ...)

Now you add the equation: t(lst) = [a] because of (match lst with [] ...)

然后等式: b = t(0) = Int; y = b

由于匹配可能为0: c = t(match lst with ...) = b

Since 0 is a possible result of the match: c = t(match lst with ...) = b

从第二种模式开始: t(lst) = [d]; t(hd) = e; t(tl) = f; f = [e]; t(lst) = t(tl); t(lst) = [t(hd)]

From the second pattern: 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

Guess a type (a generic type) for hd: g = t(hd); e = g

然后，我们需要sumList的类型，所以现在我们将只获得无意义的函数类型: h -> i = t(sumList)

Then we need a type for sumList, so we'll just get a meaningless function type for now: h -> i = t(sumList)

现在我们知道: h = f; t(sumList tl) = i

So now we know: h = f; t(sumList tl) = i

然后从附加项中我们得到: Addable g; Addable i; g = i; t(hd + sumList tl) = g

Then from the addition we get: Addable g; Addable i; g = i; t(hd + sumList tl) = g

现在我们可以开始统一了:

Now we can start unification:

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

我跳过了一些琐碎的步骤，但我认为您可以了解它的工作原理.

I skipped some trivial steps, but I think you can get how it works.

这篇关于F#中的Hindley Milner类型推断的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！