Определить тип перед использованием

Question

Согласно документации MLton:

Стандарт ML требует, чтобы типы были определены до их использования. [ ссылка]

Не все реализации соблюдают это требование (например, SML/NJ), но ссылка на странице выше дает хорошее обоснование того, почему она может быть необходима для надежности (в зависимости от того, как реализация обрабатывает ограничение значения), и это согласуется с некоторыми комментариями в определении:

Хотя это и не предполагается в наших определениях, предполагается, что каждый контекст C = T, U, E обладает свойством, называемым E ⊆ T. Таким образом, T можно свободно рассматривать как содержащий все имена типов, которые "были сгенерированы". […] Конечно, замечания о том, что "было сгенерировано", не являются точными с точки зрения семантических правил. Но следующий точный результат может быть легко продемонстрирован:

Пусть S - предложение T, U, E ⊢ фраза ⇒ A такое, что тимнасы E ⊆ T, и пусть S′ - предложение T′, U′, E′ ⊢ фраза′ ⇒ A′, встречающееся в доказательстве S; затем также имена T′ ′ T′.

[страница 21]

Но я вдвойне смущен этим.

Во-первых, приведенная выше теорема кажется отсталой. Если я правильно понимаю фразу "встречается в доказательстве S", то это, по-видимому, будет означать (в противоположность этому) "как только у вас возникнет контекст, который нарушает намерение, называемое E E T, все последующие контексты также будут нарушать это намерение". Даже если это правда, кажется, что было бы гораздо более полезным и значимым утверждать обратное, а именно: "если все контексты до сих пор соответствуют намерению с тимьянами 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), которое охватывает datatype объявлений, требует только, чтобы сгенерированные имена типов не были в T of C; поэтому он не предотвращает генерацию имени типа, используемого в существующей среде значений (кроме случаев, когда уже верно, что имена VE ⊆ T в C).

Я чувствую, что, наверное, здесь что-то довольно простое, но я понятия не имею, что это может быть!

Answer 1

Что касается вашего первого вопроса, я не уверен, почему вы предлагаете это чтение. Результат в основном говорит о том, что если у вас есть деривация S (представьте, что это дерево), контекст которой удовлетворяет условию, то все его подчиненные выражения (думаю, поддеревья) будут иметь контексты, которые также удовлетворяют условию. Другими словами, все правила поддерживают условие. Думайте об условии как о требовании правильной формы контекста C.

Что касается вашего второго вопроса, обратите внимание на использование ⊕ в правиле секвенирования (24), которое расширяет T of C по мере необходимости. Конкретнее, если r был назначен тип t option refтогда первое объявление создаст среду E₁ с соответствующими t ∈ tynames E₁. Затем, согласно правилу секвенирования (24), второе объявление должно быть разработано в контексте C ' = C ⊕ E₁, который определен как C + (имена E₁, E₁) в Разделе 4.3. Следовательно, t ∈ T в C ', как требуется для правильности, и, следовательно, правило (17) не сможет выбрать тот же t, что и обозначение t,