functional-programming - SML:可泛化与不可泛化类型变量

Question

我刚刚在Ch中遇到了这些。 Ullman 的 ML 编程要素中的 5 个。他说:

“类型变量如 'a 有两种不同的含义。它可以表示“对于每个类型 T，都有一个类型为 T 的对象的实例代替 'a。 .这种类型变量称为可泛化的。”

然后他说:

"'a 也可以表示我们选择的任何一种类型。但是，在选择了一种类型之后，即使我们重用使用原始类型变量 'a 描述类型的对象，该类型也不能改变。这个类型变量称为不可概括。”

有人可以举一个每种类型的例子吗？很难理解这一点并理解其中的区别似乎很重要(他建立在这些定义之上)。

谢谢!

Answer 1

这是 value restriction 的结果在 SML 中。

由于语言为您的程序推断类型，它可以找到适用于任何类型的表达式，它用类型变量表示。 map函数就是一个很好的例子。 (我的语法可能有点不对劲，因为我从未使用过 SML。)

fun map f nil     = nil
  | map f (x::xs) = f x :: map f xs

由于此函数适用于任何类型的列表，因此它获取一个类型变量:

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

我们可以使用相同的 map两个函数 int list和 string list ——这是一个 泛化类型变量 .值得注意的一件事是 nil案例: nil可以很容易地成为 int 的空列表作为 string 的空列表.它的类型为 'a list .

在一个完美的世界里，这就是我们所拥有的。但是有一个问题:可变引用。按照与上面相同的逻辑，以下 ref在其类型中也会有一个类型变量:

val x = ref nil

我们预计 x成为 ('a list) ref .就像 nil本身，它可以很容易地成为 (int list) ref或 (string list) ref ——或者可以吗？问题是我们可以设置引用。如果我们可以使用 x好像它有更具体的类型 (int list) ref我们可以将其设置为 [1,2,3] .然后，如果我们可以将它用作 (string list) ref在其他地方，我们可以读出 [1,2,3]到期待字符串列表的东西!那是个问题。

为了克服这个问题，SML 有 值(value)限制 .粗略地说，这意味着那些“看起来”不像函数的东西不能是完全多态的——它们不能有可泛化的类型变量。相反， x 的类型将基于我们使用它的第一个具体类型(即 (int list) ref )。如果我们继续尝试使用 x使用不同的具体类型，我们会收到关于不可泛化类型变量的错误。，

从某种意义上说，在我们使用 x 之前，不可泛化的类型变量只是一个占位符。并给它一个具体的类型。这有点令人困惑，因为它看起来仍然像一个普通类型变量( 'a )，但如果我们以多种方式使用它，则会出现错误。我认为 OCaml 在区分两者方面做得更好。 OCaml 会推断出 x 的类型如 '_a它在语法上与普通类型变量不同，并且清楚地表明它只是一个占位符，而不是普通的多态值。

这在语言中有点麻烦，但如果你想拥有这样的可变引用，这基本上是不可避免的。