日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

モジュールの生成が可能なマルチステージ言語の提案
渡部 恭久

亀山幸義

本研究ではモジュールの生成が可能なマルチステージ言語の提案を行う. マルチステージ・プログラミングはメタプ
ログラミングの実現手法の一つであり, コードの生成を行う段階, 生成したコードを実行する段階といったようにプ
ログラムの実行が複数の段階 (ステージ) に分かれているという特徴がある. マルチステージ・プログラミングをサポートするプログラム言語をマルチステージ言語という. マルチステージ・プログラミングはプログラムの実行効率と保守性・再利用性を両立可能なプログラム手法として有力なものであることが知られているが, 現在のマルチス
テージ言語は生成の対象をプログラムの項のみに限定しており, 他の言語要素をコード生成の対象として扱うことができない. そこで本研究ではモジュールの生成が可能なマルチステージ言語 λ⟨M ⟩ を提案し, 提案体系を用いてモジュールを活用したソフトウェアの実行効率が改善可能であることを示す.

な言語機能として OCaml プログラムでは広く利用さ

1 はじめにれているが, ファンクタ (モジュール上の関数) を利用

マルチステージ・プログラミングはメタプログラ

したプログラムでは, モジュールのメンバ参照に関し

ミングの一形態であり, プログラムの実行効率と保守て実行時オーバヘッドが生じてしまうという問題があ

性・再利用性を両立可能なプログラム手法として有る. 本研究では, マルチステージ・プログラミングの用なものである. マルチステージ・プログラミングを手法により, モジュール内部メンバへの参照を参照先

サポートする機能をもつ言語 (以下，マルチステージのプログラムで置き換えたコードを生成することで,言語と呼ぶ) の中でも, MetaOCaml などの MetaML

このオーバヘッドを削減し, モジュール抽象化と実行

系統のマルチステージ言語は, 静的束縛のもと, 生成効率の両立をはかる.

されるコードの型安全性を保証する理論に支えられてML 系統のマルチステージ言語におけるモジュールいるという特徴がある. 本研究は，MetaML 系統のの扱いに関する従来研究として,Inoue らの研究 [1] がマルチステージ言語を拡張し, モジュールを表すコー

ある. 彼らは, モジュール生成機能が必要と思われる

ドを生成することが可能なマルチステージ言語を提いくつかのメタプログラムの例について論じた後, そ案し, モジュールを活用したソフトウェアの実行効率

れらの例は, 手動によるプログラムの書換えによってを改善することを目標とする.

モジュール生成が必要のない MetaOCaml プログラ

現在の MetaOCaml はコード生成の対象を項のみ

ムとして実現できることを示した. ただし, この書換に限定しており, 他の言語要素, 例えば型やモジューえが有効な範囲については論じていない. 本研究はルといった要素を生成することができない. モジュー

MetaOCaml のコード言語にモジュール生成機能を

ルは, ソフトウェアの構造化・抽象化を提供する強力

加えた新しいプログラム言語 λ⟨M ⟩ を提案し, その言

Multi-Stage Module Generation
Takahisa Watanabe, Yukiyoshi Kameyama, 筑波大学
大学院 システム情報工学研究科コンピュータサイエ
ンス専攻, Dept. of Computer Science, University ofTsukuba.

語で記述された任意のプログラムが, Inoue らの書換えを一般化した変形により,MetaOCaml プログラムに変換できることを示す.
本稿の構成は以下の通りである. 2 章では, 本研究の背景であるマルチステージ・プログラミングについCaml でのマルチステージ・プログラミングについてて述べる. 3 章では, マルチステージ・プログラミン

説明する. MetaOCaml は OCaml に対するマルチス

グによるモジュールの生成を概観し, 本研究の立場・テージ・プログラミングのための拡張言語であり, 擬

目的を明らかにする. 4 章では, モジュールの生成が似引用 (Quasi-quotation) 方式によるマルチステージ

可能なマルチステージ言語の実現方針について述べ言語である.

る. 5 章では, 本研究で提案するマルチステージ言語

λ

⟨M ⟩

についての概略を述べる. 6 章では, λ

