F-ing modules: 存在型によるモジュール基盤

ML モジュールによる抽象化

まず前提として ML モジュールを少し紹介しておく。と言っても、実は僕もそこまで使用経験ないので、OCaml とか、SML とかのチュートリアル読んだり、実際触ってみた方がいいかもしれない。なお、僕は OCaml しか知らないので、構文は OCaml 寄りのものを使っていく。

プログラミングにおいて、整数集合、つまり重複のない整数の集まりを使ったアルゴリズムを実装するシチュエーションを考える。この場合、整数集合を表現するプログラム片を切り離し抽象化しておくことで、よりアルゴリズムの本質的な部分の実装に集中できる。その為、整数集合に関する部分を1つのモジュールとして実装したい。そのような場合に ML モジュールのストラクチャを使うことで、以下のように整数集合を表現するモジュールを定義できる:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

module IntSet = struct
    type elem = int
    type t = elem list

    let empty = []
    let rec add (x, ys) = match ys with
        | [] ->
            [x]
        | y :: ys ->
            if x = y then ys
            else if x < y then x :: ys
            else y :: add (x, ys)
    let rec delete (x, ys) = match ys with
        | [] -> []
        | y :: ys -> if x = y then ys else y :: delete (x, ys)
    let rec member (x, ys) = match ys with
        | [] -> false
        | y :: ys -> x = y || (y < x && member (x, ys))
end

これはソート済みリストによる素朴な整数集合の実装で、 IntSet.t が整数集合を表すデータ型、 IntSet.empty が空集合、 IntSet.add が要素を追加する関数、 IntSet.delete が要素を削除する関数、 IntSet.member が要素が含まれるかを判定する関数になる。このモジュールを使うことで、整数集合に関する処理を抽象化し、他の部分と独立して開発することができるし、性能などの面で内部実装を変えたくなったら、それぞれのこちらのモジュールの実装だけを変えることで変更が可能になり抽象性を担保できる。

ところで、抽象性を担保できると言ったが、厳密にはこのプログラムでは抽象性、つまりこのモジュールの実装を他のモジュールに影響を与えずに変更できるという性質を壊してしまう可能性がある。例えば、 IntSet.t が int list であることが外部からも分かる為、それを前提としたプログラムをこのモジュールの外で書かれてしまうと、 IntSet.t を別のデータ型に変更する際変更がこのモジュールだけで閉じなくなってしまう。このような問題を解決する為、シグネチャを使用することができる。例えば、以下のように整数集合のシグネチャを付与できる:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

module type INTSET = sig
    type elem = int
    type t

    val empty : t
    val add : elem * t -> t
    val delete : elem * t -> t
    val member : elem * t -> bool
end

module IntSet: INTSET = struct
    type elem = int
    type t = elem list

    let empty = []
    let rec add (x, ys) = match ys with
        | [] ->
            [x]
        | y :: ys ->
            if x = y then ys
            else if x < y then x :: ys
            else y :: add (x, ys)
    let rec delete (x, ys) = match ys with
        | [] -> []
        | y :: ys -> if x = y then ys else y :: delete (x, ys)
    let rec member (x, ys) = match ys with
        | [] -> false
        | y :: ys -> x = y || (y < x && member (x, ys))
end

通常シグネチャを指定する際は、 module IntSet: sig ... end = struct ... end という形で指定するのだが、今回は module type でシグネチャを作って指定している点と、 sig ... end の中で type t が具体的な型を伴っていない点がポイントとなっている。これによりストラクチャの外からは、 IntSet.t は何かしらの型であることは分かるが int list であることは分からず、 IntSet.add (1, IntSet.empty) のように使うことはできるが、 1 :: IntSet.empty のように使うことはできない。この型の隠蔽機能こそが、ML モジュールにおける抽象化の一つの真髄と言える。

さて、今は整数集合を考えているが、集合操作に依存したアルゴリズムというのは世の中に多く存在する為、より汎用的に任意の型に対してその要素を持つ集合操作を提供するようなモジュールを作りたいという場面もあるだろう。このような場合に、上記の実装を整数以外にも拡張することを考える。上記の実装において、整数に依存しているのは type elem と比較演算のみであり、これらを与えられれば整数以外の型にも拡張できる。このような拡張を可能にするために、ファンクタを使うことができる:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

