Sml Church 数字类型推断

Question

我在 SML 中有这个表达式，需要找到它最通用的类​​型。通过编译器运行时，我得到下面显示的内容。我如何才能找到最通用的类​​型，不仅是这个函数，还有其他函数，比如教堂数字函数“二”。

val one = fn f => (fn x => f x)

为什么是这个类型：

('a -> 'b) -> 'a -> 'b

Answer 1

您所做的是，您应用一个名为 Hindley–Milner 类型推断的过程。

一般原则包括三个步骤：

1. 首先，我们将未确定类型（写成'Z、'Y、'X 等）分配给变量和表达式。

   • 如果表达式使用我们已经分配类型的变量，那么我们使用它。例如，如果three 已经与int 类型绑定，那么在val nine = three * three 中，我们知道three 具有int 类型。
   • 如果表达式使用我们已经分配了非平凡类型 scheme 的变量（即，它是多态的），那么我们使用该方案，但将每个类型变量替换为未确定的类型。例如，如果first 已经与'a * 'b -> 'a 类型绑定，那么在val firstOfFirst = fn quartet => first (first quartet) 中，我们将一个first 指定为'Z * 'Y -> 'Z 类型，另一个指定为'X * 'W -> 'W 类型。
   • 如果表达式使用新绑定的变量（范围为fn 或rec），那么所有出现的该变量都必须具有完全相同的类型——此时不允许多态。例如，在fn f => (f 1, f "one")（最终给出类型错误）中，我们最初将所有出现的f 分配给单一类型'Z。 （导致类型错误是因为我们稍后需要将其细化为 int -> 'Y 和 string -> 'Y，这两个是矛盾的。这是因为标准 ML 不支持 first-class polymorphism。）李>

   在您的示例val one = fn f => (fn x => f x) 中，我们可以将f 分配给'Z 类型，将x 分配给'Y 类型。

2. 接下来，我们执行类型统一，我们在其中识别必须匹配的不同子表达式的类型的不同部分。例如，如果我们知道f 的类型为'Z -> real，i 的类型为int，那么如果我们看到f i，我们可以将'Z 与int“统一”并得出结论f 的类型为 int -> real。

   • 类型统一有很多很多的细节，但我认为它们几乎都是你所假设的，所以我不会深入探讨。

   在您的示例中，由于f 应用于x，我们可以将'Z 与'Y -> ... 统一起来，最终将f 分配给'Y -> 'X 类型。所以整个表达式的类型为('Y -> 'X) -> 'Y -> 'X。

3. 最后，我们执行类型泛化。一旦我们执行了所有可以执行的统一——一旦我们推导出了关于类型的一切——我们可以安全地用绑定类型变量替换未确定的类型。在您的情况下，这让我们可以分配 one 类型方案∀ αβ 。 (α → β) → α → β（意思是“对于任何和所有类型 α 和 β，one 具有类型 (α → β) → α → β”）。在标准 ML 表示法中，我们不包括显式的“∀ αβ”部分；我们只写('a -> 'b) -> 'a -> 'b。

Answer 2

我不太明白你的问题，所以我只是猜测......

如果我在 REPL 中定义第一个教堂数字函数：

val c0 = fn f => fn x => x
val c1 = fn f => fn x => f x
val c2 = fn f => fn x => f (f x)
val c3 = fn f => fn x => f (f (f x))
val c4 = fn f => fn x => f (f (f (f x)))

...然后看看它们的类型：

val c0 = fn : 'a -> 'b -> 'b
val c1 = fn : ('a -> 'b) -> 'a -> 'b
val c2 = fn : ('a -> 'a) -> 'a -> 'a
val c3 = fn : ('a -> 'a) -> 'a -> 'a
val c4 = fn : ('a -> 'a) -> 'a -> 'a 

... 在第二个函数之后，类型 ('a ->'a) -> 'a -> 'a 出现。这是您要寻找的一般类型吗？

前两个函数的类型不同只是因为类型推断算法选择了最通用的类​​型。对于第一个函数 'a -> 'b -> 'b 是更通用的类型，如 ('a -> 'a) -> 'a -> 'a。但是你总是可以使用类型注释给编译器一个提示：

val c0 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => x
val c1 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => f x

...现在你所有的函数都应该有相同的类型了。