在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,等等。
在進一步研究之前,我想知道是否有任何關於此主題的工作,表明這種遞歸模塊的編譯方案是安全的還是不安全的?是否有反例顯示正確輸入此方案的不安全程序?
確實是一個非常有趣的問題。請注意,您提出的解決方案會忽略A的類型可能取決於B和C的類型,如果不是這樣,就沒有理由將它們一起鍵入(與依賴性順序相反)。 – Ingo 2012-02-21 11:03:50
不,實際上,A的類型可以依賴於B和C,但是我認爲在這種情況下B和C的近似就足夠了。我的問題來自一個真實的例子,我通過在編譯器中編寫一個包含此解決方案的補丁來解決此問題,並且程序是安全的(因爲它是由具有遞歸類型的編譯單元組成的),但是我想知道該補丁是否安全一般情況。 – 2012-02-21 12:02:18