module type OrderedType = sig
    type t
    val compare: t * t -> int
end

module type Set = sig
    type elem
    type t

    val empty: t
    val add: elem * t -> t
    val delete: elem * t -> t
    val member: elem * t -> bool
end

module SetMake(Elem: OrderedType): Set with type elem := Elem.t = struct
    type elem = Elem.t
    type t = elem list

    let empty = []
    let rec add (x, ys) = match ys with
        | [] ->
            [x]
        | y :: ys ->
            let cmpXY = Elem.compare (x, y) in
            if cmpXY = 0 then ys
            else if cmpXY < 0 then x :: ys
            else y :: add (x, ys)
    let rec delete (x, ys) = match ys with
        | [] ->
            []
        | y :: ys ->
            let cmpXY = Elem.compare (x, y) in
            if cmpXY = 0 then ys else y :: delete (x, ys)
    let rec member (x, ys) = match ys with
        | [] ->
            false
        | y :: ys ->
            let cmpXY = Elem.compare (x, y) in
            cmpXY = 0 || (cmpXY > 0 && member (x, ys))
end

例えば、この SetMake ファンクタを使えば、先ほどまで実装していた IntSet は以下のようにして作ることができる:

1
2
3
4

module IntSet = SetMake(struct
    type t = int
    let compare (x, y) = y - x
end)

ファンクタをストラクチャをとってストラクチャを返すような、ストラクチャに限定した関数と思えば何となく捉えやすいと思うが、 Set with type elem := Elem.t については説明が必要だろう。まず、 module SetMake(Elem: OrderedType): Set = struct .. end という指定は可能である。しかし、その場合少し困ったことが起きる。というのは、 IntSet が Set シグネチャを持つ為、 IntSet.elem がどういう型なのか外部から分からず、 IntSet.add (1, IntSet.empty) のように使うことができなくなってしまう。今回隠蔽したいのはあくまで、 IntSet.t の型であり、 IntSet.elem の型ではないが、 elem はファンクタに渡されたストラクチャから決まる為ファンクタとしては具体的にどういう型であるとは言えないのだ。このような場合に、 Set with type elem := Elem.t と指定すると、 Set の type elem の定義を type elem = Elem.t に置き換えることができ、外部に Elem.t として公開することができる。これにより、 IntSet.elem が Elem.t であることが分かり、さらに Elem.t は int であることが公開されている為、推移的に IntSet.elem が int であることが外部からも分かるようになる。

このように抽象化機構とファンクタ機能を連携させることができるようになっており、非常に多様な抽象化を実現できるのが ML モジュールの特徴となる。

System-Fω

さて、この ML モジュールをどう形式的に捉えるかという話をしていきたいわけだが、その前にもう一個、今回意味論の土台となる System-Fω という体系も見ていく必要があるので、こちらも一応見ておく。

型付きラムダ計算には、幾つか主要な拡張が知られている。単純型付きラムダ計算をベースとして、高階型または総称型と呼ばれる型を加えた System-F、今回扱う System-F に型構築子と呼ばれる型を加えた System-Fω、System-Fωに依存型と呼ばれる型を加えた Calculus of Constructions (CoC) などがよく知られてるものだろう。ML 系の言語や Haskell では、高階型、型構築子相当の機能が言語中枢に組み込まれているため、その機能について議論するにはそれに見合う表現力を持つ体系が必要になる。ただ、依存型相当の機能は組み込まれていないと整理しても本質的に議論できることが多い。なので、System-Fωをモデルとして使った議論が多い。そういう意味で System-Fω 自体を知っておくのは ML 系言語での他の議論を理解する上でも有用だろう。

さて、今回の F-ing modules のフレームワークにおいては、実は System-F でも本質的な議論ができる。これは、今回重要なのが高階型と存在型の存在にあり、存在型は System-F の範囲で扱えるからだ。なので、System-Fω で議論するのは、そうしないと議論ができないからというよりは、ML 系言語のモデル基盤として System-Fω の表現力が必要であり、そっちに寄せておいた方がより実用的だからという理由からだ。そういう意味で、System-F の基本的な概念を押さえている人は、System-Fωの話は、こういう拡張があるんだなぐらいで捉えておいてもらっても問題ないだろう。

まず、今回プログラム変換対象として考える言語の構文は、以下になる:

