OCamlの型検査は決定不能

1990年代から(少なくとも一部の人に)知られていることですが、OCamlの型検査は決定不能です。この文書では、ML系モジュールシステムにおけるシグネチャマッチングの仕組みを説明した後、OCamlの型検査器がどのように無限ループに陥るかを確認します。

シグネチャマッチング

ML系言語において、シグネチャは、モジュールのインターフェイスを表すために用いられます。あるモジュールが何らかのシグネチャに適合していることを保証するためにsignature ascriptionという機構があります。

Standard MLでは、M : SM :> Sという風に書くと、モジュールMがシグネチャSに適合していることを保証できます。M : Sはtransparent signature ascriptionと呼ばれ、M :> Sはopaque signature ascriptionと呼ばれます。

シグネチャSinstanceとは、Sの抽象型コンポーネントを何らかの型で置換したものを指します。そして、このときの置換をrealizationと呼びます。たとえば、S = sig type t; val f : t -> t endであるとき、次の全てのシグネチャがSのinstanceとなります。

シグネチャマッチングには2つの側面があります。1つは、Sの任意のinstanceが、Sにマッチすることを許し、もう1つは、よりコンポーネントが多いシグネチャが、よりコンポーネントの少ないシグネチャにマッチすることを許します。

M : SM :> Sの違いは、M : Sはrealizationを明らかにしたままのシグネチャが全体のシグネチャになるのに対し、M :> Sはrealizationを隠してしまうことです。

OCamlの型検査

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つの条件を満たす任意の言語にも適用されます。

  1. 反変関数を持つ。
  2. transparent typeとopaque typeの両方を持つ。
  3. 任意のtransparent typeがopaque typeの部分型になることを許す。

要するに、シグネチャ上を抽象化できるとき、シグネチャマッチングは決定不能になります。これは(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つ目の条件を回避することによって静的に決定可能な型検査を達成しています。

参考文献

  1. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. 1994.
  2. Andreas Rossberg. Undecidability of OCaml type checking. 1999.
  3. Andreas Rossberg. 1ML — Core and modules united. 2018.