5

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

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

[§4.7，第 19 页；强调我的]

我在网上找到了很多关于 ref-cell 部分的信息，但几乎没有关于异常部分的信息。（一些消息来源指出，多态绑定仍然有可能 raise 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

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

（“生成异常”是否可能意味着生成异常名称，而不是生成异常数据包？）

4

2 回答 2

2

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

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

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

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

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

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.
 *)
于 2015-07-12T18:06:08.100 回答
2

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

“生成异常”是否可能意味着生成异常名称，而不是生成异常数据包？

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

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

（正如您在那里看到的那样，该页面始终将异常名称称为“异常”。）

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

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

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

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

于 2015-07-12T19:13:46.593 回答