在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

我发现很难找到对这种推理和类型约束过程的一个很好的解释.我用两本书来学习它 - 安德鲁·阿佩尔的"现代编译器实现ML"和皮尔斯的"类型和编程语言".两个人都没有独立完全照亮我,但在他们两个之间我发现了它.