⟨M ⟩

に対

する型システムの設計などについて明らかにする. 7
章では, λ⟨M ⟩から MetaOCaml への変換について述

MetaOCaml は 3 種類のマルチステージ構成子によってマルチステージ・プログラミングを実現している.

• コードの生成 .<e>.

べ, モジュールの生成が可能なマルチステージ言語の式 ブラケット.<>.で括ることで, コードが生成実現手法を明らかにする. 8 章では本研究の内容とそされる. コード化された式は現在の段階では評価の成果について総括する. また今後の課題についてもされず, そのままの形で保持される. 例えば, 式

述べる.

1 + 2を評価すると 3という結果が得られるが, 式.<1 + 2>.という式を評価しても, .<>.の中身は2 マルチステージ・プログラミング
マルチステージ・プログラミングは, プログラムを評価されず, .<1 + 2>.という評価結果になる.

• コードの合成 .~e

生成する段階・生成したプログラムを実行する段階とブラケット中の式 .~e は, 式 eを評価して得らいったようにプログラムの実行が複数の段階 (ステーれるコードをブラケットの中に埋め込む. let xジ) を持つという特徴を持つ. 保守性・再利用性の高= .<1>. in .<.~x + 2>.という式の評価結果はい形でプログラムを生成するプログラムであるプロ.~xの箇所に.<1>.というコードの中身が展開さ

グラム生成器を記述し, 記述したプログラム生成器かれ, .<1 + 2>.という評価結果となる.

ら対象領域に関する知識や実行環境などのパラメー• コードの実行 !.e

タに特化した実行効率の良いプログラムを生成・利式 !.e は式 eを評価して得られるコードを実用することで, プログラムの保守性・再利用性と実行

行する. 式 !.(.<1 + 2>.)の評価結果はコード効率を両立させることができる. 本論文ではプログラ.<1 + 2>.の中身が評価され, 3という評価結果とム生成器が生成する値としてのプログラム片を, 通常なる.

のプログラムと区別してコードと呼ぶことにする. マ
ルチステージ・プログラミングの利点としてプログ

3 モジュールの生成

ラム生成器によって生成されるコードが構文エラー・

MetaOCaml のモジュールにはモジュールの境界

自由変数への参照・型の不整合などを含まないことがを越えたメンバ参照 (間接参照) に関して実行時オー型システムによって静的に保証されるという点が挙バーヘッドが存在する. 例えば効率の良い SQL 問いげられる. 型システムによる保証のないコード生成で合わせを生成するための言語統合クエリ (LINQ) には, 生成されたコードの安全性に関する問題がコード関する研究 [3] では, 再帰モジュールを用いてモジューが実行される段階になって表面化するために, エラー

ルの内部メンバを膨大な回数参照するプログラムがの発見が遅れてしまいデバッグが難しくなるという問用いられており, 間接参照にかかるコストは非常に小題がある. 生成されるコードの安全性に関する型シス

さいながらも, その回数が膨大になるとオーバーヘッテムによるサポートが受けられるプログラム言語とドが累積して無視できないものになる.

して MetaOCaml, Scala LMS などがある.

ソースコード 1 は MetaOCaml のモジュールを用本研究で提案するマルチステージ言語は MetaO-

いた集合型を表現するモジュールの素朴な実装例でCaml をその基盤としているため, 本節では MetaO-

ある. MetaOCaml (OCaml) ではモジュールの型をsig ... end で, モジュールの実装を struct ... end でログラミングによって実現したい.

記述する. モジュール型 EQ は等しさが定義できるような型の表現, MakeSet は EQ 型のモジュール Eq を受けとって, Eq.t 型の値を要素とするとうな集合型を作るモジュールである. MakeSet は引数にモジュー
ルを取るモジュール (モジュール上の関数) になっており, このようなモジュールを特にファンクターと呼ぶ. IntSet は MakeSet を用いて作成した int 型の要

1
2
3
4
5
6
7
8

module IntSet = structtype elt = int
type set = int list
let member = elt = function| [] -> false| elt ’ : : set ’ - >( = ) e l t elt ’ | | m e m b e r e l t elt ’end

