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

自然結合制約を含む型推論アルゴリズムの実装方式
佐々木 智啓

上野 雄大

大堀 淳

本稿では，型付き関数型言語のコンパイラに自然結合演算を加える実装方式について報告する．自然結合は強力なレコード演算のひとつであり，関係データベースにおける基本演算のひとつでもある．レコードを含む型付き言語が自然結合をサポートするならば，より柔軟かつ記述力の高いレコード処理が書けるようになるとともに，SQL とのより高い親和性も実現できると期待できる．この目的のため，著者らは SML#に自然結合演算を加え，その型推論器を実装した．本稿では，まず自然結合を含む型システムの概要を紹介したのち，行った実装の詳細と利用例を報告し，今後の展望について述べる．

文献 [1] によれば，自然結合演算は 2 つの値の上限を1 はじめに計算する演算の特殊な場合であると解釈できる．し自然結合は関係代数において部分的な 2 つの記述たがって，適切な順序関係を定められるならば，関係を統合する演算と解釈できる．関係データベースにおデータベース以外の処理系でも自然結合演算を提供いては 2 つのテーブルを結合する基本演算のひとつできるはずである．

として提供されている．以下は関係データベース上での自然結合演算 ◃▹ の例である．

この一般化された自然結合演算を ML 系関数型言語に組み込みの演算として提供できるならば，複雑なデータを取り扱うプログラムをより効率よく記述でき

名前idid給料

るようになり，ML 系関数型言語の可能性を大きく広太郎

11450

げると期待できる．また，提供された演算と SQL の花子

22500

ML への統合方式 [5] を組み合わせれば，SQL の自然一郎

34700

結合を ML に型付きで統合することも可能である．

◃▹自然結合演算の ML 系関数型言語への組み込みに

=

名前id

給料

向け，著者らは自然結合演算を含む ML の型システ

太郎

1450

ムの開発に取り組んできた [7]．この型システムは文花子

2500

献 [3] の型システムをベースとして作られている．また，LET 多相などの文献 [3] の型システムで扱っていない箇所を補うために，HM(X) 型システム [2] の制約

An implementation method of type inference algorithm including natural join constraints
Tomohiro Sasaki, 東 北 大 学 大 学 院 情 報 科 学 研 究 科,
Graduate School of Information Sciences, Tohoku
University.
Katsuhiro Ueno, Atsushi Ohori, 東北大学電気通信研究所, Research Institute of Electrical Communication
Tohoku University.

を型システムに加える考え方を加えて導入している．
文献 [7] で示した型システムは従来の ML 系型システ
ムとほぼ直行しており，ML 系型システムを採用する実際のコンパイラに容易に実装できると思われる．
著者らは文献 [7] の型システムを SML# コンパイ
ラ 3.1.0 版 [8] を拡張することで実装した．実装の過程では文献 [7] で述べられていない種々の課題が発生した．その主要な要因はランク 1 多相性である．ラ

2 自然結合演算の型付け

ンク 1 多相型をうまく推論するために，SML#コン

本節では，文献 [7] が提案する自然結合演算に関す

パイラの型推論アルゴリズムは様々な構文の型推論る制約ベースの型システムの概要を述べる．

時に多相型に対する多様な処理を行なっている．今回

型付け規則を自然結合制約で拡張するために，自実装する型システムでは，多相型は束縛する型変数

然結合制約の導入，型ジャッジメントの拡張，多相型に閉じた制約も束縛している．したがって，変数式，の拡張が行われた．自然結合制約はオペランドと結LET 式，JOIN 式のみで制約を取り扱うのではなく，果の関係を示し，その形は τ = τ ⊔ τ の形である．型

多くの箇所で制約を取り扱う必要があった．本稿ではジャッジメントは型環境 Γ と式 e から型 τ を導出す

文献 [7] で提案された型推論器の実装と技術的な課題

る形を制約集合 C で拡張し，C, Γ ⊢ e : τ の形で示すの詳細を報告する．

