MLton のドキュメントによると:
標準 ML では、使用する前に型を定義する必要があります。【リンク】
すべての実装がこの要件を強制するわけではありません (たとえば、SML/NJ は強制しません) が、上記のリンクのページは、健全性のために必要になる理由 (実装が値の制限をどのように処理するかによって異なります) の良い例です。定義のコメントの一部と一致します。
私たちの定義では想定されていませんが、すべてのコンテキストC = T、U、EがE ⊆ Tという名前のプロパティを持つことが意図されています。したがって、 Tは大まかに、「生成された」すべての型名を含むと考えることができます。[…] もちろん、「生成された」ものについての発言は、意味規則に関して正確ではありません。しかし、次の正確な結果は簡単に実証できます。
S を文T , U , E ⊢句⇒ Aとし、 E ⊆ Tを tynamesとし、S' を S の証明に現れる文T ', U ', E ' ⊢句⇒ A ' とする。次に、 E ' ⊆ T 'も tynames します。
[21ページ]
しかし、私はこれに二重に混乱しています。
まず、上記の定理は後ろ向きに見えます。「Sの証明で発生する」というフレーズを正しく理解すると、これは（対比によって）「E ⊆ Tという名前の意図に違反するコンテキストがあると、後続のすべてのコンテキストもその意図に違反する」ことを意味するようです。それが本当だとしても、逆を主張する方がはるかに有用で意味があるように思われます。 "。いいえ？
第二に、MLton のステートメントもDefinitionのステートメントも、実際には推論規則 (またはそれに続く「さらなる制限」) によってサポートされているようには見えません。いくつかの推論規則には、副条件として「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) は、生成された型名がCのTにdatatypeないことだけを要求します。したがって、既存の値環境で使用される型名の生成を妨げません (ただし、VE ⊆ TのCという名前が既に真である場合を除きます)。
ここにはかなり基本的なものが欠けているように感じますが、それが何であるかはわかりません!