System-Fω は種 (kind) $\kappa$、型 (type) $t$、式 (expression) $e$ の3つの構文要素を持つ。最後の $\Gamma$ は型環境で、System-Fω の直接の構文要素ではないが、この後必要になるので一緒に導入しておく。型、式はいいとして、種は見慣れない人もいるかもしれないが、型の型みたいなものだと思ってもらうのが良い。型と同じく、動的意味論には影響を与えないが、型システムに影響を与え、型構築操作に対する安全性を担保するために使われる。存在型、レコードは、この後紹介する型システムと簡約システムを見てもらうのがいいと思うが、通常の System-Fω にはない構文要素になる。ただ、この存在型、レコードの部分は関数型、多相型で模倣可能であり、なんら表現力を変えるわけではないので、表現力が同じ言語体系という意味で今回この存在型、レコード込みの言語を System-Fω と呼んでいる。

さて、次に型システムを見ていく。System-Fω の型システムは、種付け (kinding) $\Gamma \vdash \tau: \kappa$、型等価性 (type equivalence) $\Gamma \vdash \tau_1 \equiv \tau_2: \kappa$、型付け (typing) $\Gamma \vdash e: \tau$ の3要素からなる。この内まず型付けから見ていく:

幾つかの場所で種付けの検査が前提にあることが分かる。これは、型構築の安全性を検査するのと同時に、型付けされる型が型の種を持つこと、つまり $\Gamma \vdash e: \tau$ ならば $\Gamma \vdash \tau: \mathrm{T}$ であることを担保するために指定されている。また、1規則だけ型等価性の検査が前提にある規則がある。これは型キャストの規則であり、型構築子を含む型を正規化した型に変換することをこの規則によって許容している。それぞれの規則の詳細は今回は本題ではないので省略する。System-F、レコード、存在型の規則については、多分 TaPL とかに書いてあるのでそっち参照してもらえると [1]。てことで、次は種付けを見ていく:

式の導入を持つ型は型の種がつく。後は型変数と、型構築子、型構築それぞれで種がつくって感じ。最後に型等価性を見ていく:

α-等価性 (alpha-equivalence)、つまり束縛変数の違いを除く構文的等価性、対称性 (symmetric)、推移性 (transitive)、合同性 (congruence) を載せる規則突っ込んで、最後がβη-等価性 (beta-eta-equivalence)。強正規化で判定可能な範囲のいつものやつ [2]。

で、この型判定通る範囲で、今回の System-Fω は以下の値 (value) を持つ:

動的意味論どう定義するかは諸派あるだろうけど、今回は題材に倣ってコンテキストベースの1ステップ簡約システムで定義すると以下になる:

ま、今回動的意味論そこまで詳しく踏み込まないが、ML モジュールの動的意味論はこれベースで定義されるので、一応ということで。今回理論的な話は抜きなので、自然意味論とかの方が意味掴みやすいかもだけど、本題じゃないし、まいいでしょ。動的意味論については、System-F 踏襲という感じではあるので、こっちも詳しくは TaPL とか参照してもらうのが良さそう [1]。

なお、この後のために、いくつか略記法を導入しておく:

シグネチャのモデル化

さてここからが本題。問題は ML モジュールの本質をどう System-Fω に埋め込んでいくかということだが、その前に議論しやすいように ML モジュールに構文を与えておく:

$M$ がモジュール、$S$ がシグネチャの構文要素になる。種や型、式の詳細は今回興味がなく、System-Fω レベルで表現できるものなら何詰め込んでもいい。雰囲気として、前に出したファンクタによる IntSet モジュール定義の例をこの構文で書いてみると、大体以下の感じ:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

{
    sig OrderedType = {
        type t: *;
        val compare: ...;
    };

    sig Set = {
        type elem: *;
        type t: *;
        val empty: ...;
        val add: ...;
        val delete: ...;
        val member: ...;
    };

    module SetMake = fun Elem: OrderedType => {
        module X = {
            type elem = Elem.t;
            type t = ...;
            val empty = ...;
            val add = ...;
            val delete = ...;
            val member = ...;
        };
    }.X :> Set where type elem = Elem.t;

    module IntSet = {
        module X1 = {
            type t = ...;
            val compare = ...;
        };

        module X2 = SetMake X1;
    }.X2;
}