ようにした．多相型 σ は束縛した変数に閉じている

自然結合を SML#に導入する具体的な内容は，以下の構文を加えることである．

join(e1 , e2 )この構文はレコード e1 と e2 を自然結合したレコー

制約集合を加え，∀t.C ⇒ τ の形で示すようにした．
式に対する型付け規則のうち，制約が関連するものは以下のように示された．
C, Γ ⊢ e1 : τ1C, Γ ⊢ e2 : τ2ドを表す．構文を完成させるためには型推論器とコー(τ = τ1 ⊔ τ2 ) ∈ Cド生成器の拡張が必須である．拡張した SML#コンC, Γ ⊢ join(e1 , e2 ) : τパイラはこの構文に文献 [7] で与えられた通りの多相型を与える．文献 [7] では型システムについては言及している一方，多相的な自然結合の評価モデルの構築は将来の課題としている．そのため現段階では結果のレコードを計算するコード生成は未実装であり，この構文を実行すると例外が発生するようにしている．

SQL を ML に統合する際に必要となる toy term の生成にはこれで十分であり，したがって自然結合を含む SQL クエリの ML への統合は可能である．以上の機能を実現するため，SML#コンパイラの型推論器までのフェーズを拡張した．
行った拡張はほぼ型推論器で閉じている．本稿では

SML#の型推論器に制約に基づく型規則を導入するための方針とその実装の詳細を述べる．さらに，本稿では，より完全な自然結合演算の ML への統合に向けた展望を述べる．
本稿の構成は以下の通りである．2 節では文献 [7]の型システムの概略を述べる．3 節では SML#におけるランク 1 多相性の概略を述べる．4 節では型システムの SML#コンパイラへの実装の詳細を述べる．

5 節で結論と今後の展望，特により完全な自然結合演
算の ML への統合に向けた課題を述べる．

C1 ∪ C2 , Γ ⊢ e1 : τ1C1 , Γ{x : ∀t.C2 ⇒ τ } ⊢ e2 : τ(F T V (Γ) ∪ F T V (C1 )) ∩ t = ∅, F T V (C2 ) ⊆ t
C1 , Γ ⊢ let x = e1 in e2 : τ
変数 x に対する型付け規則は x に対応する多相型に閉じている制約集合をインスタンス化し，インスタンス化された制約集合が型ジャッジメントにおける制約集合の部分集合であるという条件を加えている．
文献中に示された自然結合制約で型推論アルゴリズムを拡張するためのアイデアを以下に述べる．まず，制約集合はグローバルなものとみなす．そのため，LET 式のケースで閉じている制約を多相型に束縛させる場合を除き，制約集合は常に和をとる．また，制約が増えるのは JOIN 式または変数式のみである．得られる制約集合は LET 式の型推論時に解き，トップレベルが LET 式以外の式は等価な LET 式とみなすことでトップレベルで制約を解くようにする．
また，制約集合を解く場合も計算時間の増加を抑えるためにオペランドの型に自由変数が存在しない制約のみを解く．LET 式のケースで多相型に束縛しない変数は型環境 Γ から制約集合 C をたどって到達できる変数とする．

ンパイラの型推論器におけるランク 1 多相性の扱い

3 ランク 1 多相性に触れた上で，型推論器の主な変更点と，実装後の型SML#コンパイラが採用するランク 1 多相性を持推論器を用いた型推論の例を述べる．

つ型システムは文献 [6] に示されている型システムをSML#コンパイラの型推論器は，ランク 1 多相性基としている．また，SML#におけるランク 1 多相のに関してはおおむね文献 [6] で示されたアルゴリズム

概略は SML#のマニュアルにも記述されている．本をそのまま実装している．型推論器内では多相型に節では，4 節を読む上で前提となる，SML#コンパイ対する処理は大まかに generalization，instantiation，ラが採用する型システムの概略を述べる．

