5

全部，

我想在 ML 中导出以下函数的类型表达式：

fun f x y z = y (x z)

现在我知道输入相同的内容会生成类型表达式。但我希望手动得出这些值。

另外，请提及派生类型表达式时要遵循的一般步骤。

4

3 回答 3

9

我将尝试以最机械的方式来做这件事，就像大多数编译器中的实现一样。

让我们分解一下：

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

好的，所以我们可以开始从中生成一个约束系统。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 替换第一个未绑定类型变量，用 'b 替换第二个，依此类推。

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

我很确定您会发现您的 SML 编译器也会为该术语建议的类型。我是凭记忆手动完成的，如果我在某个地方搞砸了，请道歉：p

我发现很难找到对这种推理和类型约束过程的良好解释。我用了两本书来学习它——Andrew Appel 的“现代编译器实现”和 Pierce 的“类型和编程语言”。两者都没有独立地完全启发我，但在他们两个之间我想通了。

于 2010-07-17T23:30:41.140 回答
3

要确定某物的类型，您需要查看使用它的每个地方。例如，如果您看到val h = hd l，您就知道这l是一个列表（因为hd将列表作为参数）并且您还知道 ofh的类型l是列表的类型。因此，假设 is 的类型和ish的a类型（占位符在哪里）。现在如果你看到，你知道and是s，因为是一个 int，你可以将一个 int 与另一个 int 相乘，两个 int 相乘的结果就是一个 int。既然我们之前说的类型是这个意思就是那个，所以类型的就是。la listaval h2 = h*2hh2int2haaintlint list

因此，让我们处理您的功能：

让我们按照它们被评估的顺序来考虑表达式：首先你做x z，即你x申请z。这意味着x是一个函数，所以它有类型a -> b。由于z作为函数的参数给出，因此它必须具有 type a。的类型x z是因此b，因为那是 的结果类型x。

现在y用 的结果调用x z。这意味着y也是一个函数，它的参数类型是 的结果类型x，即b。y类型也是如此b -> c。表达式的类型也是y (x z)如此c，因为那是 的结果类型y。

由于这些都是函数中的所有表达式，因此我们不能进一步限制类型，因此最通用的类​​型分别为,x和y,和整个表达式的类型是。z'a -> 'b'b -> 'c'a'c

这意味着整体类型f是('a -> 'b) -> ('b -> 'c) -> 'a -> 'c

有关如何以编程方式推断类型的说明，请阅读Hindley-Milner 类型推断。

于 2010-07-16T11:15:38.620 回答
0

解释类型推断的另一种方法是为每个（子）表达式和每个（子）模式分配一个类型变量。

然后，程序中的每个构造都有一个方程式，将与该构造相关的那些类型变量关联起来。

例如，如果程序包含 fx，'a1 是 f 的类型变量，'a2 是 x 的类型变量，'a3 是“f x”的类型变量，

然后应用程序导致类型方程：'a1 = 'a2 -> 'a3

然后，类型推断基本上涉及求解声明的类型方程组。对于 ML，这只是通过使用统一来完成，而且很容易手动完成。

于 2010-07-17T16:51:02.080 回答