печатая рекурсивные модули

Question

В Leroy's paper о том, как рекурсивные модулях набираются в OCaml, написано, что модули проверяются в среде из приближений типов модулей:

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

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

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

Возвращаясь к моему первому примеру, я обнаружил, что решением было бы ввести тип 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: приблизительно (СО), С: ок (СК)}.

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

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

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

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