素を持つ集合型の実装である.

ソースコード 2: 効率化されたモジュール

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

ソースコード 3 は Inoue らの手法を用いた擬似的module type EQ = sig
type tval eq: t -> t -> boolend
module type SET = sig
type elt
type setval member: (elt -> set -> bool)end
module MakeSet (Eq: EQ): SET with type t = Eq.t =structtype elt = Eq.t
type set = Eq.t list
let member elt = function| [] -> false| elt ’ : : set ’ - >E q . e q e l t elt ’ | | m e m b e r e l t set ’endmodule IntSet = MakeSet (structtype t = int
let eq = (=)end)

ソースコード 1: 間接参照を含むプログラム

このプログラムは 11 行目で Eq.eq という間接参照を含んでいる. この間接参照は最大で集合の要素数だけ呼ばれるため, 間接参照のオーバーヘッドが累積する問題のあるプログラム例になっている.
間接参照を除去した結果のプログラムがソースコー
ド 2 である. ソースコード 1 の 11 行目に対応する箇所がソースコード 27 行目であり, 間接参照 Eq.eq が展開されて, 参照先のプログラムである (=) で置き換えられている. このような展開をマルチステージ・プ

モジュール生成を用いた間接参照の除去を行うプロ
グラムである. モジュールの境界を越えて参照される

Eq.eq 関数をコードとして保持しておき, 参照先でそのコードを展開することでソースコード 2 のようなプログラムを生成する. Eq.eq という間接参照はコードを生成する時に一度行われるのみとなり, 生成されたコードからは間接参照を完全に除去することができる.
ソースコード 3 はソースコード 1 とのギャップが大きい. 特に MakeSet モジュールが受けとる引数の型
が EQ CODE という新しいモジュール型に変わってしまっており, EQ 型の要素を再利用できなくなってしまっている点が問題である.

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

module type EQ_CODE = sig
type tval eq: (t -> t -> bool) codeend
module type SET = sig
type elt
type setval member: (elt -> set -> bool)end
let makeSet (type a)(module Eq: EQ_CODE with type t = a) =(module structtype elt = Eq.t
type set = Eq.t list
let member = Runcode.run. <l e t r e c m e m b e r e l t = f u n c t i o n| [] -> false| elt ’ : : set ’ - >

22
23
24
25
26
27
28
29
30

. ~ ( E q . e q ) e l t elt ’| | m e m b e r e l t set ’
i n member > .
end: SET with type elt = a)module IntSet =(val makeSet (module structtype t = int
l e t e q = . <(=) >.
end: EQ_CODE with type t = int))

25
26
27
28
29

module IntSet =r u n _ m o d u l e ( v a l m a k e S e t . <(m o d u l e
structtype t = int
let eq = (=)
e n d : E Q w i t h t y p e t = i n t ) >.)ソースコード 4: 提案するマルチステージ言語を用いた間接参照の除去

ソースコード 3: MetaOCaml を用いた間接参照の除去

4 本研究のアイデア
本研究ではソースコード 1 とのギャップの少ない,

Inoue らによる第一級モジュールを用いた擬似的なモジュールの生成を自然に記述できる表層構文を提案

モジュールコードの生成を観察することにより, 「モする. ソースコード 4 は提案するマルチステージ言語

ジュールのコード」と「コードからなるモジュール」

を用いて記述したものである. 提案言語を用いることが同型であるため, 前者で記述したプログラムを後者

で, 元々の EQ モジュール型に code という型構成子に変換すればよいという観察に至った. これを詳しくを付けて再利用できるようになっており, Inoue らの説明する.

手法をそのまま適用した場合と比べてプログラムの

図 1 は、モジュールのコードの型 (左) とコードをメ

再利用性が向上している. また, ソースコード 1 のプンバとして持つモジュールの型 (右) を表す. これらのログラムをソースコード 4 のプログラムに変換する

型の自然な解釈のもとでは, 両者は全単射で対応する

ためには, マルチステージプログラミングのための構集合として解釈され, 型として同型であると考えられ成子を挿入する必要があるが，これは部分計算における。MetaOCaml では直積型に対して (A ∗ B) code

