Standard ML中`datatype ref = datatype ref;`语法语义及用途咨询

1. 语法结构 #

这是Poly/ML对标准ML的扩展语法，属于「类型复制声明」的形式，语法模板为：

datatype <新类型构造器名> = datatype <已有类型构造器名>

标准ML本身没有这个语法，是Poly/ML为方便模块内类型复用新增的特性。

2. 语义含义 #

这个声明的作用是在当前作用域（比如Unsynchronized结构内部）创建一个和目标类型构造器完全等价的别名：

• Unsynchronized.ref和全局的ref本质是同一个类型构造器，并非创建了新的同构类型
• 两者的具体类型（比如Unsynchronized.ref int和ref int）在类型检查中会被视为完全相同，所有针对原类型的操作（比如!、:=）都可以直接用于这个新别名类型的值

3. 用途分析 #

结合你提到的ML_Name_Space.forget_val和ML_Name_Space.forget_type操作，这个写法的核心用途是封装与全局类型重定向：

• 先将全局的ref类型“迁移”到Unsynchronized模块内部，再通过遗忘全局的ref类型和相关操作，强制后续代码只能通过Unsynchronized.ref使用原本的非同步引用
• 这种设计能实现API隔离：Isabelle中可能存在同步版本的引用实现，把原非同步引用封装到Unsynchronized模块后，可明确区分同步/非同步引用类型，避免用户混淆误用
• 同时也能规整模块命名空间：把外部类型引入模块内，让模块API更内聚，用户无需依赖全局类型，仅通过模块即可访问相关类型

内容的提问来源于stack exchange，提问作者opus26