OCamlの型検査は決定不能1990年代から(少なくとも一部の人に)知られていることですが、OCamlの型検査は決定不能です。この文書では、ML系モジュールシステムにおけるシグネチャマッチングの仕組みを説明した後、OCamlの型検査器がどのように無限ループに陥るかを確認します。 シグネチャマッチングML系言語において、シグネチャは、モジュールのインターフェイスを表すために用いられます。あるモジュールが何らかのシグネチャに適合していることを保証するためにsignature ascriptionという機構があります。 Standard MLでは、M : SやM :> Sという風に書くと、モジュールMがシグネチャSに適合していることを保証できます。M : Sはtransparent signature ascriptionと呼ばれ、M :> Sはopaque signature ascriptionと呼ばれます。 シグネチ
GitHub - dhall-lang/dhall-lang: Maintainable configuration files