る束縛時解析の手法で容易に実行できる.

と (A code) ∗ (B code) は同型であると考えらえ, 図

1 は直積型をモジュール型に一般化したものである.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

module type EQ = sig
type tval eq: t -> t -> boolend
module type SET = sig
type elt
type setval member: (elt -> set -> bool)
end

(sig

sig

type t = int

type t = int

val v1 : t

val v1 : t codeval v2 : t → tval v2 : (t → t) codeend) codeend

図 1: 左: モジュール・コードの型, 右: コードの要素
let makeSet (type a)(module Eq: (EQ with type t = a) code) =. <(m o d u l e s t r u c t
t y p e e l t = %( ⇓E q ) . t
t y p e s e t = %( ⇓E q ) . t l i s t
let member elt = function| [] -> false| elt ’ : : set ’ - >. ~ ( ( ⇓ E q ) . e q ) e l t elt ’| | m e m b e r e l t set ’e n d : S E T w i t h t y p e e l t = a ) >.

を含むモジュールの型
現在の MetaOCaml では, 図 1 の左側の型は表現できない一方で, 右側の型は表現可能である. そこで本研究では上記の対応に基づき, 左側の型の要素を右側の型の要素に変換する. これはモジュール・コードの生成が可能なマルチステージ言語をモジュール・コードの生成ができない MetaOCaml へ変換することに相当するというのが本研究の基本的なアイデアである. なお, 上記における「同型性」は, 圏論等における厳密に定式化された用語ではなく, 非形式的な意味

されていないために, モジュール・コードの内部メン論にもとづくものである.

バーを参照することができないという問題がある. 間

上記の変換で注意すべき点は, モジュールのメンバ

接参照の除去では, モジュール・コードの内部メンとしての型 t の具体的な型である int は変換していバーをコードという形で参照したい. そこで, 本研究ない (int code にしていない) 点である. これは型 tで行う変換を ⇓ という形で明示することで, コードのをコード型に変形してしまうと, たとえば図におけるモジュールを経由したモジュール・コードの内部メン

v2 の型が記述できなくなるためである.

バーの参照を可能にした.

また本研究では, 型の生成 (型をあらわすコードの本研究で提案するマルチステージ言語は性質の証明

生成) は許していないことにも注意されたい. 型 (のを簡単にするため, 2 段階のマルチステージ言語に制

コード) の生成を許す言語では, コード生成段階で使限している. またサブタイピングなどの複雑な要素をえる型の集合より, コード実行段階で使える型の集合

なるべく排し, 必要最低限の構成となるように努めた.

が多くなる. コード生成前に, 生成されるコードの型

本研究で提案するマルチステージ言語はネストした

安全性を保証する MetaML 系統のマルチステージ言モジュールをサポートしない. この制限のために, 式語では, 型の生成を許すことは技術的に相当大きな困をモジュールの内部で利用できる式とモジュールの外難があると予想される. 一方で, 型の生成が絶対不可部で利用できる式の 2 階層に分割した. また, 変換の欠な (型の生成をおこなわない同等のプログラムが存都合から ((module M)-> (module N))code といったよ

在しない) プログラム効率化の具体例は見つけられてうな一級モジュール上の関数 (ファンクター) のコー

いない. そこで本研究では, 型の生成は扱わないこと

ドをサポートできないため, この制限のために, 型もとした. これによりモジュール・コードの生成を簡潔

Small Type と Large Type の 2 階層に分割している.

に扱うことができるようになるという利点があった.

直感的には Small Type は 現在の MetaOCaml で記述できる型, Large Type は現在の MetaOCaml では

5 提案するマルチステージ言語 λ⟨M ⟩記述できない可能性のある型である.

モジュールの生成が可能なマルチステージ言語には⇓ によるモジュール・コードの内部メンバーを参照

設計上の選択肢が幾つか存在するが, 本研究で提案すを考える上で, モジュール内部メンバーの依存性を考るマルチステージ言語 λ⟨M ⟩ では一級モジュールとマ

慮しなければならない点に注意されたい. 例えば モ

