透明签名归属的惊人行为

Question

我想定义自己的抽象类型 'a foo，它与 'a ref 一样是 eqtype，即使 'a 不是。例如：

lolcathost% poly
Poly/ML 5.5.2 Release
> signature FOO =
# sig
#   eqtype 'a foo
#   val bar : real foo
#   val qux : real foo
# end;
signature FOO = sig val bar : real foo type 'a foo val qux : real foo end
> structure Foo : FOO =
# struct
#   datatype 'a wat = Wat of 'a
#   type 'a foo = 'a wat ref
#   val bar = ref (Wat 0.0)
#   val qux = ref (Wat 0.0)
# end;
structure Foo : FOO
> Foo.bar = Foo.qux;
val it = false: bool

到目前为止，一切顺利！现在：

> !Foo.bar;
val it = Wat 0.0: real wat
> !Foo.qux;
val it = Wat 0.0: real wat

等等。 wat 不是应该隐藏吗？为什么我看到 real wat 类型的值？

Answer 1

Isn't wat supposed to be hidden?

它是 "hidden"，因为代码无法引用它；但是既然你作为一个人都知道它，那么 REPL 就没有理由回避它。

Why am I seeing values of type real wat?

为什么不呢？标识符 wat 不在范围内，但类型名称仍然存在。没有理由不能有涉及它的类型的值。

（即使没有签名，同样的事情也是可能的；比如

local
   datatype 'a wat = Wat of 'a
in
   val it = Wat 0.0
end

完全有效，并且具有相似的效果。）

Since I don't want outside code to know that 'a foo is internally 'a wat ref, this means that !Foo.bar and !Foo.qux should not typecheck in the first place.

如果你不想让外部代码知道'a foo在内部是'a wat ref，那么你不应该使用透明归属；透明归属的全部要点是，即使签名没有指定，外部代码仍然知道类型是什么（与不透明归属相反，在不透明归属中，外部代码实际上只有签名中指定的内容）。

I want to define my own abstract type 'a foo, that, like 'a ref, is an eqtype even if 'a isn't.

不幸的是，这是不可能的。 标准 ML 的定义（修订版）（大部分定义了 Standard ML '97）在第 4.4 "Types and Type Functions" 页列出了确切的相等类型集17. 仅当 (1) 它的类型名称和它的所有类型参数都承认相等或 (2) 它的类型名称是由 ref 表示的类型时，构造类型才承认相等。在您的情况下，由于 'a 显然不是相等类型，并且 foo 不是 ref，因此 'a foo 不承认相等。

（注意：我应该提到 Definition 在这里有点错误，因为 The Standard ML Basis Library 指定了一个一些额外的类型名称与 ref 具有相同的特殊属性，编译器也实现了这些。但是这个扩展只是增加了更多的硬编码；它没有为程序员添加任何创建额外此类类型的方法名字。)

透明签名归属的惊人行为

Surprising behavior of transparent signature ascription

module

sml

signature