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

Question

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

我在一些地方看到 cmets 感叹用户无法提供自己的平等定义并构建自己的 eqtypes 以及 SML 规则的意外后果（例如，bare refs 和 arrays 是 eqtypes , 但datatype Foo = Foo of (real ref) 不是 eqtype)。

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

人们可能期望能够比较两个实数 t 类型的值，因为在 ref 单元上进行指针比较就足够了。不幸的是，类型系统只能表示用户定义的数据类型是否承认相等。

我想知道是否可以阻止 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 实现不同意，那么它就有一个错误。 datatype 'a bar = Bar of 'a ref 时的real bar 是另一种情况（这是 MLton 手册所讨论的内容）。第一个有效但第二个无效的原因是 ref 在 SML 中是一种魔法：它具有一种用户类型无法拥有的多态 eq-ness 形式。