sml - 在不隐藏构造函数的情况下防止 SML 类型变为 eqtype

Question

在 datatype 声明中，如果所有变体的所有类型参数本身都是 eqtype ，标准 ML 将产生一个相等类型。

我在一些地方看到过评论，提示用户无法提供自己的平等定义并构建自己的 eqtype 以及 SML 规则的意外后果(例如，裸 ref 和 array 是 eqtype，但 datatype Foo = Foo of (real ref) 不是 eqtype )。

来源:http://mlton.org/PolymorphicEquality

one might expect to be able to compare two values of type real t, because pointer comparison on a ref cell would suffice. Unfortunately, the type system can only express that a user-defined datatype admits equality or not.

我想知道是否可以阻止 eqtyping。比如说，我将一个集合实现为二叉树(带有一个不必要的变体)，并且我想放弃在结构上比较集合的能力。

datatype 'a set = EmptySet | SetLeaf of 'a | SetNode of 'a * 'a set * 'a set;

假设我不希望人们能够将 SetLeaf(5) 和 SetNode(5, EmptySet, EmptySet) 与 = 区分开来，因为这是一个破坏抽象的操作。

我尝试了一个 datatype on = On | Off 的简单示例，只是想看看我是否可以使用签名将类型降级为非 eqtype。

(* attempt to hide the "eq"-ness of eqtype *)
signature S = sig
  type on
  val foo : on
end

(* opaque transcription to kill eqtypeness *)
structure X :> S = struct
  datatype on = On | Off
  let foo = On
end

似乎透明归属无法阻止 X.on 成为 eqtype，但不透明归属确实阻止了它。但是，这些解决方案并不理想，因为它们引入了新模块并隐藏了数据构造函数。有没有办法防止自定义类型或类型构造函数成为 eqtype 或在不隐藏其数据构造函数或引入新模块的情况下承认相等？

Answer 1

简短的回答是否定的。当一个类型的定义可见时，它的 eq-ness 就是定义所暗示的。防止它成为 eq 的唯一方法是调整定义使其不是，例如，通过添加一个带有 real 的虚拟构造函数范围。

顺便说一句，小修正:您的类型foo应该是相等类型。如果您的 SML 实现不同意，那么它就有一个错误。一个不同的案例是 real bar当datatype 'a bar = Bar of 'a ref (这是 MLton 手册讨论的内容)。第一个有效但第二个无效的原因是 ref在 SML 中很神奇:它具有用户类型所不能具有的多态 eq-ness 形式。