0

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

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

为什么是这个类型：

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

2 回答 2

2

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

一般原则包括三个步骤：

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

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

    在您的示例中val one = fn f => (fn x => f x)，我们可以分配ftype'Z和xtype 'Y。

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

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

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

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

于 2015-02-19T18:38:14.503 回答
1

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

如果我在 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

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

于 2015-02-19T18:29:19.027 回答