ocaml - OCaml 'underscore types'(例如'_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)

如果您将第一行逐字输入 New Jersey repl 的 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

弱多态类型('_ 样式类型)是一种编程便利，而不是类型系统的真正扩展。

2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?

OCaml 不会牺牲值限制，而是实现了一种启发式方法，使您无需系统地注释值的类型，例如 ref None 其类型仅为“每周”多态。通过查看当前的“编译单元”来进行启发式:如果它可以确定每周多态类型的实际类型，那么一切都会像初始声明具有适当的类型注释一样工作，否则编译单元将被拒绝并显示消息:

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

3) The type '_a option ref seems less polymorphic than 'a option ref. Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in 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>