使用前定义类型

Question

根据MLton文档：

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

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

虽然在我们的定义中没有假设，但每个上下文 C = T、U、E 都具有同名 E ⊆ T 的属性。 因此，可以松散地认为 T 包含"已生成"的所有类型名称。[...]当然，关于"已经生成"的内容的评论在语义规则方面并不准确。但以下精确结果可能很容易证明：

设 S 是句子 T、U、E ⊢短语⇒ A，使得 tyname E ⊆ T，让 S′ 是句子 T′、

U′、E′ ⊢短语′ ⇒ A′ 出现在 S 的证明中;然后也是 tynameE′ ⊆ T′。

[第21页]

但我对此感到

加倍困惑。

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

其次，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( 中对 ⊕ 的使用，该规则根据需要扩展了 C 的 T。更具体地说，如果r被分配了类型 t option ref，那么第一个声明将生成一个环境 E 1，其相应的 t ∈ tyname E₁。然后，根据排序规则(24(，必须在上下文C' = C ⊕E 1下详细说明第二个声明，在第4.3节 中定义为C +(tyname E 1，E₁(。因此，C'的t∈t，作为良好格式的要求，因此，规则(17(将无法选择与t的表示相同的t。