набор рекурсивных модулей

Question

В В статье Лероя о том, как рекурсивные модули набираются в OCaml, написано, что модули проверяются в среде, составленной из приближений типов модулей:

module rec A = ... and B = ... and C = ...

окружающая среда {A -> прибл. (A); B -> приблизительно (B); C -> приблизительно (C)} сначала строится, а затем используется для вычисления типов A, B и C.

Я заметил, что в некоторых случаях аппроксимации недостаточно хороши, и проверка типов не выполняется. В частности, при помещении источников блоков компиляции в определение рекурсивного модуля может произойти сбой проверки типов, тогда как компилятор смог скомпилировать блоки компиляции отдельно.

Возвращаясь к моему первому примеру, я обнаружил, что решением будет тип A в исходной приближенной среде, а затем тип B в этой исходной среде, расширенной новым вычисляемым типом A, и тип C в предыдущий env с новым вычисляемым типом B и т. д.

Прежде чем заняться дополнительным изучением, я хотел бы узнать, есть ли какие-либо предварительные работы по этому вопросу, показывающие, что такая схема компиляции для рекурсивных модулей является либо безопасной, либо небезопасной? Существует ли контрпример, показывающий, что небезопасная программа правильно набрана по этой схеме?

Answer 1

Во-первых, обратите внимание, что Leroy (или Ocaml) не разрешает module rec без явных аннотаций подписи.Таким образом, это скорее

module rec A : SA = ... and B : SB = ... and C : SC = ...

, а примерная среда: {A: прибл. (SA), B: прибл. (SB), C: прибл. (SC)}.

Это не удивительночто некоторые модули проверяют тип при определении отдельно, а не когда рекурсивно.В конце концов, то же самое уже верно для объявлений основного языка: в 'let rec' рекурсивные вхождения связанных переменных мономорфны, в то время как с разделенными объявлениями 'let' вы можете полиморфно использовать предыдущие переменные.Интуитивно понятно, что причина в том, что вы не можете обладать всеми знаниями, которые вам понадобятся, чтобы вывести более либеральные типы, прежде чем вы действительно проверите определения.

Что касается вашего предложения, проблема в том, что оно делаетmodule rec построить несимметричный, то есть порядок будет иметь значение потенциально тонкими способами.Это нарушает дух рекурсивных определений (по крайней мере, в ML), которые всегда должны быть безразличны к порядку.

В общем, проблема с рекурсивной типизацией заключается не в правильности, а в полноте.Вам не нужна система типов, которая либо неразрешима в целом, либо спецификация которой зависит от алгоритмических артефактов (например, порядка проверки).

Что касается более общего замечания, хорошо известно, что обращение Окамла срекурсивные модули довольно ограничены.Была работа, например, Nakata & Garrigue, которая расширяет свои границы.Однако я убежден, что в конечном итоге вы не сможете стать настолько либеральным, как вам хотелось бы (и это относится и к другим аспектам его модульной системы типов, например, к функторам), не отказавшись от чисто синтаксического подхода Ocaml к типизации модулей.,Но тогда я пристрастен.:)