ルチステージ構成子を組み合わせてモジュール・コー

ジュール・コード .<(module struct val x : int =ドを記述するという設計を採用した. この方式の利点

0; val y : int = 1 + x end: sig .. end)>. におけは MetaOCaml にはこれらの機能が既に存在しておる y は, それより先に定義されたメンバーである x へり, MetaOCaml とのギャップが少ないこと (現在のの参照を含んでおり, このようなコードから y を素朴

MetaOCaml ではブラケットの中で一級モジュールをに取り出すと 1 + xという自由変数を含んだコードに記述するとコンパイル・エラーになる), 一級モジューなるという問題がある. 本研究の現段階ではこの依存ルを用いることでモジュール・コードやモジュール・性を考慮に入れていないシステムになっているが, こ

コードから生成されたモジュールを自然に扱うことがの問題は参照する可能性のある定義を全て let 束縛

できるということなどが挙げられる.

の形でコード内に挿入してしまうという手法で解決

本研究では 提案するマルチステージ言語に 新しできると考えている. この手法を用いると先程の問題

いマルチステージ構成子 ⇓ を導入している. こののあるコードは.<let x = 0 in 1 + x>. という形に

マルチステージ構成子はモジュール・コードをコー

なり, 自由変数への参照を含まない. この手法は生成ドのモジュールへと変換する働きをする, 本研究のされるコードを肥大化させてしまうが, 実際のプログ提案する同型性に基づく変換そのものを表している.

ラミングにおいては許容できる範囲だろうと予想しMetaOCaml ではコードの一部を取り出す操作は許ている. コードの肥大化を抑える工夫については将来

課題である.

て実装することで, モジュールの生成が可能なマルチ
ステージ言語を容易に実現できるというのが本研究6 型システムの利点である.

本研究では Leroy によるモジュールに対する型シ
ステム [2] を基盤とし, 一級モジュールやマルチステー

8 まとめと今後の課題

ジ構成子などに対する型付け規則を追加した型シス

本研究ではマルチステージ・プログラミングによテムの定義を行った. 型システムの完全な定義は付録

るモジュールの生成について検討し, モジュールのB に掲載した.

生成が可能なマルチステージ言語 λ⟨M ⟩ 及びそのシ

後述する MetaOCaml の変換について, 提案する型

ステムの設計を行った. λ⟨M ⟩ から 既存のマルチスシステムの上で以下のような理論的性質が成り立つ

テージ言語 MetaOCaml への変換を与え, 提案言語

ことが期待されるが, 現在これらの定理について具体の実現手法を示した. Inoue らによる研究論文で,的な証明は与えられていない.

MetaOCaml の既存の言語機能を用いて擬似的にモジュールの生成を表現するプログラム手法が提案さ定理 6.1. 変換による型付けの保存 (レベル 0)

If

E ⊢0 e : τ,then

れているが, モジュールの生成を扱うようなプログラ
ムを MetaOCaml 上で表現するための具体的なエン

JEK0 ⊢0 JeK0 : Jτ K0

コーディングは与えられていない. 本研究は提案したモジュールの生成を扱えるようなマルチステージ言語

定理 6.2. 変換による型付けの保存 (レベル 1)から MetaOCaml 上の表現への具体的な変換アルゴ

If

E ⊢ e : τ,1then

リズムを定義した点に新規性がある.

JEK ⊢ JeK : Jτ K
1

1

1

1

今後の課題としてまず挙げられるのは, 提案体系の理論的性質, 特に進行性 (Progress) や型の保存性

7 MetaOCaml への変換
⟨M ⟩(Presevation) の証明である. 他には提案言語 λ⟨M ⟩から MetaOCaml への変換を J◦K ,から MetaOCaml への変換器を実装し, モジュール生J◦K として定義する. それぞれ λ⟨M ⟩ のレベル 0 の成の有効性を様々な例について確かめたいと考えてい提案体系 λ01項, レベル 1 の項に対応している. ◦ には λ

⟨M ⟩

の構

る. 現在の λ⟨M ⟩ は translucent signature, sharing,

