值多态性和“产生异常”答案

【问题标题】：Value polymorphism and "generating an exception"值多态性和“产生异常”
【发布时间】：2015-04-15 05:31:13
【问题描述】：

根据标准 ML 的定义（修订版）：

这个想法是，非扩展表达式的动态评估既不会生成异常也不会扩展内存的域，而扩展表达式的评估可能会。

[§4.7, p19;强调我的]

我在网上找到了很多关于 ref-cell 部分的信息，但几乎没有关于异常部分的信息。（一些消息来源指出，多态绑定仍有可能引发Bind，并且这种不一致可能会产生类型理论和/或实现后果，但我不确定这是否相关。）

我已经能够提出一种与异常相关的不健全性，如果我没记错的话，它只能通过值限制来防止；但这种不健全并不依赖于引发异常：

local
  val (wrapAnyValueInExn, unwrapExnToAnyType) =
    let exception EXN of 'a
    in  (EXN, fn EXN value => value)
    end
in
  val castAnyValueToAnyType = fn value => unwrapExnToAnyType (wrapAnyValueInExn value)
end

那么，谁能告诉我定义的含义，以及为什么它提到异常？

（难道“产生异常”是指产生异常name，而不是产生异常packet？）

【问题讨论】：

标签： exception language-lawyer sml value-restriction

【解决方案1】：

我不是类型理论家或形式语义学家，但我想我理解这个定义试图从操作的角度得到什么。

ML 异常的生成意味着，每当流控制两次到达相同的异常声明时，就会创建两个不同的异常。这些不同的对象不仅在内存中，而且这些对象在扩展上也是不平等的：我们可以通过与异常构造函数的模式匹配来区分这些对象。

[顺便说一下，这显示了 ML 异常与大多数其他语言中的异常之间的重要区别。在 ML 中，可以在运行时创建新的异常类。]

另一方面，如果您的程序两次构建相同的整数列表，您可能在内存中有两个不同的对象，但您的程序无法区分它们。它们在外延上是相等的。

作为生成异常为何有用的示例，请考虑 MLton 的 universal type 示例实现：

signature UNIV =
sig
  type univ
  val embed : unit -> { inject : 'a -> univ
                      , project : univ -> 'a option
                      }
end

structure Univ :> UNIV =
struct
  type univ = exn

  fun 'a embed () =
    let
      exception E of 'a
    in
      { inject = E
      , project = fn (E x) => SOME x | _ => NONE
      }
    end
end

如果 ML 没有值限制，此代码将导致巨大的类型安全漏洞：

val { inject = inj1, project = proj1 } = Univ.embed ()
val { inject = inj2, project = proj2 } = Univ.embed ()

(*  `inj1` and `proj1` share the same internal exception. This is
 *  why `proj1` can project values injected with `inj1`.
 *  
 *  `inj2` and `proj2` similarly share the same internal exception.
 *  But this exception is different from the one used by `inj1` and
 *  `proj1`.
 *  
 *  Furthermore, the value restriction makes all of these functions
 *  monomorphic.  However, at this point, we don't know yet what these
 *  monomorphic types might be.
 *)

val univ1 = inj1 "hello"
val univ2 = inj2 5

(*  Now we do know:
 *  
 *    inj1 : string -> Univ.univ
 *    proj1 : Univ.univ -> string option
 *    inj2 : int -> Univ.univ
 *    proj2 : Univ.univ -> int option
 *)

val NONE = proj1 univ2
val NONE = proj2 univ1

(*  Which confirms that exceptions are generative.  *)

val SOME str = proj1 univ1
val SOME int = proj2 univ2

(*  Without the value restriction, `str` and `int` would both
 *  have type `'a`, which is obviously unsound.  Thanks to the
 *  value restriction, they have types `string` and `int`,
 *  respectively.
 *)

【讨论】：

您好，感谢您的回复。似乎这个答案只是对我上一段中的问题回答“是”的一种长期方式？
（因为除非我真的遗漏了什么，否则您使用术语“异常”，或在一个地方使用“异常类”来表示定义所指的内容作为“异常名称”。）
来吧，做出改变。

【解决方案2】：

[对Eduardo León 的回答表示感谢，因为他声明定义确实指的是这一点，并引入了“生成异常”这一短语。我赞成他的答案，但我将其单独发布，因为我觉得他的答案来自错误的方向，有点：大部分答案是对问题已经预设的事物的阐述。]

有没有可能“产生异常”是指产生异常name，而不是产生异常packet？

是的，我想是的。尽管定义通常不单独使用“异常”一词，但其他来源通常将异常名称简称为“异常”——包括在生成它们的特定上下文中。比如来自http://mlton.org/GenerativeException：

在标准 ML 中，异常声明被称为生成，因为每次评估异常声明时，都会产生一个新异常。

（如您所见，该页面始终将异常名称称为“异常”。）

标准 ML 基础库同样以这种方式使用“异常”。例如，从第 29 页开始：

在一个极端情况下，程序员可以在任何地方使用标准异常General.Fail，让它携带一个描述特定故障的字符串。 [...] 例如，一种技术是在结构 Sample 中使用函数 sampleFn 引发异常 Fail "Sample.sampleFn"。

如您所见，本段两次使用“异常”一词，一次是指异常名称，一次是指异常值，依靠上下文来明确含义。

所以定义用“生成异常”这个短语来指代生成异常名称是很合理的（尽管如此，这可能是一个小错误；定义通常比这更精确和正式，并且通常表明它打算依赖上下文来消除歧义）。

【讨论】：