なお、OCaml の元の構文と比べて少し冗長なところがあると思う。ただ、表現力はそこまで落ちてないことが分かると思う。これらの構文をベースに以下のような拡張を考えると、上の構文が結構現実的な要素を備えていることは分かるんじゃないだろうか:

let 宣言なども ML モジュールベースで考えることができ、中々強力な機能拡張が考えられる。さて、問題はこれらの構文に対して、意味付けをどのようにして与えていくかだ。全体の意味付けを考える前に、まずはシグネチャに対する意味付けを考えていく。シグネチャの意味付けは実は System-Fω の型のうち、以下の要素により捉えることができる:

無名の3つは、原子シグネチャ (atomic signature) と呼ばれる。それぞれ値宣言、型定義、シグネチャ定義それぞれに名前付けする部分を除いた機能をレコード型でモデル化している。例えば、値宣言から名前付けする部分を抜くってことは、つまりその値がどういう型を持つかって情報に着目するわけで、これを静的意味論でモデル化するということは、使われてる型が妥当かどうかを System-Fω の型システムでチェックできるようにするということ。なので、$[\tau]$ はその型を情報として持つレコード型にしてやれば、レコード型の妥当性を調べることがその無名の値宣言の妥当性を調べることと同じになる。レコードにしているのは、普通の型と無名値宣言を区別するためなので、レコードである必要性はあまりないが、そんな感じで System-Fω の型システムを通して、それぞれの宣言が妥当であることを確認できるようにうまく埋め込んでいくのが原子シグネチャの考え方になる。型定義、シグネチャ定義はちょっと複雑だけど、こいつらは実際の値を持たないので、値は自明に作れるようにしつつ、型の部分だけ妥当性を調べるようにできなきゃいけないので、ちょっとハック的な構成になっている。つまり、$\tau$ が $\kappa$ で種付けされるのを System-Fω の 型付け でどうチェックするかという話なんだけど、それを多相的な恒等関数ならどんな型に対しても値作れるよねっというのを利用して、

の型付け調べれば、$\Gamma \vdash \tau: \kappa$ の種付け調べたのと同じになるよねみたいな発想でやってく感じ [3]。シグネチャ宣言の方もそんな感じのハックを使ってチェックすることになる。

これらの原子シグネチャをラベル付けて結合していったのが、ざっくりストラクチャのシグネチャのモデルという感じ。で、型パラメータで多相化されたモジュールからモジュールを生成するのがファンクタという感じになる。で、$\Sigma$ は大体そんな感じになるんだけど、シーリング、つまり型の隠蔽は存在型で表現するようにしてて、その隠蔽付きのモジュールのモデルが $\Xi$ になる。多分ざっくり説明するより、どうモデルに着地させていくか見ていった方がいいと思うので、シグネチャの意味付けを見ていく。シグネチャは以下で定義される $\Gamma \vdash S \rightsquigarrow \Xi$ によって意味付けされる:

シグネチャパスの意味付けはパスの意味付けをそもそも説明してないのでちょっといきなり難易度高いと思うが、そもそもシグネチャパスとはどういうものかというと、他のモジュールで宣言されているシグネチャにアクセスする式のこと。で、$\Gamma \vdash P: [= \Xi] \rightsquigarrow e$ という判定の詳細は後ほど触れるが、これが意味するのはこのパスが $\Xi$ をモデルに持つシグネチャの宣言、つまりそのモデルである $[= \Xi]$ を参照するパスで、そのシグネチャ宣言が妥当であるということを意味している。静的意味論の中の存在であるシグネチャの妥当性を調べるのに、なぜ式が出てくるかというと少し前で触れたように今回は式の型付けにより、静的意味論も調べていくから。つまり式自体は自明なもの、つまり恒等関数で意味のないものだが、その型付けの過程で種付けなどを通ることにより妥当性を調べる。つまりは、最初の判定はシグネチャパスが $\Xi$ のモデルを持つシグネチャ宣言を指すパスならば、$\Xi$ をモデルに持つシグネチャとして扱おうという感じ。

次もやっぱりまだ説明してないのであれだが、宣言群の意味付けをこの後別途与えるので、その意味付けをそのままシグネチャの意味付けとして扱うという感じ。ま、これは後で宣言群の意味付け見た方が分かりやすいと思うので、今はそんな感じで認識してもらうのがいいだろう。