文要素が入る. 変換の完全な定義は付録 C に掲載しsubtyping など現在のモジュール・システムでは広くている.

用いられている言語機能のいくつかをサポートして変換の設計はモジュール・コードとコードの要素を含んだモジュールの間の同型性に着目した. 変換の性いないので, それらについて拡張することも将来課題の一つである.

質として, それぞれのレベルに対する変換が型付けを保存することを念頭において設計を行っている. 変換後の λ⟨M ⟩ のプログラムは現在の MetaOCaml でコ
ンパイル可能である.
ソースコード 4 は λ⟨M ⟩ によるプログラム例である. このプログラムに対して変換を適用すると, Inoueらの手法による MetaOCaml プログラム (ソースコー
ド 3) が得られる. ソースコード 3 を実行することで,実行効率の改善されたプログラムであるソースコー
ド 2 が得られる.
本研究で提案する変換をソースコード変換器とし

参 考 文 献[1] Inoue, J., Kiselyov, O., and Kameyama, Y.: Staging Beyond Terms: Prospects and Challenges, Proceedings of the 2016 ACM SIGPLAN Workshop
on Partial Evaluation and Program Manipulation,
PEPM ’16, New York, NY, USA, ACM, 2016,
pp. 103–108.
[2] Leroy, X.: A Modular Module System, J. Funct.
Program., Vol. 10, No. 3(2000), pp. 269–303.
[3] Suzuki, K., Kiselyov, O., and Kameyama, Y.:
Finally, Safely-extensible and Eﬃcient Languageintegrated Query, Proceedings of the 2016 ACM
SIGPLAN Workshop on Partial Evaluation andProgram Manipulation, PEPM ’16, New York, NY,
USA, ACM, 2016, pp. 37–48.

付録 A λ⟨M ⟩ の抽象構文
抽象構文中の v, t はそれぞれ式, 型の変数を表すメタ変数である.
以降の議論ではマルチステージ構成子の. を省略して ⟨e⟩ や ˜ e と書く.

(Module types)

M::= sig S end(Signatures)S::= ϵ | C; S

(Signature components)C::= val v : σ | type t :: κ = σ(Typing environment)

E

::= ϵ
| E; (val v : τ )i

where i = 0, 1

| E; (type t :: κ = τ )(Kinds)κ::= ∗(Small Types)σ::= t | v.t | (⇓ v).t | σ → σ | σ code | %σ

(Large Types)τ::= σ | τ → τ | (module M ) | (module M ) code

提案するマルチステージ言語 λ⟨M ⟩型の抽象構文(Module expressions)m::= struct s end(Structures)s::= ϵ | c; s(Structure components)c::= val v : σ = e | type t :: κ = σ(Simple Expressions)e::= v | v.v | (⇓ v).v | fun (v : σ) → e | let v = e in e
| e @ e | ⟨e⟩ | ! e | ˜ e(General Expressions)g::= e | fun (v : τ ) → g | let v = g in g | g @ g | (module m : M )| ⟨g⟩ | module run g

提案するマルチステージ言語 λ⟨M ⟩式の抽象構文

付録 B λ⟨M ⟩ の型システム
付録 B. 1型に関する規則E ⊢ M wf
E wf
E ⊢ S wf
E ⊢ (sig S end) wf

E ⊢i S wf
E wf
E ⊢ ϵ wf

(2)

(1)

E ⊢ τ :: κE ⊢ S wfv ̸∈ Dom(E)E ⊢ (val v : σ; S) wf
E ⊢ τ :: κE; (type t :: κ = σ) ⊢ S wf

(3)t ̸∈ Dom(E)E ⊢ (type t :: κ = σ; S) wf

E ⊢ τ :: κandE ⊢ σ :: κ
E = E1 ; (type t :: κ = τ ); E2
E ⊢ t :: κ

E = E1 ; (val v : (module (sig S end))); E2
E ⊢ v.t :: κ

E = E1 ; (val v : (module M ) code)0 ; E2

(5)

S = S1 ; (type t :: κ = σ); S2

