使用前定义类型

Question

根据 MLton 文档：

标准 ML 要求在使用类型之前对其进行定义。 [link]

并非所有实现都强制执行此要求（例如，SML/NJ 没有），但上面链接的页面很好地说明了为什么可能需要它来保证可靠性（取决于实现如何处理值限制） ，并且符合定义中的一些注释：

虽然在我们的定义中没有假设，但每个上下文 C = T, U, E 具有 tynames E ⊆ T 的属性。因此，T 可以粗略地认为包含所有“已生成”的类型名称。 […] 当然，就语义规则而言，关于“已生成”的内容的评论并不精确。但是可以很容易地证明以下精确结果：

让 S 是一个句子 T, U, E ⊢ phrase ⇒ A em> 使得 tynames E ⊆ T，令 S′ 为句子 T′，U′， E′ ⊢ 短语′ ⇒ A′ 出现在 S 的证明中；然后还有tynames E′ ⊆ T′。

[第 21 页]

但我对此感到双重困惑。

首先——上述定理似乎倒退了。如果我正确理解短语“发生在 S 的证明中”，那么这似乎意味着（通过反证法）“一旦你的上下文违反了 tynames E ⊆ T，所有后续上下文也将违反该意图”。即使这是真的，似乎断言相反会更有用和更有意义，即“如果到目前为止所有上下文都符合 tynames E ⊆ T em>，那么任何随后可推断的上下文也将符合该意图”。没有？

其次——MLton 的陈述和 定义 的陈述实际上似乎都不受推理规则（或遵循它们的“进一步限制”）的支持。一些推理规则有“tynames τ ⊆ T of C”或“tynames VE ⊆ T of C" 作为一个附带条件，但是这个程序不需要这些规则（在上面链接的文档中给出）：

val r = ref NONE
datatype t = A | B
val () = r := SOME A

（特别是：规则（4）与let有关，规则（14）与=>有关，规则（26）与rec有关。这些都没有在这个程序中使用。）

从另一个方向来看，规则 (17)，它涵盖了 datatype 声明，只要求生成的类型名称不在 C的 T 中>;因此它不会阻止生成在现有值环境中使用的类型名称（除非 tynames VE ⊆ T of C)。

我觉得我可能在这里遗漏了一些非常基本的东西，但我不知道它可能是什么！

Answer 1

关于你的第一个问题，我不确定你为什么建议阅读。结果基本上表明，如果您有一个派生S（将其视为一棵树），其上下文满足条件，那么它的所有子派生（认为子树）将具有也满足条件的上下文。换句话说，所有规则维护条件。将条件视为上下文C的格式良好要求。

关于您的第二个问题，请注意在排序规则 (24) 中使用了 ⊕，它根据需要扩展了 T of C。更具体地说，如果 r 被分配类型 t option ref，那么第一个声明将产生一个环境 E₁ 和对应的 t &in ; tynames E₁。然后，根据排序规则 (24)，第二个声明必须在上下文 C' = C ⊕ E1，定义为C + (tynames E₁, E₁) 在第 4.3 节中。因此，t ∈ T of C'，根据格式良好的要求，因此，规则 (17) 将无法选择与 t 的表示相同的 t。