入力して再帰的なモジュールのOCamlで入力されている方法を再帰的なモジュールの<a href="http://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.pdf" rel="noreferrer">Leroy's paper</a>で

Question

は、モジュールがモジュールタイプの近似値で作られた環境の中でチェックされていることを書かれています）; B→約（B）。 C - > approx（C）}が最初に構築され、A、B、Cの型を計算するために使用されます。

近似が十分でなく、型検査が失敗することがあります。特に、コンパイル単位のソースを再帰的なモジュール定義に入れると、型チェックが失敗する可能性がありますが、コンパイラはコンパイル単位を別々にコンパイルできました。

私の最初の例に戻って、最初の近似環境ではA型を入力するが、Aの新しい計算型で拡張された初期環境でB型を入力し、以前の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では）。これは常に順序付けに無関係でなければなりません。

一般的に、再帰的タイピングの問題はあまり健全ではなく、むしろ完全です。一般的に決めることのできないタイプのシステムや、アルゴリズムのアーチファクト（照合順序など）に依存するタイプのシステムは望ましくありません。

より一般的なこととして、Ocamlの再帰的モジュールの扱いはかなり制限されていることはよく知られています。例えば、 Nakataによって&ガリゲ、それはさらに限界をプッシュします。しかし、私は最終的には、Ocamlのモジュール型入力に対する純粋に構文的なアプローチを放棄することなく、あなたが望むようにリベラルなものになることはできないと考えています（そして、それは型モジュールシステムの他の側面にも同様に適用できます） 。しかし、その後、私は偏っている。 :)