E ⊢ σ1 :: ∗E ⊢ σ2 :: ∗E ⊢ (σ1 → σ2 ) :: ∗E ⊢ σ :: ∗E ⊢ σ code :: ∗付録 B. 2(8)(9)

E ⊢ M wf
E ⊢ (module M ) :: ∗

and

(6)

(⇓ (module M ) code) = sig S1 ; (type t :: κ = σ code); S2 end
E ⊢ (⇓ v).t :: κ

⇓M

(4)

(10)

E ⊢ M wf
E ⊢ (module M ) code :: ∗(11)

E ⊢ τ1 :: ∗E ⊢ τ2 :: ∗E ⊢ (τ1 → τ2 ) :: ∗

(12)

⇓C
⇓ (sig C1 ; ...; Cn end)=

(sig ⇓ C1 ; ...; ⇓ Cn end)

⇓ (val v : σ)=val v : σ code

⇓ (type t :: κ = τ )=type t :: κ = τ

式に関する規則E ⊢i m : M
E ⊢i s : S
E ⊢i (struct s end) : (sig S end)

E ⊢i s : S

E ⊢i ϵ : ϵ

(14)

(13)

(7)

E ⊢i e : τE ⊢ σ :: κE; (val v : σ)i ⊢i s : Sv ̸∈ Dom(E)E ⊢i (val v : σ = e; s) : (val v : σ; S)
E; (type t :: κ = σ) ⊢i s : S

t ̸∈ Dom(E)

(15)

(16)

E ⊢i (type t :: κ = σ; s) : (type t :: κ = σ; S)E ⊢i e : σ
E = E1 ; (val v : σ)i ; E2
E ⊢i v : σ
E ⊢0 v1 : (module sig S end)

(17)

S = S1 ; (val v2 : σ); S2

E ⊢0 v1 .v2 : σ {t ← v1 .t | t ∈ Dom(S1 )}E = E1 ; (val v1 : (module M ) code)0 ; E2(⇓ (module M ) code) = sig S1 ; (val v2 : σ code); S2 end

E ⊢0 (⇓ v1 ).v2 : σ codeE ⊢ σ1 :: κE; (val v : σ1 )i ⊢i e : σ2

E ⊢i (fun (v : σ1 ) → e) : (σ1 → σ2 )E ⊢i e1 : σ1 → σ2

E ⊢i e2 : σ1

E ⊢i e1 @ e2 : σ2
E ⊢i e1 : σ1

E; (val v : σ1 )i ⊢i e2 : σ2

E ⊢i let v = e1 in e2 : σ2
E ⊢1 e : σE ⊢0 ⟨e⟩ : σ code(23)

E ⊢0 e : σ codeE ⊢1 .˜ e : σ(24)

E ⊢0 e : σ code
E ⊢0 ! e : σ

(25)

(20)

(21)

(22)

E ⊢i g : τ
E = E1 ; (val v : τ )i ; E2
E ⊢i v : τE ⊢ τ1 :: κ(26)E; (val v : τ1 )i ⊢i g : τ2

E ⊢i (fun (v : τ1 ) → g) : (τ1 → τ2 )E ⊢i g 1 : τ 1 → τ 2
E ⊢i gE ⊢i g 1 : τ 1(18)

E ⊢i g 2 : τ 1

1 @ g2 : τ 2

E; (val v : τ1 )i ⊢i e2 : τ2

E ⊢i let v = g

1 in g2 : τ2

(27)

(28)

(29)

(19)

E ⊢1 g : (module M )E ⊢0 ⟨g⟩ : (module M ) code(30)

E ⊢0 g : (module M ) code
E ⊢0 module run g : (module M )(31)

付録 C λ⟨M ⟩ から MetaOCaml への変換

JM K0
Jsig C1 ; ... ; Cn endK0=

sig JC1 K0 ; ... ; JCn K0 end

Jval v : σK0=

val v : JσK0

Jtype t :: ∗ = σK0=

type t :: ∗ = JσK0

JtK0

=

t

0

Jv.tK

=

v.t

0

J(⇓ v).tK

=

v.t

0

Jσ1 → σ2 K=

Jσ1 K0 → Jσ2 K0

