防止SML类型变为eqtype而不隐藏构造函数

Question

在datatype声明中,如果所有变体的所有类型参数都是eqtypes ,则Standard ML将生成相等类型.

我在一些地方看过评论,哀叹用户无法提供他们自己的平等定义,并构建他们自己的eqtypes和SML规则的意外后果(例如,裸refs和arrays是eqtypes,但datatype Foo = Foo of (real ref)不是eqtype).

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

人们可能期望能够比较两个类型为real的值,因为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的唯一方法是调整定义,使其不是,例如,通过添加带real参数的伪构造函数.

顺便说一句,小修正:你的类型foo应该是一个相等的类型.如果您的SML实现不同意,那么它就有错误.一个不同的情况是什么real bar时候datatype 'a bar = Bar of 'a ref(这是MLton手册讨论的).第一个工作原因但第二个不工作的原因ref是SML中的神奇之处:它具有用户类型不能拥有的多态性等形式.