typessmlisabellepolyml

Datatype declaration by datatype in Standard ML

I'm trying to read the source of Isabelle even though I'm a beginner of Standard ML. I arrive at the structure Unsynchronized in src/Pure/Concurrent/unsynchronized.ML, which seems for the multi-thread programming. It includes

...

structure Unsynchronized: UNSYNCHRONIZED =
struct

datatype ref = datatype ref;

...

end;

ML_Name_Space.forget_val "ref";
ML_Name_Space.forget_type "ref";

and I cannot understand datatype ref = datatype ref;. It's not in the usual form of datatype declaration.

As an experiment, in the REPL of poly/ML, I got

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

and so this declaration seems doing nothing or giving a type constructor synonym Unsynchronized.ref = ref (also Unsynchronized.ref seems not being distinguished from ref at all).

So my questions are:

  1. What kind of syntax structure does datatype ref = datatype ref; have?
  2. What is the semantics (or meaning?) of datatype ref = datatype ref;?
  3. What is the usage of such a type constructor synonym declaration? (Just for the clarity in semantics?)

Addendum: The functions

ML_Name_Space.forget_val
ML_Name_Space.forget_type

are defined in src/Pure/ML/ml_name_space.ML as

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

and so after loading (?) unsynchronized.ML, the original type constructor ref is not available anymore. Probably, this answers Q.3 partially.

Solution 
  • datatype ref = datatype ref

    means that we create a synonym for the SML builtin type ref. It has the same constructor (ref) as the original one.

    The commit does not provide any motivation why this was introduced, but I would not be surprised to hear that this comes from

    (i) supporting the compilers PolyML and Moscow ML.

    (ii) putting ref into a proper module for more clarity, making it possible to call other datypes ref (there is one in src/Pure/facts.ML)