Удивительное поведение прозрачной сигнатурной аскрипции

Я хочу определить свой собственный абстрактный тип '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?

1 3
module sml

1 ответ:

Разве wat не должен быть скрыт?

Он "скрыт" в том смысле, что код не может ссылаться на него; но поскольку вы, как человек, знаете о нем, нет причин для того, чтобы REPL уклонялся от него.

Почему я вижу значения типа real wat?

Почему нет? Идентификатор wat отсутствует в области видимости, но имя типа все еще существует. Нет никаких причин, по которым не может быть значений типов, которые включают его.

(то же самое возможно даже без подписей; что-то вроде 

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

Совершенно справедливо и имеет аналогичный эффект.)

Поскольку я не хочу, чтобы внешний код знал, что 'a foo является внутренним 'a wat ref, это означает, что !Foo.bar и !Foo.qux не должны проверять тип в первую очередь.

Если вы не хотите, чтобы внешний код знал, что 'a foo является внутренним 'a wat ref, то вы не должны использовать прозрачное приписывание; весь смысл прозрачного приписывания заключается в том, что внешний код все еще знает, что такое тип даже если подпись не определяет его (в отличие от непрозрачной атрибуции, где внешний код действительно имеет только то, что указано в подписи).

Я хочу определить свой собственный абстрактный тип 'a foo, который, как и 'a ref, является eqtype, даже если 'a не является.

, К сожалению, это невозможно. определение стандарта ML (пересмотренное) (которое определяет стандарт ML '97, по большей части) излагает точный набор типов равенства в §4.4" типы и тип Функции", на стр. 17. Сконструированный тип допускает равенство только в том случае, если (1) его имя типа и все его аргументы типа допускают равенство или (2) его имя типа является именем, обозначаемым ref. В вашем случае, поскольку 'a, очевидно, не является типом равенства, а foo - нет ref, 'a foo не признает равенства.

(Примечание: я должен упомянуть, что определение здесь немного неверно, в том, что стандартная библиотека базиса ML определяет несколько дополнительных имен типов, которые имеют то же самое специальное свойство, что и ref, и компиляторы реализуют их также. Но это расширение просто добавляет больше жесткого кодирования; оно не добавляет никакого способа для программистов создавать дополнительные имена таких типов.)

2