Surprising behavior of transparent signature ascription

Question

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

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

So far, so good! Now:

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

Wait. Isn't wat supposed to be hidden? Why am I seeing values of type real wat?

Answer 1

Isn't wat supposed to be hidden?

It's "hidden" in the sense that code cannot refer to it; but since you as a human are aware of it, there's no reason for the REPL to be evasive about it.

Why am I seeing values of type real wat?

Why not? The identifier wat is not in scope, but the type-name still exists. There's no reason there can't be values of types that involve it.

(The same thing is possible even without signatures; something like

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

is perfectly valid, and has a similar effect.)

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.

If you don't want outside code to know that 'a foo is internally 'a wat ref, then you shouldn't use transparent ascription; the whole point of transparent ascription is that outside code still knows what the type is even if the signature doesn't specify it (as opposed to opaque ascription, where outside code really only has what's specified in the signature).

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

Unfortunately, this is not possible. The Definition of Standard ML (Revised) (which defines Standard ML '97, for the most part) lays out the exact set of equality types in §4.4 "Types and Type Functions", on page 17. A constructed type admits equality only if (1) its type name and all of its type arguments admit equality or (2) its type name is the one denoted by ref. In your case, since 'a obviously isn't an equality type, and foo is not ref, 'a foo doesn't admit equality.

(Note: I should mention that the Definition is a little bit wrong here, in that The Standard ML Basis Library specifies a few additional type names that have the same special property as ref, and compilers implement these as well. But this extension just adds more hardcoding; it doesn't add any way for programmers to create additional such type names.)