Во-первых, обратите внимание, что 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 к типизации модулей.,Но тогда я пристрастен.:)