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

好的，所以我们可以从此开始生成一个约束系统。 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 的《ML 中的现代编译器实现》和 Pierce 的《类型和编程语言》。这两个人都不能独立地完全启发我，但在他们两个之间我找到了答案。

Answer 2

要确定某物的类型，您需要查看使用它的每个地方。例如，如果您看到 val h = hd l，则您知道 l 是一个列表（因为 hd 将列表作为参数）并且您还知道 h 的类型是 l 的列表类型。因此，假设 h 的类型是 a，而 l 的类型是 a list（其中 a 是占位符）。现在，如果您看到 val h2 = h*2，您就知道 h 和 h2 是 int，因为2 是一个 int，您可以将一个 int 与另一个 int 相乘，两个 int 相乘的结果是一个 int。由于我们之前说过 h 的类型是 a 这意味着 a 是 int，因此 h 的类型是 a code>l 是 int list。

因此，让我们来处理您的函数：

让我们按照计算顺序考虑表达式：首先执行 x z，即将 x 应用于 z >。这意味着 x 是一个函数，因此它的类型为 a -> b。由于 z 作为函数的参数给出，因此它的类型必须为 a。因此，x z 的类型是 b，因为它是 x 的结果类型。

现在使用x z 的结果调用y。这意味着y也是一个函数，其参数类型是x的结果类型，即b。所以 y 的类型为 b -> c.同样，表达式y (xz) 的类型是c，因为它是y 的结果类型。

由于这些都是函数中的表达式，因此我们无法进一步限制类型，因此最常见的类型为 x、y 和 z是 'a -> 'b，'b ->分别为 'c 和 'a，整个表达式的类型为 'c。

这意味着 f 的整体类型为 ('a -> 'b) -> （'b -> 'c）-> '一-> 'c

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

Answer 3

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

然后，程序中的每个构造都有一个方程，该方程涉及与该构造相关的那些类型变量。

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

则应用结果为类型方程：
'a1 = 'a2 -> 'a3

然后，类型推断基本上涉及求解声明的类型方程组。对于机器学习来说，这只需使用统一即可完成，并且手动完成非常容易。