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と呼ばれます。
シグネチャS
のinstanceとは、S
の抽象型コンポーネントを何らかの型で置換したものを指します。そして、このときの置換をrealizationと呼びます。たとえば、S = sig type t; val f : t -> t end
であるとき、次の全てのシグネチャがS
のinstanceとなります。
sig type t = int; val f : t -> t end
sig type t = string -> bool; val f : t -> t end
sig type t = string -> bool; val f : t -> string -> bool end
シグネチャマッチングには2つの側面があります。1つは、S
の任意のinstanceが、S
にマッチすることを許し、もう1つは、よりコンポーネントが多いシグネチャが、よりコンポーネントの少ないシグネチャにマッチすることを許します。
M : S
とM :> S
の違いは、M : S
はrealizationを明らかにしたままのシグネチャが全体のシグネチャになるのに対し、M :> S
はrealizationを隠してしまうことです。
OCamlにはabstract signature specification (OCamlの用語ではabstract module type specification)という機能があります。これは任意のシグネチャにマッチします。
次のように書くと、
module type S = sig
module type T
end
module M : S = struct
module type T = sig
type t = int
end
end
「任意のシグネチャT
」をコンポーネントに持つシグネチャがS
にマッチします。ちなみにOCamlのモジュールレベルの:
はopaque signature ascriptionですので、Standard MLの:>
に対応します。OCamlにもtransparent signature ascriptionが(<:
という記号で)入る予定はあるようですが、OCaml 4.08には入りませんでした。
さて次のコードは、1999年にRossbergがcaml-listに投稿したもの[2]を簡略化したものです。
module type I = sig
module type A
module F :
sig
module type A = A
module F : A -> sig end
end -> sig end
end
module type J = sig
module type A = I
module F : I -> sig end
end
module Loop(X : J) = (X : I)
最後のLoop
ファンクタはJ <: I
かどうかを試すためにあります。以下で実際にJ <: I
を計算します。
J <: I
-- まず最初のコンポーネントAのinstanceがIだと分かる --
J <: sig
module type A = I
module F :
sig
module type A = A
module F : A -> sig end
end -> sig end
end
-- 最初のコンポーネントAを削除しつつ、残りの部分のAをIで置換する --
sig
module F : I -> sig end
end
<:
sig
module F :
sig
module type A = I
module F : A -> sig end
end -> sig end
end
-- congruence --
I -> sig end
<:
sig
module type A = I
module F : A -> sig end
end -> sig end
-- contravariant --
sig
module type A = I
module F : A -> sig end
end
<:
I
sig
module type A = I
module F : I -> sig end
end
<:
I
J <: I
というようにJ <: I
にまた戻ってしまいます。このコードを実際にOCamlで型検査すると無限ループに陥ります。
¬A := (A -> sig end)
と定義すると、ファンクタ引数の反変性より¬A <: ¬B ⇄ B <: A
が成り立ちます。これにより部分型関係の左辺と右辺を入れ替えられます。
Harper & Lillibridge [1]の言語の型検査は決定不能です。この結果は次の3つの条件を満たす任意の言語にも適用されます。
要するに、シグネチャ上を抽象化できるとき、シグネチャマッチングは決定不能になります。これは(true) first-class moduleの型検査が決定不能になる原因です。そして、abstract signatureの存在するOCamlでも、同じ現象がモジュールレベルで発生します。
Moscow ML (2.00, 2000年)やOCaml (3.12.0, 2010年)がサポートしているfirst-class packaged moduleとは違って、コア言語とモジュール言語の区別を無くした本当の意味でのfirst-class moduleを実現した言語として、1ML [3]が存在します。1MLは「opaque typeの部分型になれるtransparent typeを、抽象型や型パラメータを含まないもの(いわゆるsmall type)に制限する」という方法で3つ目の条件を回避することによって静的に決定可能な型検査を達成しています。