次はファンクタシグネチャの意味付けだが、ファンクタは多相的なモジュールからモジュールへの関数になるので、その引数のシグネチャ、返り値のシグネチャがどうなるかからファンクタシグネチャのモデルが決まる。ただし、2点特徴があり一つが多相パラメータを引数のシグネチャの抽象性から決める点、そして返るシグネチャが引数のシグネチャに依存する点が通常の多相関数型に比べて特殊になる。これはファンクタへの適用を見てもらわないとちょっと説明しにくいのだが、ML モジュールでのファンクタ適用というのは、通常の多相関数、ジェネリック関数などのように型パラメータを別途与えてそこから具体化を行うというような機能は持ち合わせておらず、適用するモジュールのラベルから適当に型パラメータ部分におく型が類推されることになる。また、受け取ったモジュールへのアクセス状況によって返り値のモジュール・シグネチャも決まってくるわけだ。例えば、 SetMake の例で言うと、 elem ラベルは受け取った Elem モジュールの t ラベルに依存すると言う感じだ。つまり、ML モジュールは、表層的にはどうラベル付けされているか、意味論的にはどうモジュールへのアクセスが行われるかによって、ファンクタがどう振る舞うべきか、もっと言うとモジュール全体がどう振る舞うべきかが決まってくるデザインになっている。これが一つ ML モジュールが通常の関数型プログラミング言語の機能と異なる点であり、その表現力の所以となってる点だろう。

最後にシグネチャの制約だが、これは $S$ の中の $\overrightarrow{X}$ でアクセスした型宣言の内容に $T$ と等価であると言う制約をかけたシグネチャになる。なお、$l_X$ は $X$ に対応する一意な System-Fω のラベルになり、$X$ の System-Fω での変換先ということになる。気持ち的には $\overrightarrow{X} = X_1 X_2 X_3$ だとすると、 $S.X_1.X_2.X_3$ が抽象的な型宣言かつ $T$ と種が合うかを調べ、$S.X_1.X_2.X_3 = T$ みたいな制約を $S$ に追加する感じか。ただ等価制約は一度しか付けられない事からも、意味付け方法的にも、シグネチャのうちまだ型が明示されていない部分を具体的に明示するという感じの方が近いかもしれない。

さて、後回しにした宣言群の意味付けも見ていく。宣言群もシグネチャと同じく $\Xi$ でモデル化する。宣言群は以下で定義される $\Gamma \vdash D \rightsquigarrow \Xi$ によって意味付けされる:

値宣言は無名値宣言のモデルにラベルをつける、型定義は無名型定義のモデルにラベルをつける、シグネチャ定義は無名シグネチャ定義にラベルをつけるというのが基本になる。ただし、型宣言は具体的な型に言及できないものとして、存在型を導入しそれにより無名型定義を作る。$\Gamma \vdash T: \kappa \rightsquigarrow \tau$、$\Gamma \vdash K \rightsquigarrow \kappa$ は、パス以外は今回の本題じゃないので、必要に応じて与えられてるものとする。

また、モジュール宣言は基本的に指定されてるシグネチャのモデルが名前付け以外の部分のモデルとなるはずで、それにラベル付けすれば基本モデルになる。ただ、抽象化部分、つまり存在型をフラットにするため外に出している。このフラット化は、ネストしたモジュール宣言へのアクセスと、トップレベルのモジュールに対してのアクセスで抽象化のモデルの相違を招き、非自明なものになる。ただ、実はこのフラット化が一つ F-ing modules のキモの部分になっており、このフラット化によって宣言されたモジュールに対しての抽象化された部分に対してのアクセスを、元来のラベルへの依存を示す依存型による表現ではなく、存在型によって表現できるようになる点が一つ利点になる。題材に分かりやすい例と参考文献が載ってるので、詳細はそっち見てもらうといいと思う。ま、パッと見モデルとしては少し気持ち悪い感はあるが、これを存在型のスコープが抽象化のスコープのモデルになってると捉えると少し納得しやすいかもしれない。トップレベルのモジュールはその中の抽象型のスコープはそのモジュール内に閉じているが、ネストしたモジュールの場合はそのモジュールを含むモジュールのスコープになるという感じか。そのスコープの中で抽象化される型は共有され、その範囲で共通のものとして使えるという感じだ。

