OCaml'下划线类型'(例如'_a)是否会引入运行时类型错误/健全性违规的可能性？

Question

我正在阅读有关标准ML中的值限制的一些内容,并尝试将示例转换为OCaml以查看它将执行的操作.似乎OCaml在上下文中产生这些类型,其中SML由于值限制而拒绝程序.我也在其他上下文中看到过它们,比如空哈希表尚未"特化"到特定类型.

http://mlton.org/ValueRestriction

以下是SML中被拒绝程序的示例:

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

如果您逐字输入新泽西州的SML的第一行,则会收到以下错误:

- val r: 'a option ref = ref NONE;
stdIn:1.6-1.33 Error: explicit type variable cannot be generalized at its binding declaration: 'a

如果您不使用显式类型注释

- val r = ref NONE

stdIn:1.6-1.18 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val r = ref NONE : ?.X1 option ref

这个虚拟类型究竟是什么？它似乎完全无法访问,无法与任何东西统一

- r := SOME 5;

stdIn:1.2-1.13 Error: operator and operand don't agree [overload conflict]
  operator domain: ?.X1 option ref * ?.X1 option
  operand:         ?.X1 option ref * [int ty] option
  in expression:
    r := SOME 5

相比之下,在OCaml中,虚拟类型变量是可访问的,并且首先与它结合.

# let r : 'a option ref = ref None;;
val r : '_a option ref = {contents = None}

# r := Some 5;;
- : unit = ()
# r ;;
- : int option ref = {contents = Some 5}

这有点令人困惑,并引发了一些问题.

1)符合SML的实现是否可以选择使上面的"虚拟"类型可访问？

2)如果没有价值限制,OCaml如何保持健全？它是否比SML提供更少的保证？

3)类型'_a option ref似乎不如多态'a option ref.为什么不在let r : 'a option ref = ref None;;OCaml中拒绝(带有明确的注释)？

Answer 1

弱多态类型('_-style类型)是编程方便,而不是类型系统的真正扩展.

2)如果没有价值限制,OCaml如何保持健全？它是否比SML提供更少的保证？

OCaml并没有牺牲价值限制,而是实现了一种启发式方法,可以使您免于系统地注释类型的类型,例如ref None其类型只是"每周"多态.通过查看当前的"编译单元"来启发:如果它可以确定每周多态类型的实际类型,那么一切就像初始声明具有适当的类型注释一样,否则编译单元将被拒绝并带有以下消息:

Error: The type of this expression, '_a option ref,
       contains type variables that cannot be generalized

3)类型'_a选项ref似乎比'选项ref更少多态.为什么不让r:'一个选项ref = ref无;; (有明确的注释)在OCaml中被拒绝了吗？

这是因为'_a它不是"真实"类型,例如禁止编写明确定义此"类型"值的签名:

# module A : sig val table : '_a option ref end = struct let option = ref None end;;
Characters 27-30:
  module A : sig val table : '_a option ref end = struct let option = ref None end;;
                             ^^^
Error: The type variable name '_a is not allowed in programs

通过使用递归声明将弱多态变量声明和稍后完成类型定义的函数用法打包在一起,可以避免使用这些弱多态类型,例如:

# let rec r = ref None and set x = r := Some(x + 1);;
val r : int option ref = {contents = None}
val set : int -> unit = <fun>

Answer 2

1)符合SML的实现是否可以选择使上面的"虚拟"类型可访问？

修订后的定义(SML97)没有规定存在"虚拟"类型; 所有它正式指定的是val不能引入多态类型变量,因为右侧表达式不是非扩展表达式.(也有一些关于类型变量未泄漏到顶层的评论,但正如Andreas Rossberg在标准ML的修订定义中的缺陷中指出的那样,这些评论实际上是关于未确定类型而不是定义中出现的类型变量形式主义,所以它们不能真正被视为要求的一部分.)

在实践中,我认为实现有四种方法:

• 某些实现在类型检查期间拒绝受影响的声明,并强制程序员指定单态类型.
• 一些实现,例如MLton,可以防止泛化,但是推迟统一,以便适当的单态类型可以在程序的后期变得清晰.
• 正如您所见,SML/NJ发出警告并实例化一个随后不能与任何其他类型统一的虚拟类型.
• 我想我听说有些实现默认为int？我不确定.

所有这些选项都可能是允许的,并且显然是合理的,尽管"延迟统一"方法确实需要注意确保类型不与尚未生成的类型名称统一(特别是来自仿函数的类型名称,因为那么单形类型可以对应于仿函数的不同应用中的不同类型,其当然具有与常规多态类型相同的类型的问题.

2)如果没有价值限制,OCaml如何保持健全？它是否比SML提供更少的保证？

我对OCaml不是很熟悉,但是根据你所写的内容,它听起来像是使用与MLton相同的方法; 所以,它不应该牺牲稳健性.

(顺便说一下,尽管你暗示了什么,OCaml 确实有价值限制.OCaml 中的值限制和SML中的值限制之间存在一些差异,但是你的代码片段都没有与这些差异相关.你的代码片段只是演示了在OCaml与SML的一个实现中如何实施限制的一些差异.)

3)类型'_a option ref似乎不如多态'a option ref.为什么不在let r : 'a option ref = ref None;;OCaml中拒绝(带有明确的注释)？

再说一次,我对OCaml不太熟悉,但是 - 是的,这对我来说似乎是个错误!

Answer 3

要回答上一个问题的第二部分,

3)[...]为什么不让r:'一个选项ref = ref无;; (有明确的注释)在OCaml中被拒绝了吗？

这是因为OCaml对类型注释中出现的类型变量有不同的解释:它将它们解释为存在量化,而不是普遍量化.也就是说,类型注释只需要适用于其变量的一些可能的实例化,而不是所有.例如,甚至

let n : 'a = 5

在OCaml中完全有效.可以说,这是相当误导的,而不是最好的设计选择.

要在OCaml中强制执行多态,您必须编写类似的东西

let n : 'a. 'a = 5

这确实会导致错误.但是,这引入了局部量词,因此与SML有些不同,并且不适用于'a需要在其他地方绑定的示例,例如:

fun pair (x : 'a) (y : 'a) = (x, y)

在OCaml中,您必须将其重写为

let pair : 'a. 'a -> 'a -> 'a * 'a = fun x y -> (x, y)