coercion に分けられ，型推論器中の様々な箇所に発SML#コンパイラで扱う単相型 τ ，多相型 σ はそれぞれ以下のように定義される．

τ::=t | b | τ → τ | ···σ::=

τ | ∀t.σ | τ → σ | · · ·生する．ここで，coercion は多相型を部分に含む型を等価な型にする処理の SML#コンパイラ内での呼び方である．これらの説明と変更点を以下で述べる．

generalization は与えられた型に閉じている型変数多相型が部分型に現れるため，多相型の生成が LETを束縛し，多相型を作る処理である．演算を行わない式のみではなく関数抽象式でも行われる．

関数式等の式，LET 式の型推論時に多相型を生成す

ランク 1 多相性を導入することで従来の型システる際に行われる．閉じている型変数の導出は与えられムから大きく変わる関数適用式について述べる．このた型から到達可能な型変数から，型環境から到達可能型システムにおける関数適用式の型付け規則を以下な型変数を除外することで行う．に示す．

generalization に対しては，以下の 2 つの変更をΓ ⊢ e1 : τ → σΓ ⊢ e2 : τΓ ⊢ e1 e2 : σ
これを踏まえた上で関数適用式 e1 e2 に対する型推論
アルゴリズム W で起こることを述べる．まず，式 e1に対し W を適用し，e1 の型 σ1 を得る．型付け規則から，なんらかの τ1 ，σ2 に対し，σ1 と τ1 → σ2 を単一化する必要がある．従来の単一化アルゴリズム Uは多相型に対して適用できず，単一化対象の型にも多相型が含まれているため，U を用いる以外の手段で単一化する必要がある．提案された型推論アルゴリ
ズムでは，σ1 の形に応じて型の一部分をインスタンス化することで単一化としている．また，式 e2 に対し W を適用し，得られた e2 の型 σ3 の fresh な型変数による単相型のインスタンス τ2 を生成し，τ1 と τ2の単一化を行なっている．

4 型推論アルゴリズムの実装行った．まず，多相型で束縛するものはその中に閉じているという性質の保持のために，導出時に現在の制約集合もたどるよう変更した．また，多相型では束縛した変数に閉じている制約も束縛しているため，現在の制約集合中から束縛対象の変数に閉じている制約も導出す 1 るよう変更した．

instantiation は多相型が束縛している型変数に新しい型変数を割り当て，単相型とする処理である．変数の型推論時や U を使用するために多相型のインスタンスを生成する際に行われる．新しい型変数の割り当ては，束縛している型変数から新しい型変数への代入を作成し，その代入を適用することで行う．

instantiation に対しては，インスタンス化対象の多相型が束縛している制約を制約集合に追加する変更を行った．多相型で束縛している制約も満たすべき制約であるため，束縛している制約にも作成した代入を適用し，制約集合に追加するよう変更した．

著者らは文献 [7] で提案された自然結合制約を含む型推論アルゴリズムを SML#コンパイラの型推論器を拡張することで実装した．3 節で述べたランク 1 多相性により，提案されたアルゴリズムでそのまま型推論器を拡張することはできない．本節では，SML#コ

coercion はある型を型推論を進める上で必要な型に一致させる処理である．3 節で述べた関数適用式の型推論時のように，部分に含まれる多相型を等価な単相型に変換する処理も行われる．

coercion に対しては，変換される型が多相型の場

合，その多相型に含まれる制約も満たすべき制約で推論アルゴリズムに対する自然結合制約による拡張はあるので，この制約も制約集合に追加するよう変更

そのアルゴリズムの性質によっては文献で言及されてした．

いる以外の課題が存在するが，拡張を適切に行えば実また，提案されたアルゴリズムでは LET 式及び現できる．また，型推論器の拡張による変更の範囲はトップレベルで制約を解くようにしていた．アルゴリ

ほぼ型推論器の実装に閉じていることが確認できた．