シグネチャ展開、空シグネチャはそのままなのでいいだろう。結合も割とそのまま。1個目の宣言群に依存させて、2個目の宣言群が妥当であれば、そのまま結合させる。この際抽象化のスコープをやっぱりそれぞれフラット化して全体にするという感じ。ただこの際、1個目の宣言のラベルを変数としても使えるように、2個目の宣言群チェックの際環境に入れてる。ここで、$x_X$ は $X$ に対応する一意な System-Fω の変数になる。ML モジュールの変数 $X$ に対応するものが、System-Fω ではラベル $l_X$ と変数 $x_X$ 2つあることに注意。基本はラベル $l_X$ が変換先なのだが、モジュールの内部を読み込んで使えるようにしてる場合は変数 $x_X$ も変換先に追加され、その変数を通してもアクセスできるようになるという感じだ。

ストラクチャ・ファンクタの埋込方法

さて、ここまでは ML モジュールのドメインというべき、シグネチャのモデルについて見てきた。ここからが本題で、モジュール本体、つまりストラクチャ・ファンクタをどうモデル化していくかも見ていくことにしよう。モジュールは $\Xi$ を型に持つ System-Fω の式によって意味付けされることになる。その意味付けは、以下で定義された $\Gamma \vdash M \rightsquigarrow e: \Xi$ によって行われる:

変数の解決はいいだろう。また、定義群に対しての意味付けはシグネチャでの宣言群の意味付けと同じように、後で与えたものを流用する。次にモジュールへの射影だが、これも単純に射影元のモジュールを表すレコードから、該当する部分を射影する、ただし抽象化部分について存在型の除去と導入操作で外に出すということを行う。これもいいだろう。ファンクタも、単にファンクタシグネチャの意味付けに倣って、存在型パラメータを多相パラメータに変換し、そのパラメータに依存させた返るモジュールのモデルによる、多相関数を作るだけという感じ。

さて、問題になるのが最後の2つだ。両方見慣れぬ仮定が載ってると思う。まず、ファンクタへの適用から見ていこう。$X_1$、 $X_2$ それぞれまず環境からシグネチャモデルを引っ張ってくるのはいい。その後、そいつらを突っ込んでる謎の仮定がなんだという話になる。ファンクタシグネチャの説明で少し触れたのだが、ML モジュールのファンクタ適用は、多相関数への適用という形になるにも関わらず型パラメータ指定という概念がない。代わりに型パラメータは適用するモジュールのラベルから自動的に判定される。この自動判定の機能を請け負うのが、この謎の判定になる。詳細は後で見るとして、読み方としては、 $\Sigma_2$ と $\exists \overrightarrow{t: \kappa}\ldotp \Sigma_2'$ をマッチングさせると、型パラメータ $\overrightarrow{t: \kappa}$ として、$\overrightarrow{\tau}$ が選ばれ、またサブタイプを反映させるための式が $e$ になるという感じ。この $e$ は今回はサブタイプ考えないので実はなくてもいいが、入れといた方が色々拡張しやすいので入れている感じになる。ま、ようは抽象化部分のマッチングも兼ねたサブタイプの導出という感じになるだろう。後は、ファンクタのモデルである多相関数に、マッチングさせた型を適用し、サブタイプ反映させたモジュールのモデルを適用するという感じになる。

シーリングも、マッチングとサブタイプ関係に合う範囲でシグネチャの制限を入れれるようになっていて、シーリング元のシグネチャモデルと、シーリングするシグネチャのモデルでマッチングさせて、抽象化する部分の型を見つけ、その部分を存在量化して抽象化するという形になる。

マッチングは具体的には、以下のように定義できる:

と言っても単に与えられた型で置き換えてサブタイプ関係満たすかチェックするだけだが。もちろん、どういう型を与えればマッチング満たすかはこっちで考えなきゃいけない。ここら辺のアルゴリズムは今回触れないが、題材に完全性の証明付きで載ってるので、そっち見てもらうのがいいだろう。