Jσ codeK0=

JσK0 code

JCK0

JσK0

Jτ K0
Jτ1 → τ2 K0=

Jτ1 K0 → Jτ2 K0

J(module M )K0=(module JM K0 )J(module M ) code K0=(module JM K1 )JmK0
Jstruct c1 ; ... ; cn endK0=

struct Jc1 K0 ; ... ; Jcn K0 end

Jval v : σ = eK0=

val v : JσK0 = JeK0

Jtype t :: κ = σK=type t :: κ = JσK0

JcK0

0

JeK0

JvK0

=

v

0

Jv1 .v2 K=v1 .v2J(⇓ v1 ).v2 K0=

v1 .v2

Jfun (v : σ) → eK0=

fun (v : JσK0 ) → JeK0

Je1 @ e2 K0=

Je1 K0 @ Je2 K0

Jlet v = e1 in e2 K0=

let v = Je1 K0 in Je2 K0J⟨e⟩K0=⟨JeK0 ⟩

J ! eK=! JeK00

JgK0
Jfun (v : τ ) → gK0=

fun (v : Jτ K0 ) → JgK0

Jg1 @ g2 K0=

Jg1 K0 @ Jg2 K0

Jlet v = g1 in g2 K0=

let v = Jg1 K0 in Jg2 K0

0

J(module m : M )K=

(module JmK0 : JM K0 )J⟨(module m : M )⟩K0=

(module JmK1 : JM K1 )J(module run g : M )K0=(付録 C. 1 を参照)

JM K1
Jsig C1 ; ... ; Cn endK1=

sig JC1 K1 ; ... ; JCn K1 end

Jval v : τ K1=

val v : Jτ K1 code

Jtype t :: ∗ = τ K1=

type t :: ∗ = Jτ K1

JtK1

=

t

1

Jv.tK

=

v.t

J(⇓ v).tK1

=

v.t

1

Jσ1 → σ2 K=

Jσ1 K1 → Jσ2 K1

J%σK1

=

JσK1

Jτ1 → τ2 K1=

Jτ1 K1 → Jτ2 K1

J(module M )K1=(module JM K1 )

JCK1

JσK1

Jτ K1

JmK1
Jstruct c1 ; ... ; cn endK1=

struct Jc1 K1 ; ... ; Jcn K1 end

Jval v : σ = eK1=

val v : JσK1 = ⟨JeK1 ⟩Jtype t :: κ = σK1=

type t :: κ = JσK1

JvK1

=

v

1

Jv1 .v2 K=v1 .v2

1J(⇓ v1 ).v2 K=v1 .v2

1

Jfun (v : σ) → eK=

fun (v : JσK1 ) → JeK1

Je1 @ e2 K1=

Je1 K1 @ Je2 K1

1

Jlet v = e1 in e2 K=

let v = Je1 K1 in Je2 K1J˜ eK1=

˜ JeK0Jfun (v : τ ) → gK1=

fun (v : Jτ K1 ) → JgK1

Jg1 @ g2 K1=

Jg1 K1 @ Jg2 K1

1

Jlet v = g1 in g2 K=

let v = Jg1 K1 in Jg2 K1

J(module m : M )K1=(module JmK1 : JM K1 )

JcK1

JeK1

JgK1

付録 C. 1 module run の変換

module run はモジュール・コードの実行を行うためのプリミティブであり, コードのモジュール内のval v : σ = e の形をした要素たちの右辺にコードの実行を表すマルチステージ構成子!を挿入する. このようなmodule run は, 単純な変換では実現することができない. 例えば, fun (v : (module M)code)-> module_runvという式中の m では module run の対象である v は変数なので, 関数に具体的なモジュール・コードが適用されるまで, !を挿入することができない.
そこで module run g という形の式に限り, module run の対象となる式 g の型を基に変換を行うことにする. g の型が module (sig type t; val v1 : σ1; val v2 : σ2 end)のとき, 以下のようなプログラムに変換
する.
J m o d u l e _ r u n g K0
= module struct
val g’ = ⇓ gval v1 = run g’.v1
val v2 = run g’.v2
end