ズムの方針に従った上で多相型が制約を束縛する前に実際に SML#コンパイラの型推論器を自然結合制約制約を解かせるため，generalization 前とトップレベで拡張した例を報告し，利用可能であることも確認でルに制約を解く処理を追加した．

きた．

最後に，実装後の型推論の実例を示す．まず，SQL今後の課題は自然結合の計算を実現することであの自然結合に型付けした例を示す．SML#は SQL をる．一般化された自然結合の意味は文献 [1] で示されプログラムへ統合する機能を有しており，この機能にている．自然結合を言語に導入する観点では文献 [4]自然結合を追加した．対話型モードで SQL の自然結で導入の概略が示されている．一方で，これらを現実合の型を推論したものを以下に示す．のコンパイラへ導入するには型主導コンパイルにお# _sql db =>ける扱いといった種々の課題が存在する．

>

select #t.name, #t.age>

from (#db.t1 natural join #db.t2) as t;val it = fn
: [’a#{t1: ’b, t2: ’c}, ’b#{}, ’c#{},’d, ’e, ’f, ’g,

謝辞 本研究の一部は JSPS 科研費 25280019「ML系多相型言語 SML#の実用化技術に関する基礎研究」
および 15K15964「実用プログラミング言語のための系統的言語開発基盤の実現」の助成を受けて実施されたものである．

’h#{age: ’f, name: ’d}.
(’h = ’b join ’c) =>参 考 文 献’a db -> (’d * ’f) query][1] Buneman, P., Jung, A., and Ohori, A.: Using
Powerdomains to Generalize Relational Databases,
Theoretical Computer Science, Vol. 91, No. 1(1991),pp. 23–56.
[2] Odersky, M., Sulzmann, M., and Wehr, M.: Type
Inference with Constrained Types, Theor. Pract.
Object Syst., Vol. 5, No. 1(1999), pp. 35–55.
[3] Ohori, A. and Buneman, P.: Type Inference ina Database Programming Language, Proceedings ofthe 1988 ACM Conference on LISP and Functional
Programming, LFP ’88, New York, NY, USA, ACM,
1988, pp. 174–183.
[4] Ohori, A., Buneman, P., and Breazu-Tannen, V.:
Database Programming in Machiavelli&Mdash;aPolymorphic Language with Static Type Inference,
Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, SIGMOD ’89, New York, NY, USA, ACM, 1989,pp. 46–57.
[5] Ohori, A. and Ueno, K.: Making Standard MLa Practical Database Programming Language, Proceedings of the 16th ACM SIGPLAN International
Conference on Functional Programming, ICFP ’11,
New York, NY, USA, ACM, 2011, pp. 307–319.
[6] Ohori, A. and Yoshida, N.: Type Inference with
Rank 1 Polymorphism for Type-directed Compilation of ML, SIGPLAN Not., Vol. 34, No. 9(1999),

推論結果の型は，データベース db は少なくとも 2 つのテーブル t1 と t2 を有しており，t1 と t2 の自然結合の結果は少なくとも 2 つの列 age と name を有することを示している．次に，制約を満たす型が存在しないが，型推論が行えてしまう例を以下に示す．

# fn (x, y) =>>(#a x ^ "a", #a y + 1, _join (x, y));val it = fn
: [’a#{a: string}, ’b#{a: int}, ’c#{}.
(’c = ’a join ’b) =>’a * ’b -> string * int * ’c]
このとき，制約を満たす x と y の型は存在しないが，制約の妥当性の確認はオペランドの自由変数が存在しなくなるまで行わないため型推論は行えてしまう．

5 まとめと今後の展望
本稿では，文献 [7] で報告している自然結合制約を含む型推論アルゴリズムの実装を報告した．既存の型

pp. 160–171.
[7] Sasaki, T., Ueno, K., and Ohori, A.: SML# with
Natural Join, ACM SIGPLAN Workshop on ML,

2016. to appear.
[8] SML# Compiler.
http://www.pllab.riec.tohoku.ac.jp/smlsharp/