サブタイプ関係もそこまで複雑なものではない。まず最初に触れておくのが、$[\Xi]$ という表記で、これは $\{\mathit{sig} = \lambda x: \Xi\ldotp x\}$ の略記になる。つまり、$[= \Xi]$ の自明な導入形式。そこだけ抑えれば最初の3つはいいだろう。値宣言のサブタイプは、型同士のサブタイプ定義して入れることで拡張の余地などもある。構造家シグネチャのサブタイプは、ラベルの順番変えたり、ラベルを少なくするみたいなのを許容しつつ、さらにラベル付けされてる中身のシグネチャもサブタイピングできるという感じ。ファンクタシグネチャのサブタイプは、関数型サブタイプよろしく、引数部分と返り値部分でそれぞれ逆のサブタイプ入れれる感じだ。ただ、ただの関数型と違う部分が、引数の抽象型をマッチングにより具体化できるという部分だ。これにより、わざわざ型制約とか書かなくても、いい感じにマッチングで具体化をしてくれ、使い勝手が上がることになる。抽象シグネチャのサブタイプは、抽象型の一部をマッチングで具体化できるみたいな感じになる。そんな感じで、ファンクタ適用時などは、いい感じに具体化する部分を選びながら、抽象型の一部をパラメータに変換したりサブタイピングで変換したりして、類推をしてくれるような設計がされている。

後は定義群の意味付けを見れば、F-ing modules の全体が完成する感じだ。定義群も $\Xi$ を型に持つ System-Fω の式によって意味付けされる。具体的には、以下の $\Gamma \vdash B \rightsquigarrow e: \Xi$ によって意味付けされる:

まず、$[e]$、 $[\tau: \kappa]$ だが、これは $[\tau]$、 $[= \tau: \kappa]$ の導入形式で、それぞれ $\{\mathit{val} = e\}$、 $\{\mathit{type} = \Lambda t: (\kappa \to \star)\ldotp \lambda x: t\; \tau\ldotp x\}$ の略記となる。また、$\Gamma \vdash E \rightsquigarrow e: \tau$、 $\Gamma \vdash T \rightsquigarrow \tau: \kappa$ も、パス以外は必要に応じて与えられてるものとする。

この前提で、最後以外の規則はいいと思う。触れておくとしたらモジュール定義の $\mathrm{NotAtomic}(\Sigma)$ ってやつかなと思うが、これは要は原子シグネチャ以外ですよってこと。つまり、無名の値宣言だけを引っ張ってくるとかそういうことはできないって感じ。ま、これは無名値宣言の構文とかが与えられているわけではないわけで、構文としてはあくまでモジュールっていうのは構造化されたものかファンクタだと思うので、いいかなと思う。それが意味論段階で限定されるのはちょっと気持ち悪いかもだけど。ただ、射影とかで引っ張ってくるものが型宣言のものか、モジュールかみたいな区別って、ラベルの名前空間でも分けない限り構文的には区別つけられないので、しょうがないと思う。名前空間分けてる言語もあるけど、その分命名の自由度は下がるので賛否あるかなと思う。

さて、問題はモジュールの結合だが、これがなんでこんな複雑になってるかだが、実はあんまり本質的な話じゃない。結合する際に、ラベル被り考慮したりとか、一回 unpack してから pack することになり、その際ラベルアクセスで一番最後の定義だけ引っ張ってくることになるので、それに合わせたシグネチャを作らなきゃいけないとかで複雑化している。$\mathrm{Comb}$ がそういうシグネチャをいい感じに作ってくれる関数になってて、結合するもののうちどちらの定義を使うか、その定義のシグネチャは何かをラベル毎に返してくれるので、それによって結合したモジュールとシグネチャを作ってくという感じ。こんな感じでモジュールの意味付けができる。

最後に残ってるパスの意味付けを見ていく。

パスの意味付けは、モジュール中、型中、式中、それぞれで定義されることになるが、まずモジュール中の場合は普通のモジュールの意味付けと基本同じだが、シグネチャ内に抽象型が使われてないことが要求され、その保証のもとで unpack して抽象型を捨てた部分を持ってくるということをする。これだけを見ると、パスでは抽象型を持つモジュールにアクセスできないため、そのような外部モジュールを使う方法がないように見える。しかし、抽象型含むモジュールを一回モジュール定義で変数に束縛すると、その抽象スコープがモジュール内に広がるということを利用して、モジュール定義と組み合わせればパスによりアクセスができるので、問題がない。これは、外部モジュールは一回インポート文でインポートしてから使う言語が多いことを考えれば、技術的な制約にはあまりならないだろうし、一回一回 unpack するよりインポート文でまとめて unpack させた方が色々扱いやすいことも考えると理にかなってるんじゃないだろうか。型中、式中での使用もモジュール中での使用とあまり変わらず、それぞれ型定義、値定義に限定して、型定義の場合は型の妥当性だけ判定、値定義の場合は定義元の指揮を参照するという形になる。

