Объявление типа данных по типу данных в Standard ML
Я пытаюсь прочитать источник Изабель, хотя я новичок в стандартном ML.
Я прихожу к структуре Unsynchronized в src/Pure/Concurrent/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;. Это не обычная форма объявления типа данных.
В качестве эксперимента в REPL поли/ML я получил
> datatype ref = datatype ref;
datatype 'a ref = ref of 'a
и поэтому это объявление, кажется, ничего не делает или дает синоним конструктора типа Unsynchronized.ref = ref (также Unsynchronized.ref, похоже, вообще не отличается от ref).
Итак, мои вопросы:
- Какая синтаксическая структура у
datatype ref = datatype ref;? - Какова семантика (или значение?)
datatype ref = datatype ref;? - Каково использование такого объявления синонима конструктора типа? (Просто для ясности в семантике?)
Приложение: Функции
ML_Name_Space.forget_val
ML_Name_Space.forget_type
определены в src/Pure/ML/ml_name_space.ML как
val forget_val = PolyML.Compiler.forgetValue;
val forget_type = PolyML.Compiler.forgetType;
и поэтому после загрузки (?) unsynchronized.ML исходный конструктор типов ref больше недоступен. Возможно, это частично отвечает на вопрос 3.
Ответы 1
datatype ref = datatype ref
означает, что мы создаем синоним для встроенного типа SML ref. Он имеет тот же конструктор (ref), что и исходный.
Коммит не дает никакой мотивации, почему это было введено, но я не удивлюсь, если услышу, что это происходит из
(i) поддержка компиляторов PolyML и Moscow ML.
(ii) помещение ref в соответствующий модуль для большей ясности, позволяющий вызывать другие типы данных ref (один есть в src/Pure/facts.ML)
В любом случае, я должен был проконсультироваться с «определением», хотя новичку вроде меня трудно следовать ему.
Давным-давно Изабель поддерживала несколько компиляторов SML. И они немного различались по своей семантике (IIRC moscow ml требовал дополнительных ';' в конце определения модулей). Возможно, была какая-то разница в модуле ref.
А... понятно (наверное). Я также однажды запутался в типе chr в Poly/ML (int -> char) и в Isabelle/ML (int -> string), и это несовместимость SML '90 и SML '97. (Позже я обнаружил, что chr переопределено в Isabelle/ML.) В «Определении (пересмотренном)» я обнаружил, что ';' дело еще и в несовместимости 90 vs 97... Меня такая тонкость немного смущает... В любом случае, спасибо большое, Матиас!
Спасибо за ответ. Я также нашел грамматику для
datatype ref = datatype refв Приложении G. 6 к «Определению стандартного ML (пересмотренного)». Я не знал этого объявления «Репликация типов данных». Кроме того, ваше замечание оsrc/Pure/facts.MLочень четко мотивирует репликацию. Я не могу понять пункт (i), но, возможно, это просто потому, что у меня нет опыта, и я забочусь только о поли / ML в текущем чтении исходного кода.