再帰モジュールとは

ML系の言語などが持つ階層的なモジュールシステムは大きなソフトウェアを分割して構成するための効果的なツールです。しかし、そのような強い非循環性を要求するモジュールシステムを利用する際は、相互再帰する型や項を1つのモジュールに押し込めなければなりません。

再帰モジュール(recursive modules)はそのような問題を解決するための機構であり、自己言及可能なモジュールを指します。Standard ML風の構文では次のように書かれます。

signature LIST =
  sig
    type t
    val nil : t
    val cons : int * t -> t
  end

structure rec List :> LIST =
  struct
    datatype t = NIL | CONS of int * List.t
    val nil = NIL
    fun cons (n, l) =
      case l of
        NIL          => CONS(n, List.nil)
      | CONS(hd, tl) => CONS(n, List.cons (hd, tl))
  end

このプログラムは整数のリストの、再帰モジュールによる実装例です。LISTシグネチャは何の変哲もないシグネチャですが、Listストラクチャの宣言にはrecという記号が付いています。このrecListが再帰モジュールとして定義されることを意味します。再帰モジュールの内部では、List.tList.nilのように、自身への言及が可能になります。

Listストラクチャはプログラムの残りの部分と、List自身からopaqueに扱われます。言い換えれば、LISTシグネチャがListストラクチャに関する全ての情報を表します。

この定義では、再帰型も再帰関数も使わずに、再帰モジュールだけで再帰構造を表現しています。

ちなみに、consの定義がfun cons (n, l) = CONS(n, l)となっていないのは、現時点ではそのように出来ないからです。この件についてはdouble vision problemの節で話します。

再帰モジュールは既に存在する

先程の例は、再帰モジュールが無くても次のように書けます(少し冗長ですが、比較のためです)。

signature LIST = ...

structure List :> LIST = struct
  datatype t = NIL | CONS of int * t
  val nil = NIL
  fun cons (n, l) =
    case l of
      NIL          => CONS(n, nil)
    | CONS(hd, tl) => CONS(n, cons(hd, tl))
end

この事が示唆するように、再帰モジュールはストラクチャと再帰型、再帰関数で表現できます。(Phase separationを知っている人のために言うと、これは高階モジュールがストラクチャと型レベル関数、高階関数で表現可能なことと似ています。)

Double vision problem

これで話が終われば良いのですが、型生成性と再帰モジュールが絡むと話が複雑になります。上のリストの例ではconsがO(n)になってしまいます。List.tがopaqueである以上、List.ttが同じ型であることが分からないのです。本来1つであるはずの型が2つの異なる型に見えてしまうことから、この問題をdouble vision problemと呼びます。

この問題の解決策として、シグネチャでList.t = tという事実を捉えることにします。このために再帰的依存シグネチャ(recursively dependent signature)というシグネチャを用います。以下に再帰的依存シグネチャを利用したListストラクチャの例を載せます。

structure rec List :>
  sig
    datatype t = NIL | CONS of int * List.t
    ...
  end =
  struct
    datatype t = NIL | CONS of int * List.t
    ...
    fun cons (n, l) = CONS(n, l)
  end

再帰的に定義されるモジュールのシグネチャが、そのモジュール自身に依存していることから、そのシグネチャは再帰的依存シグネチャと呼ばれます。このように再帰的依存シグネチャを使うことでList.ttと一致することを保証できます。

展望

ここまで話した内容は基本的に1999年の(:title paper)に基づくものです。この後、2000年から2010年くらいの間に、型変数の生成と定義を分離するようになったり、さらにそこからopen existential typesに繋がっていったりします。特にopen existential typesは面白いので読んでみてください(再帰モジュールそのものの話ではありませんが)。

Double vision problemは、元々What is a recursive module?ではtrouble with opacityと呼ばれていた問題ですが、最近ではdouble vision problemと呼ばれる傾向にあると思います。

What is a recursive module?では、高階カインドにおける同値再帰型コンストラクタの同値性を検査する必要があるのですが、その同値性は決定的だと知られているわけではなく(not known to be decidable)、決定的な型検査は実装できないと見てよいと思います。もっと実用的な再帰モジュールシステムについて知りたいなら、それ以降の論文を読む必要があるでしょう。モジュールシステムのbibliographyからrecursiveで検索してみるとよいと思います。

参考文献

What is a recursive module?

Karl Crary, Robert Harper, Sidd Puri.
In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 50–63, Atlanta, Georgia, 1999.