在Leroy's paper如何遞歸模塊OCaml中被輸入，它被寫入的模塊是在由模塊類型的近似值的環境檢查：打字遞歸模塊
module rec A = ... and B = ... and C = ...
的環境{A - >約（A ）; B - >約（B）;首先建立C→C（近似）），然後用於計算A，B和C的類型。
我注意到，在某些情況下，近似值不夠好，並且類型檢查失敗。特別是，在將編譯單元源放入遞歸模塊定義中時，類型檢查可能會失敗，而編譯器可以單獨編譯編譯單元。
回到我的第一個例子，我發現一個解決方案是在初始近似環境中鍵入A，然後在該新的計算類型A擴展的初始環境中鍵入B，然後在類型C中鍵入C以前的env和新的計算類型的B，等等。
在進一步研究之前，我想知道是否有任何關於此主題的工作，表明這種遞歸模塊的編譯方案是安全的還是不安全的？是否有反例顯示正確輸入此方案的不安全程序？
首先，請注意，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中），這對定序應該始終無所謂。
一般來說，遞歸鍵入的問題不是那麼健全，而是完整性。你不想要一個通常不可定義的類型系統，或者其規範依賴於算法文物（如檢查順序）的類型系統。
在更一般的說明中，衆所周知Ocaml對遞歸模塊的處理是相當嚴格的。已經有工作，例如由Nakata & Garrigue，進一步推動其極限。然而，我相信最終，你將無法像自己想要的那樣獲得自由（也適用於其類型模塊系統的其他方面，例如函子），而不會放棄Ocaml純粹的句法方法來進行模塊類型化。但是，我有偏見。 :)
感謝您指向Nakata＆Garrigue的作品，我不知道這件事。確實，順序對'let rec'來說並不重要，但是它在語言的其他部分'let x = x + 2 in let x = x * 3 in ...'確實取決於順序。那麼，爲什麼不引入一個「模塊增量記錄」的順序是重要的，並且允許輸入現在不能打字的程序呢？ （現在，我必須閱讀論文......） – 2012-02-21 12:59:08
那麼，嵌套'let'並不完全可比。你可以比較一個平行的'let x = a和y = b in ...'，其中的順序與打字無關。爲什麼不「增量rec」？那麼，恕我直言，這將是一個醜陋的黑客攻擊，而且只能覆蓋一些特定用例。 ;）你不想要更通用的解決方案嗎？ – 2012-02-21 13:17:00
我想要一個更通用的解決方案，但是如果沒有（我仍然需要閱讀更多關於遞歸模塊的信息......），我很喜歡這個駭客解決方案。我不認爲這是「一些具體的用例」，我認爲我的問題可能會頻繁出現。 – 2012-02-21 13:25:17
確實是一個非常有趣的問題。請注意，您提出的解決方案會忽略A的類型可能取決於B和C的類型，如果不是這樣，就沒有理由將它們一起鍵入（與依賴性順序相反）。 – Ingo 2012-02-21 11:03:50
不，實際上，A的類型可以依賴於B和C，但是我認爲在這種情況下B和C的近似就足夠了。我的問題來自一個真實的例子，我通過在編譯器中編寫一個包含此解決方案的補丁來解決此問題，並且程序是安全的（因爲它是由具有遞歸類型的編譯單元組成的），但是我想知道該補丁是否安全一般情況。 – 2012-02-21 12:02:18