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

好的，所以我们可以开始从中生成一个约束系统。 T5 是 f 的最终返回类型。目前，我们将把整个函数的最终类型称为“TX”——一些新鲜的、未知的类型变量。

因此，在您给出的示例中将产生约束的是函数应用程序。它告诉我们表达式中事物的类型。事实上，这是我们拥有的唯一信息!

那么这些应用程序告诉我们什么？

忽略我们上面分配的类型变量，让我们看一下函数的主体:

y (x z)

z 不应用于任何东西，所以我们将只查找我们分配给它的类型变量是早些时候(T4)并将其用作它的类型。

x 应用于 z，但我们还不知道它的返回类型，所以让我们为其生成一个新的类型变量，并使用我们之前分配给 x (T2) 的类型来创建一个约束:

T2 = T4 -> T7

y 应用于 (x z) 的结果，我们称之为 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 替换第一个未绑定(bind)类型变量，用 'b 替换第二个，依此类推。

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

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

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