标准ML中按数据类型声明的数据类型

Question

尽管我是标准ML的初学者，但我正在尝试阅读Isabelle的源代码。我到达src/Pure/Concurrent/unsynchronized中的结构Unsynchronized。ML，这似乎是为多线程编程。它包括

...
structure Unsynchronized: UNSYNCHRONIZED =
struct
datatype ref = datatype ref;
...
end;
ML_Name_Space.forget_val "ref";
ML_Name_Space.forget_type "ref";

和我不能理解datatype ref = datatype ref;。它不是数据类型声明的通常的形式。

作为实验，在poly/ML的REPL中，我得到了

> datatype ref = datatype ref;
datatype 'a ref = ref of 'a

，所以这个声明似乎什么也不做，或者给出一个类型构造函数同义词Unsynchronized.ref=ref(Unsynchronized.ref似乎与ref根本没有区别)。

我的问题是:

1. datatype ref = datatype ref;有什么样的语法结构?
datatype ref = datatype ref;的语义(或含义)是什么?
2. 这种类型构造函数同义词声明的用法是什么?(只是为了清晰的语义?)

附录:功能

ML_Name_Space.forget_val
ML_Name_Space.forget_type

在src/Pure/ML/ml_name_space中定义。毫升

val forget_val = PolyML.Compiler.forgetValue;
val forget_type = PolyML.Compiler.forgetType;

等加载后(?)unsynchronized.ML，原来的类型构造函数ref不再可用了。也许，这部分回答了问题3。

Answer 1

datatype ref = datatype ref

表示我们为SML内置类型ref创建了一个同义词，它具有与原始类型相同的构造函数(ref)。

提交并没有提供引入这一点的任何动机，但如果听到这来自

，我不会感到惊讶。(i)支持编译器PolyML和Moscow ML。

(ii)将ref放入适当的模块中以获得更清晰，从而可以调用其他数据类型ref(src/Pure/facts.ML中有一个)