以上が F-ing modules による、ML モジュールの意味付けになる。

ファンクタと透明性

さて、ML モジュール全体をどう意味付けしていくかを、今回見てきたわけだが、実はこの意味論は OCaml などの ML モジュールの意味論と若干ズレる部分がある。以下の OCaml プログラムを見てみる:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18

module type AbsSig = sig
    type absT
    val sampleV: absT
    val sampleF: absT -> absT
end

module SampleFun(Arg: sig end): AbsSig = struct
    type absT = int
    let sampleV = 1
    let sampleF = fun argX -> argX
end

module SampleArg = struct end

module SampleFunApp1 = SampleFun(SampleArg)
module SampleFunApp2 = SampleFun(SampleArg)

let _ = SampleFunApp2.sampleF SampleFunApp1.sampleV

これは妥当な OCaml プログラムになる。ところで、このプログラムは F-ing module でどうモデルが作られるかを少し見てみよう。まず、今回与えた ML モジュールの構文で書き直してみると、以下のようになる:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20

{
    sig AbsSig = {
        type AbsT: *;
        val SampleV: AbsT;
        val SampleF: AbsT -> AbsT;
    };

    module SampleFun = fun Arg: {} => ({
        type AbsT = int;
        val SampleV = 1;
        val SampleF = λ argX: int. argX;
    } :> AbsSig);

    module SampleArg = {};

    module SampleFunApp1 = SampleFun SampleArg;
    module SampleFunApp2 = SampleFun SampleArg;

    val Result = SampleFunApp2.SampleF SampleFunApp1.SampleV;
}

さて、この内 Result を抜いたところのモデルがどうなるかを見てみる:

注目したいのが、 SampleFunApp1 と SampleFunApp2 のモデルがそれぞれ別の存在量化されてる点。これにより Result は、$t_3$ と $t_4$ が等しいという情報が取れないため、適用の型付けができず、モデル化できない。つまり、OCaml のモジュールと意味論が異なることになる。

実は今回の F-ing modules は、Standard ML の意味論に寄せたものになっている。Standard ML では、ファンクタによって作られる抽象モジュールは、毎回新規に生成されたような動きをする。つまり、今回のようにファンクタ適用する度に新たに抽象化が行われる。それが、存在量化が関数型の中で $\Sigma_1 \to \exists t: \kappa\ldotp \Sigma_2$ のように行われることに表れている。一方 OCaml は、抽象化がファンクタの外側で行われるような意味論、つまり $\exists t: \kappa\ldotp \Sigma_1 \to \Sigma_2$ のようなモデルの与え方の方が近い [4]。前者を生成的 (generative)、後者を適用的 (applicative) であると、題材では区別しており、後者にも対応するような意味付けも紹介されている。今回は導入だけに留めておくが、気になる人は題材の適用的ファンクタのとこを見てみるといいだろう。

まとめ

というわけで、存在型を使って System-Fω の範囲で ML モジュールの意味付けを行ってくフレームワーク、F-ing modules の紹介だった。F-ing modules は、ML モジュールの抽象型の共有を、アクセス方法でそのままモデル化するのではなく、抽象型の共有範囲と共有される情報を存在型でうまくモデル化してやることで、依存型などを使わずうまく意味付けを行っているのが面白いとこかなと思う。

また、System-Fω でモデル化できるということは、その逆に System-Fω の一部機能を ML モジュールで代替できるということで、結構その辺の関係性元にレコードベースの言語デザイン考える時とか参考になるんじゃないかなと思ってたりする。多相関数への適用を、ラベルベースでマッチング駆使してやるとか、結構面白い部分だと思うんだよね。

それはそれとして、明らかに1記事の分量じゃなかった感ある。ま、System-Fω の導入から始めればそうなっちゃうよな。もうちょっと細切れに出せれば良かったが、ある程度できちゃうとそういうの考えるのめんどくってこうなっちゃった。て感じで、久しぶりに書いた記事がめちゃ長くなっちゃったけど、何か参考になればって感じです。この量でも、全然触れられてない重要な部分とかあるので、興味ある人は是非 Rossberg 先生の元論文読んでみてくれ。てわけで、今回はこれで。