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

暗黙に相互運用可能なレコードとハッシュテーブルのための型推論とコンパイル手法
梅木 孝輔 関山 太朗

五十嵐 淳

本論文では、型変換のための特殊な構文や実行時のデータ変換を必要とすることなくレコードとハッシュテーブルを相互運用するための型推論とコンパイル手法を提案する。この手法は Ohori の多相レコード計算の型推論とそのコ
ンパイル手法に基づいている。型推論については、レコードカインドの意味を拡張することで、型変換のための特殊な構文を導入せずにハッシュテーブルに対するレコード操作構文の適用やその逆を型付け可能とする。操作構文は、
アクセス対象がレコードかハッシュテーブルかを実行時に判定した上で、データ型に応じたアクセスを行うようコンパイルする。さらに、レコードアクセスに用いるインデックスに、アクセス対象がハッシュテーブルであることを表す特殊な値を導入することで、レコード操作のオーバーヘッドを軽減する。我々は、この手法を SML♯ コンパイラの拡張として実装し、その性能を評価する。

した多くの動的型付け言語でプリミティブな値とし1 はじめにてサポートされている。しかし、ハッシュテーブルのプログラミングにおいて、有限写像を表現するため操作は (最適化された) レコード操作に比べて実行時のデータ構造として、レコードとハッシュテーブルがコストが大きくなるという欠点がある。

知られている。多くの静的型付け言語に採用されてプログラミングの初期段階において、これらの有限いるレコードは、静的なラベルから値への有限写像を写像を表すデータ構造が事前に定まるのか、実行時に表し、ラベルと対応する値の型の組からなる構造を静しか定まらないのかを見極めることは難しく、結果的的に決定している。構造が静的に決定していることにレコードで十分な場合であったとしてもプロトタ

から、レコードにはメモリサイズのオーバーヘッドがイプの開発段階ではハッシュテーブルを用いること

小さく、操作の時間計算量が定数時間である、というがありうる。しかし、一般にデータ構造の変更による二つの利点がある。しかし、欠点としてレコードのリファクタリングはプログラムの大規模な書き換え

宣言時に保持する値の型や数を決定する必要がある。

につながりやすく、ハッシュテーブルからレコードへ

他方で、ハッシュテーブルは文字列などの動的なキーの移行の際にもプログラムを大きく変更する必要がから値への有限写像を表し、キーと値の組からなる構

生じる可能性が高い。

造が動的に決定できる。構造が動的に決定できるこ

本論文は、動的な構造であるハッシュテーブルととから、実行時にキーと値の追加や削除ができる利点

静的な構造であるレコードを、型システムの支援にがある。そのため JavaScript や Python をはじめとよって相互運用可能な言語を提案する。提案言語では静的なラベルを用いるレコード操作の構文を通しType Inference and Compilation for Implicitly Interoperable Records and Hash Tables.
Kosuke Umeki, Atsushi Igarashi, 京都大学 大学院情報学研究科, Graduate School of Informatics, Kyoto
University.
Taro Sekiyama, 国立情報学研究所, National Instituteof Informatics.

てハッシュテーブルを操作でき、動的なキーを用いる
ハッシュテーブル操作の構文を通してレコードを操作できる。この相互運用によって、開発の初期段階ではハッシュテーブルを用いたプロトタイピングを行
い、実装方針が固まり次第ハッシュテーブルとレコー

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

2

ドを宣言部分、操作部分と順番に置き換えることが可

案言語について説明する。第 4 節では、SML♯ での実能になる。この漸進的な置き換えによって、置き換え

装や、性能評価について説明する。第 5 節で関連研究る段階毎にコンパイルを行い、コンパイルエラーが起について、第 6 節でまとめと今後の課題を述べる。

きないことや、テストを通過することを都度確認する
サイクルを構成することができ、このようなサイクル

2 Ohori の多相レコード計算

によって、大規模なリファクタリングを一度に行うよ

本節では、背景として Ohori の多相レコード計算

り、バグを産まない移行ができると考えている。提案について述べる。なお、レコードと関わらない部分を言語では相互運用にあたってプログラマの負担を軽省略しているため、詳しい内容は [3] や [2] を参照さ減するため、特別な型注釈を必要としない暗黙的な相れたい。

互運用をサポートする。また実行時コストが小さい

ML 言語の 1 つの方言である Standard ML [1] は、というレコードの利点を活かすため、ハッシュテーブ

多相な型システムを備えたプログラミング言語であルとレコード間の実行時変換を伴わないような実装る。Standard ML では、レコードの操作として、レ方式を与える。

コードの作成、レコードの値を取り出す射影、これ

本研究の提案言語は ML 系言語の一つである SML♯ら 2 つの操作が定義される。これらの操作例を以下を拡張して与える。SML♯ の理論的基盤は Ohori のに示す。

多相レコード計算 [3] にあり、本論文が提案する言語

val r = {Name = "Alice"};の理論体系は、多相レコード計算を拡張する形で定式> val r = {Name = "Alice"}: {Name: string};

化する。この多相レコード計算の拡張では、実行時変#Name r;換を伴わない暗黙的な相互運用を実現するための型> val it = "Alice": string;

推論とコンパイル手法を与える。我々の理論体系は

しかし、レコードの射影操作には型づけに関する厳し

多相レコード計算の保守的な拡張となっており、ハッい制約が存在する。例えば、シュテーブルとレコード間の相互運用を利用しない

fun get_name(x) = #Name x;

限りにおいては多相レコード計算の型推論結果を変という get name 関数を考える。この関数は、レコー

えることはなく、型安全性などの性質も保持される。

ド x を変数として受け取り、x のレコードのうち、

一方ハッシュテーブルとレコードの相互運用を利用

Name ラベルに紐づく値を返すことを想定している。

した場合、型安全性はもはや成り立たない。例えば多しかし、Standard ML の型推論器は、レコード x が相レコード計算（より一般には、レコードをサポート持つべきラベルとその値の型を推測できない。従っする ML 系言語）では任意のラベル l によるレコーて、次のように、レコード x が持つ全てのラベルとそ

ドメンバアクセスは型検査が通れば必ず成功するが、の値の型を注釈として与える必要がある。

我々が提案する言語ではラベル l に相当するキーを含

fun get_name(x: {Name: string}) = #Name x;

まないハッシュテーブルに対してラベル l によるレ

しかし、この関数は最早 Name 以外のフィールドを

コードメンバアクセスが型付け可能となっており、実持つレコードに適用することができない。

行されると例外が送出される。

(* type error! *)♯我々は、この提案言語を SML の拡張として実装した。相互運用が可能なよう拡張した SML♯ について性能の予備評価を行った。

get_name {Name="Alice", Age=7}
このようなレコード操作に関わる制限の解決として

Ohori は多相レコード計算とその効率的なコンパイ
ル手法 [3] を提案し、SML♯ [10] として実装している。

1. 1 本論文の構成

Ohori の多相レコード計算の主要なアイデアは、射影

第 2 節では、本研究の背景である Ohori の多相レ

操作 #Name の自然な対象である「少なくとも Name

コード計算について簡単に説明する。第 3 節では提フィールドを持つレコード型」を多相性の一種として

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集型システムにおいて表現することにある。また、型情3

τ2 → τ1 型」を意味する。

報をうまく用いることで、レコードを値の並んだ配列

この直感を定式化する。図 2 に、 λlet, の項と型、に、レコードのラベルから値を得る操作を単なる配列

カインドの定義を示す。カインドと型の定義は 3 つの添字アクセス操作にコンパイルすることができる。

の言語共通である。

以下、Ohori の多相レコード計算とそのコンパイ

e は式のメタ変数である。cb は、b 型のリテラルをル手法の概略を示す。Ohori の枠組みは 3 つの言語表している。e l はレコードへのラベルによる射影を

let,

λ

,∆

let,

let,

語、 ∆

,λ

let,[]から成り立つ。 λlet,[]

は中間言語、 λ

let,

は表面言

表す。τ は単相型の集合である。注意すべき点としはターゲット言語でて、型とカインドに現れる l : τ については、ラベルある。 λlet, に型推論を行い、コンパイルに必要な型の重複がないものとする。また、出現順のみが違うふ注釈を行ったのが ∆let, である。 ∆let, の型注釈をたつの型・カインドは同一視する。b は基底型、t は参照し、コンパイルを行った後の言語が λる。以降、表面言語 λlet,let,[]

であと型システム、型推論アル

ゴリズム、コンパイルアルゴリズムの順に示す。

型変数を表し、σ は単相型から構築される型スキームを表す。
図 3 に、Ohori の 3 つの言語での、カインドとカイ
ンド付け規則を示す。

2. 1 表面言語 λlet, と型システム

U は全ての型につけることが出来るカインドであOhori の多相レコード計算では、あるラベルと値のる。また、{{l1 : τ1 , · · · , ln : τn }} はレコードカイン

型の組は存在するが、他の組の存在に言及しない、多ドであり、少なくとも、l1 : τ1 ...ln : τn のラベルと相なレコード型を表現するために、カインドという仕値の型の構造を持つレコード型に与えられる。“σ組みを用いる。カインドとは、「型の型」や「型の種」

is well formed under K” とは、σ 内に出現する自由と表現される概念である。型とは値を分類するものでな型変数が、K の定義域に入っていることを意味すあったが、これと対応し、カインドは型を分類する。

る。ok init は、ある型変数 t がレコードカインド

カインドが型を分類することは、カインドのメタ変数{{l1 : τ1 , .... , ln : τn , ... }} を持つ場合、そのレコード

k 、単相型のメタ変数 τ 、型変数からカインドへの写

カインドの構造の部分集合となる構造を持つレコー

像を表すカインド環境 K を導入し、K ` τ :: k と表ドカインド {{l1 : τ1 , .... , ln : τn }} を、型変数 t に付記する。

けて良いことを表す。ok gen は、あるレコード型

ここで、ラベルのメタ変数 l を用いてレコード型{l1 : τ1 , .... , ln : τn , ... } が well formed であるなら{l1 : τ1 , .... , ln : τn } を定義する。このレコード型やば、そのレコード型の構造の部分集合を持つレコード

型変数 t に対して、レコードカインド {{l : τ }} とは、

カインド {{l1 : τ1 , .... , ln : τn }} をレコード型に付けて「l のラベルと値の型 τ の構造を少なくとも持つ」レ

良いことを表す。

コードを表す。したがって、直感としては、レコード
へのカインド付けは図 1 のようになる。

λlet, の特徴的な型付け規則として、レコードの値の射影に関する規則を図 4 に示す。この規則は、e の

このカインド付けに従うと、序論の例で挙げた型としてレコード型を直接要求するのではなく、型 τ1

get name 関数には、型変数 t を導入して、次のような型スキーム †1 が与えられる。

が付くことを要求する。そのうえで、τ1 に {{l : τ2 }}get name : ∀t1 :: U .∀t2 :: {{Name : string}}. t2 → t1

くとも l : τ2 のフィールドを持つようなレコード型を

この型スキームは「任意の型 τ1 、カインド {{Name : τ1 }}

要求することができる。

カインドが付くことを要求する。これによって、少なを持つ任意の型 τ2 (すなわち、少なくとも Name : τ1
フ ィ ー ル ド を 持 つ 任 意 の レ コ ー ド 型 τ2 ) に 対 し 、

2. 2 型推論とコンパイル
Ohori の多相レコード計算では、2. 1 節で定義した†1 U は「全ての型」を表す特殊なカインドである。

表面言語 λlet, を、ターゲット言語 λlet,[] に変換す

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

4(∗Valid∗){Name : string} :: {{Name : string}}{Name : string, Age : int} :: {{Name : string}}{Name : string, Age : int} :: {{Name : string, Age : int}}{Name : string, Age : int} :: {{Age : int}}(∗Invalid∗){Name : string} :: {{Name : string, Age : int}}
図1

レコードカインドのカインド付けの例

一化 [7] を拡張した、カインド付け単一化 U を導入

e : expression x : variable

する。カインド付け単一化アルゴリズムの一部を図 5l : label t : type variable b : base typeに示す。

e ::= x | cb | λx .e | e e | let x = e in e

カインド付け単一化アルゴリズム U は、型の等式集| {l = e, · · · , l = e} | e l

合 E 、カインド環境 K、等式を解いた結果得られる型

τ ::= t | b | τ → τ | {l : τ, · · · , l : τ }代入 S 、(必ずしも well-formed とは限らない) カイン

σ ::= τ | ∀ t :: k .σ

ド環境 SK の四つ組を入力とする。SK は U の正し

k ::= U | {{l : τ, · · · , l : τ }}図2さの証明のために用いられるだけなので、無視してよい。このアルゴリズムは、初期状態として (E, K, ∅, ∅)λlet, の項と型 (一部抜粋)

を渡し、規則が適用できなくなるまで遷移する。遷る。この変換は、型情報のみを分析し、項の変換を行

移後の状態を (E ′ , K′ , S ′ , SK) とした時、E ′ = ∅ な

う型主導コンパイルによって実現される。したがっらば、制約が解消されたカインド環境 K′ と型代入て、この変換は、型主導コンパイルに必要な、型注釈

S ′ の二つ組 (K′ , S ′ ) を返す。もし、E ′ 6= ∅ ならば、を行う部分と、実際に型主導コンパイルを行う部分、U はエラーを返す。規則中の F とは、ラベルから型

これら二つの部分に分けることが出来る。よって、表への有限写像であり、レコード {F } やレコードカイ

面言語 λ

let,

に適切な型注釈を行い、明示的に型付けされる中間言語 ∆

let,

を生成する型推論アルゴリズ

ンド {{F }} の別の表現として用いる。また、F1 ± F2とは、dom(F ) = dom(F1 ) ∪ dom(F2 ) で、任意のに型主導コンパイルを行l ∈ dom(F ) に対し、l ∈ dom(F1 ) なら F (l) = F1 (l)うコンパイルアルゴリズム C の 2 つのアルゴリズムであり、もしそうでなければ、F (l) = F2 (l) を満たすを導入する。

ような関数 F のことを指す。

ム WK と、中間言語 ∆let,

2. 2. 1 型推論アルゴリズム WKlet,

図 5 中、規則 (iii)、(iv) は、レコードカインドに関に対して適切な型注釈を行い、かつ多相型とする制約解消を表している。規則 (iii) では、レコー

let,

単相型の適用と抽象の形を変更して、中間言語 ∆ドカインド {{F1 }} が付けられた型変数 t1 と、レコーに変換するアルゴリズムとして、WK アルゴリズム

ドカインド {{F2 }} が付けられた型変数 t2 が等しいとλを導入する。WK は、入力としてカインド環境 K、変考える時の制約を解消する。まず、t1 を t2 に代入す

数から型への写像を表す型環境 Γ、 λlet, の項 e を受る。その上で、F1 と F2 の定義域のラベルに重複する

け取り、型推論に成功した場合、出力として、カイン部分があった場合、そのラベルに対応する値の型は等ド環境 K、型変数から型への型代入 S 、e に型注釈をしいことを表すよう等式制約を拡張する。次に、t2 のの項 M 、e の型 τ を返す。

カインドとして、{{F1 ± F2 }} を与えるようカインド

まず、WK アルゴリズムに必要な、Robinson の単環境を拡張する。そして、t1 7→ t2 を表すよう型代入加えた結果得られる ∆let,日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集5

K ` τ :: kK(t) = {{l1 : τ1 , .... , ln : τn , ... }}ok initK ` t :: {{l1 : τ1 , .... , ln : τn }}{l1 : τ1 , .... , ln : τn , ... } is well formed under KK ` {l1 : τ1 , .... , ln : τn , ... } :: {{l1 : τ1 , .... , ln : τn }}図3K, Γ ▷ e : τ1

Ohori 体系でのカインド付け規則 (一部抜粋)

コードにはラベルが現れない。これは、コンパイルア

K ` τ1 :: {{l : τ2 }}K, Γ ▷ e l : τ2
図4

ok genot e dot

ルゴリズム C によって、レコードのフィールドの並び順が決められるとともに、レコードアクセスは (何番λlet, の規則 (一部抜粋)

目のフィールドかを表す) 非負整数の添字で行われるを拡張する。規則 (iv) では、レコードカインド {{F1 }}ためである。並び順を決定するために、ラベル集合にが付けられた型変数 t1 と、レコード型 {F2 } が等しは何らかの全順序  が与えられていると仮定する。

いと考える時の制約を解消する。まず、t1 を {F2 } にOhori は、ラベルを文字列リテラルの集合であると代入する。その上で、F1 と F2 の定義域のラベルにし、 を辞書付き順序としている。I は添字の集合で重複する部分があった場合、そのラベルに対応するある。i は非負整数である定数添字を表し、I は添字

値の型は等しいことを表すよう等式制約を拡張する。

変数を表す。τ は単相型の集合である。 λlet, との違

そして、t1 7→ {F2 } を表すよう型代入を拡張する。

いとして、添字の型 idx(l , τ ) が導入される。idx(l , τ )WK アルゴリズムのうち、特徴的なものとして、レは、τ 型のラベル l に対応する添字を表す型である。

コードの射影操作の項に対する WK アルゴリズムを

idx(l , τ1 ) ⇒ τ2 という型は、idx(l , τ1 ) で表される添字

図 6 に示す。

の値を受け取り、τ2 の型の値を返す関数の型を意味

図 6 のアルゴリズムでは、まず、e1 の変換後の項する。

を得る。その後、e1 の型 τ1 についての制約を解く。

C は、入力として、添字 I から添字を意味する型

まず、新しい型変数として、レコードの値の型 t1 、操idx(l , τ ) への写像を表す添字環境 L、型環境 Γ、 ∆let,

作の対象を表す t2 を導入し、の項 M を受け取り、出力として、 λlet,[] の項 C を• t1 はカインド U を持つ返す。

C アルゴリズムの特徴的な部分として、レコードの• t2 はカインド {{l : t1 }} を持つ• t2 = τ1 という等式集合を満たす

射影操作の項に対する変換を、図 8 に示す。

という制約を U に渡し、出力を得る。この出力をもとに、変換後の項として、M1 に対して型注釈 S2 (t2 )L ` I : idx(l , τ ) は添字項 I のための型判断で、以下に型付け規則を示す。

を付けている。

2. 2. 2 コンパイルアルゴリズム C
中間言語 ∆let,

let,[]からターゲット言語 λに変換するアルゴリズムとして、C アルゴリズムを導入する。この変換では、レコードを値が並んだ配列として

L{I : idx(l , t)} ` I : idx(l , t)

idx var

L ` j : idx(lj , {l1 : τ1 , .... , ln : τn })idx rec

レコードを表す項 M を C を再帰的に呼出して変表現し、ラベルから値を得る操作を、配列に添字でア換した上で、ラベル l を使って値にアクセスする操

クセスする操作に変換する。

作を添字を使ってアクセスする操作に置き換える。

λlet,[] の定義を図 7 に示す。 λlet,[] の言語では、レ

そのために、L ` I : idx(l , τ ) という添字項 I のた

日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集6(E ∪ {(t1 , t2 )}, K ∪ {(t1 , {{F1 }}), (t2 , {{F2 }})}, S, SK) =⇒(iii)([t2 /t1 ](E ∪ {(F1 (l ), F2 (l )) | l ∈ dom(F1 ) ∩ dom(F2 )}),
[t2 /t1 ](K) ∪ {(t2 , [t2 /t1 ]({{F1 ± F2 }}))},[t2 /t1 ](S) ∪ {(t1 , t2 )},[t2 /t1 ](SK) ∪ {(t1 , {{F1 }})})(E ∪ {(t1 , {F2 })}, K ∪ {(t1 , {{F1 }})}, S, SK) =⇒(iv)([{F2 }/t1 ](E ∪ {(F1 (l ), F2 (l )) | l ∈ dom(F1 )}),[{F2 }/t1 ](K),[{F2 }/t1 ](S) ∪ {(t1 , {F2 })},[{F2 }/t1 ](SK) ∪ {(t1 , {{F1 }})})
if dom(F1 ) ⊆ dom(F2 ) and t1 ∈/ F T V ({F2 })図5

カインド付け単一化の一部

WK(K, Γ, e1 l ) =let(K1 , S1 , M1 , τ1 ) = WK(K, Γ, e1 )(K2 , S2 ) = U(K1 {t1 :: U , t2 :: {{l : t1 }}},{(t2 , τ1 )}) (t1 , t2 are fresh)in(K2 , S2 ◦ S1 ,S2 (M1 ) : S2 (t2 )  l , S2 (t1 ))図6

レコード射影操作に関する WK アルゴリズム

C(L, Γ, M : τ l ) =let
C = C(L, Γ, M ) andI be an index term s.t. L ` I : idx(l , τ )in C [I]図8

レコード射影操作に関するアルゴリズム C

ムを導入する項をコンパイルする段階で導入される)を使って配列アクセスを行うことになる。

C : expression i : index value
I : index variable
I ::= i | I
C ::= x | cb | λx.C | C C | let x = C in C
| {C , · · · , C } | C [I]| λI .C | C I
τ ::= t | b | τ → τ | {l : τ, · · · , l : τ } | idx(l , τ ) ⇒ τ
σ ::= τ | ∀ t :: k .σ

2. 3 例Ohori 体系でのプログラムの例を示す。 λlet, の項
として、
let name = λx .x  Namein name {Name = ”Joe”, Age = 21}を考える。これを WK によって変換すると、
let name : ∀t1 :: U .∀t2 :: {{Name : t1 }}.t2 → t1 =Poly(λx : t2 .x  Name

図7

λlet,[] の項と型 (一部抜粋)

めの型判断を使って、L、l 、τ からその添字 I を得る。詳細は省くが、C は、与えられた L, l , τ に対し

L ` I : idx(l , τ ) が成立する I が高々ひとつとなるように作られている。τ がレコード型である場合には、lj の位置が静的にわかるので添字の値として定数が得られ、その定数を使って配列にアクセスすることになる。τ が型変数である場合には、フィールド l が存在する位置を示すための添字変数 I(これは型スキー: ∀t1 :: U .∀t2 :: {{Name : t1 }}.t2 → t1 )in (name string {Name : string, Age : int}){Name = ”Joe”, Age = 21}の ∆let, の項となる。さらに C によって変換すると、
let name = λI .λx .x [I ]in (name 1 {”Joe”, 21})の λlet,[] の項となり、これが評価される。

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

7

その実行時型を検査する。このアクセスは e1 の値の

3 提案言語

実行時型情報を使って行う。ハッシュテーブルへの

本節では、前節の 3 つの体系をハッシュテーブル

アクセス同様、e2 に対応するフィールドが存在しなによって拡張する。なお、簡単のため、ハッシュテー

かったり、取り出した値の実行時型検査に失敗した場

ブルのキーは、全て文字列であるとする。また、ハッ合は実行時エラーとなる。

シュテーブルに値を追加・上書きする構文を用意す

図 9 に、表面言語 λlet, の項 e 、単相型 τ 、多相型

るが、Standard ML および SML♯ のレコードはイ

σ 、値 v 、カインド k を示す。ハッシュテーブルのキー

ミュータブルであることから、相互運用を行わないもを表すために文字列型 string と文字列定数 s を追加のとしている。

している。また、この言語には副作用があるため、値以降、表面言語 λlet, とその型システム、型推論ア
ルゴリズム、コンパイルアルゴリズムの順に示す。

制限 [5] [1] を採用し let による定義の右辺は値を表す式に限定する。

3. 1 表面言語 λlet, と型システム

e : expression x : variable l : label

ハッシュテーブルに対するプリミティブな操作としt : type variable s : stringて、ハッシュテーブルの作成を行う create、ハッシュ

e ::= x | λx .e | e1 e2 | let x = v1 in e2

テーブル e1 のキー文字列 e2 に対応する値を取り出す| {l1 = e1 , .... , ln = en } | e lﬁnd e1 e2 、および、ハッシュテーブル e1 にキー文字列| create | ﬁnd e1 e2 | add e1 e2 e3 | s

e2 に対応する値 e3 を追加もしくは既にそのキーが存τ ::= t | string | τ → τ ′ | {l1 : τ1 , .... , ln : τn }在する場合には (破壊的に) 更新する add e1 e2 e3 を考| hashtbl

える。第 1 節で述べたように、ハッシュテーブルに格σ ::= τ | ∀ t :: k .σ

納される値の型は動的に検査するため、ハッシュテー

v ::= λx .e | s | {l1 = e1 , .... , ln = en }ブルの型は (キーや値の型情報を持たない)hashtbl で

k ::= U | {{l1 : τ1 , · · · , ln : τn }}表す。そのため、add を使って値を追加・更新する際
図9には e3 の型は任意のものを許し、ﬁnd e1 e2 の静的型

λlet, の定義

も任意の型をとることができるとする。実行時には、

e2 に対応するキーが存在するかだけでなく、取り出

型付けにおいて相互運用を許すには、カインド付けした値の型が静的型と一致するかどうかを検査する。

を少し変更するだけでよい。まず、射影操作がハッキーが存在しなかったり、型が一致しなかった場合はシュテーブルを受け入れられるようにするには、ハッ実行時エラーとする。この実行時型検査を行うため

シュテーブル型は任意のレコードカインドが与えらに、ハッシュテーブルには値だけでなくその実行時のれるとするだけで十分である。この定義を表すカイ型も格納する必要がある。

ンド付け規則を図 10 に示す。

さらに、レコードとハッシュテーブルの相互運用のため、e l の e がハッシュテーブルだった場合やﬁnd の第一引数がレコードだった場合の意味も与える必要がある。まず、e l の e がハッシュテーブルだっK ` τ :: kK ` hashtbl :: {{l1 : τ1 ; .... ; ln : τn ; ... }}た場合は、実質的に ﬁnd e l と同じ意味となる。つまり、l が存在しない場合や、取り出した値の型が静的

図 10

カインドとカインド付け規則 (一部抜粋)

な型と一致しない場合は実行時エラーとなる。逆に、

ﬁnd e1 e2 の e1 がレコードである場合、e2 の値をラ

逆に、ﬁnd の操作対象としてレコードを許すためにベルと見做して対応するフィールドの値を取り出し、は、全てのレコード型と hashtbl 型を表すような新し日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

8

いカインドを用意し、ﬁnd の第一引数はこのカインド

コードかハッシュテーブルかを実行時に判定し、それを持つ型であれば何でもよい、という型付け規則を与ぞれのアクセスに適した式に分岐する式に変換するこえればよい。このカインドは、空のレコードカインドととする。ハッシュテーブルからの値の取り出しを行{{う式として、C1 [C2 ] : τ を導入する。この τ は、式に}} を使って自然に表すことができる。
図 11 に ﬁnd e1 e2 の型付け規則を示す。この規則

与えられた静的型で、取り出した値の実行時型との比は、e1 に何らかの型 τ1 が付き、e2 が文字列型である

較に使われる。また、受け取った引数 C のデータ構ことを要求する。加えて、e1 の型 τ1 が空のレコード造に対し、I が −1 以下か 0 以上か実行時に判定し、カインド {{}} を持つことを要求する。このカイン−1 ならば、l と等しい文字列 C2 を用いた C [C2 ] : τ 、ドによって τ1 がレコード型またはハッシュテーブル

0 以上なら C [I] に分岐する式 bltz I C l : τ を導入す型に制限される。

る。この拡張を行ったターゲット言語 λlet,[] の添字
集合 I 、項 C 、型 τ を図 14 に示す。

3. 2 型推論アルゴリズム WK

添字項にハッシュテーブルへのアクセスを意味す

Ohori の型推論アルゴリズムの拡張にあたって、まる −1 を追加する。前と同様、0 以上の値 i はレコー

ずカインド付け単一化の拡張を考える。拡張されたカドを配列として見なしたときのアクセスする添字をインド付け単一化アルゴリズムの一部を図 12 に示す。

意味する。I は添字変数を意味する。

規則 (vii) では、レコードカインド {{F1 }} が付けら

図 15 に、添字項の型付け規則を示す。この規則は、れた型変数 t1 と、hashtbl 型が等しいと考える。この添字環境 L の元で、添字項 I に、idx(l , τ ) が対応す

時、規則 (iv) とは異なり、hashtbl 型はその構造につることを意味する。−1 と 0 以上の添字を、型によっいての情報を持たないため、等式制約やカインド環境て付け分けることで、レコードとハッシュテーブルをを拡張することなく、ただ t1 7→ hashtbl を表すよう区別できるようになっている。

型代入を拡張するだけでよい。

∆let, を λlet,[] に変換するアルゴリズムとして、C次に、型推論アルゴリズム WK の拡張の一部を図

アルゴリズムの一部を図 16 に示す。C は、添字環境

13 に示す。ﬁnd e1 e2 に対する変換では、まず、e1 , e2

L、型環境 Γ、 ∆let, の項 M を受け取り、 λlet,[] のそれぞれに対し、変換後の項を互いの制約を満たすよ

項 C を返す。

うに順番に得る。その後、この文脈が満たすべき、(M : τ1 l ) : τ2 に対する変換では、動的な分岐を実• e1 の型は新しい型 t1 と等しく、空のレコードカ

現している。この ∆let, の項は、レコードを渡されインドが付く• e2 の型は string と等しいという制約を U アルゴリズムに渡している。

た場合は静的にアクセスを行い、ハッシュテーブルを渡された場合は動的にアクセスを行う。従って、動的に分岐を行う bltz による項に変換される。

その他、出力の ∆let, 項に必要な型注釈を付ける部分を除き、型推論アルゴリズム WK の拡張を行う

3. 4 プログラムの例

必要はない。

本体系のプログラムの例を以下に示す。まず、ハッシュテーブルをレコードとして扱う例として、表面言3. 3 コンパイルアルゴリズム C
Ohori のコンパイルアルゴリズムとターゲット言語
let,[]

λに、ハッシュテーブルを追加して拡張することを考える。まず、ターゲット言語 λlet,[] における添
字項 I に、アクセス対象がハッシュテーブルである
ことを表現する特殊な定数 −1 を追加する。また、レ
コード射影操作は、添字項によってアクセス対象がレ

語 λlet, の項
let h = create inlet get name = λx .x  Name in get name hを考える。これを WK によって変換すると、

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

9K, Γ ▷ e : σK, Γ ▷ e1 : τ1

K, Γ ▷ e2 : stringK ` τ1 :: {{t e findK, Γ ▷ ﬁnd e1 e2 : τ
図 11

(vii)

}}

λlet, の型付け規則の一部(E ∪ {(t1 , hashtbl )}, K ∪ {(t1 , {{F1 }})},

4 実装

S, SK) =⇒(([hashtbl /t1 ]E),

本節は、第 3 節で定義した言語を、SML♯ コンパイ([hashtbl /t1 ]K),

ラに実装した手法について示す。まず、3. 1 節で述べ([hashtbl /t1 ]S) ∪ {(t1 , hashtbl )},た、ハッシュテーブルに対する構文と型システムを([hashtbl /t1 ]SK) ∪ {(t1 , {{F1 }})})SML♯ に実装することを考える。次に、3. 2 節と 3. 3

図 12

節で述べた、型推論アルゴリズムとコンパイル手法を拡張されたカインド付け単一化の一部

SML♯ に実装することを考える。最後に、性能評価を行い、オーバーヘッドを評価する。

let h : hashtbl = Poly(create : hashtbl ) in
let get name : ∀t1 :: U .∀t2 :: {{N ame : t1 }}.

4. 1 ハッシュテーブルの実装

t2 → t1 =Poly((λx : t2 .x : t2  Name : t1 ) : ∀t1 :: U .

操作構文に対応する、SML♯ 上で拡張したハッシュ∀t2 :: {{N ame : t1 }}.t2 → t1 )in get name string hashtbl hの中間言語 ∆let, の項となる。さらに C によって変

テーブル操作構文を示す。 {#} 構文は、 λlet, における create 構文に対応する。この時、ハッシュ関数と、キーの等価性判定関数は、SML/NJ のハッ

換すると、
let h = create inシ ュ テ ーブ ル ライ ブ ラ リと 同 一の も のを 用 い る。

let get name ={#}{hashFn = e1 , eqFn = e2 } 構文は、{#} 構文におλt1 .λt2 .λI .λx .bltz I x Name : t1

いてハッシュ関数 e1 とキーの等価性判定関数 e2 を

in get name string hashtbl (−1) hのターゲット言語 λlet,[] の項になる。レコードをハッシュテーブルとして扱う例として
let r = {Name = ”Joe”; Age = ”21”} in{Name = ”Joe”, Age = ”21”} in

る ﬁnd e1 e2 構文に対応する。e1 .[e2 ] ← e3 構文につ文は、ハッシュテーブル e1 に、キー e2 を指定し、値e3 の追加・上書きを行う構文である。この時、キーe2 が存在するなら値 e3 を上書きし、存在しないなら
値 e3 を追加する。また、この構文は、e1 にレコード}}.∀t2 :: U .t1 → t2 =Poly((λx : t1 .ﬁndt2 x ”Name”) : ∀t1 :: {{

指定するために用いる。e1 .[e2 ] 構文は、 λlet, におけいては、 λlet, に対応する構文が存在しない。この構

let get name = λx .ﬁnd x ”Name” in get name rを考える。これを WK によって変換すると、
let r : {Name : string, Age : string} =let get name : ∀t1 :: {{図 17 に、主に表面言語 λlet, のハッシュテーブル

}}.

∀t2 :: U .t1 → t2 )in get name {Name : string, Age : string} string rの ∆let, の項となる。さらに C によって変換すると、
let r = {Name : string; Age : string} inlet get name = λt1 .λt2 .λx .x [”Name”] : t2
in get name {Name : string; Age : string} string rの λlet,[] の項となり、これが評価される。

を受け入れることが出来ない。
これらの SML♯ の構文に対応する実装を与えることを考える。実装を与えるために、まず、SML♯ の
コンパイル方式と、実装の方針を示す。SML♯ では、
ブートストラップを行うために、SML♯ のコンパイラが初めから提供されている。よって、既に与えられているコンパイラが受理できる SML♯ 言語でハッシュテーブルの実装を与えることで、これから構成する

SML♯ コンパイル中に、その実装を呼び出すことが出日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

10

WK(K, Γ, ﬁnd e1 e2 ) =let(K1 , S1 , M1 , τ1 ) = WK(K, Γ, e1 )(K2 , S2 , M2 , τ2 ) = WK(K1 , S1 (Γ), e2 )(K3 , S3 ) = U(K2 {t1 :: {{in}}}, {(t1 , S2 (τ1 )), (string, τ2 )}) (t1 is fresh)(K2 , S3 ◦ S2 ◦ S1 , ﬁndS3 (t1 ) S3 ◦ S2 (M1 ) S3 (M2 ), S3 (t1 ))
図 13

WK アルゴリズム (抜粋)

受 理 で き る SML♯ 言 語 で 記 述 し た イ ン タ ー フ

I ::= i | −1 | I
C ::= λt.C | C τ | λI .C | C I | λx .C | C1 C2| let x = V1 in C2 | {C1 : τ1 , .... , Cn : τn }| C [I] | create | C1 [C2 ] : τ| s | error | bltz I C l : ττ ::= t | string | τ → τ ′ | {l1 : τ1 , .... , ln : τn }| hashtbl | idx(l , τ1 ) ⇒ τ2
σ ::= τ | ∀ t :: k .σ

ェ ー ス の 一 部 を 示 す 。HashTbl.create 関 数 は 、{#}{hashFn = e1 , eqFn = e2 } 構 文 の 実 装 で あ る 。
HashTbl.default 関数は、{#} 構文の実装であり、ハッシュ関数と等価性判定関数の初期設定を
与 え 、HashTbl.create 関 数 を 呼 び 出 し て い る 。

Interoperable.find 関数は、e1 .[e2 ] 構文の実装である。Interoperable.find 関数の型のうち、ハッシュテーブル型またはレコード型を受けいれる型変数′

図 14

λlet,[] の添字集合と項と型

b と、返り値の型変数 ′ a には、実行時の型情報を必要とする reify カインドが追加されている。それぞれの型変数が実行時型検査を要求する理由について述べる。型変数 ′ b は、その値の型がハッシュテーブ

L ` I : idx(l , τ )L ` −1 : idx(l , hashtbl )ルレコード型とレコード型のどちらであるかに従っ

idx hashて実行時に分岐するために、動的型検査を必要とする。型変数 ′ a は、e1 .[e2 ] を用いている文脈で期待さ

図 15

提案言語の添字項型付け規則

れる型と、返り値の型の等価性を実行時に判定するために、動的型検査を必要とする。また、型変数 ′ bC(L, Γ, (M : τ1 l ) : τ2 ) =letin

C = C(L, Γ, M )インド {{L ` I : idx(l , τ1 )この型定義は図 11 と一致する。HashTbl.add 関数

bltz I C l : τ2

は、e1 .[e2 ] ← e3 構文の実装である。この関数では、

図 16

C コンパイルアルゴリズムの一部{#} | {#}{hashFn = e1 , eqFn = e2 }e1 .[e2 ] | e1 .[e2 ] ← e3
図 17に付く {} カインドは、3 節における空のレコードカ

ハッシュテーブルに対する SML♯ 上での操作構文}} に対応する。reify カインドを除けば、Dynamic.void Dynamic.dyn 型が現れるが、動的型検査が行える型であることを意味している。

4. 2 型推論アルゴリズムの実装
3. 1 節で述べたように、Ohori の多相レコード計算には、既に空のレコードカインド {{}} が存在し、

このカインドは空のレコード型に付く。この空のレ
コードカインド {{来る。
♯}} が、ハッシュテーブル型にも図 18 に 、SML 上 の ハ ッ シ ュ テ ー ブ ル の 構 文付けられるよう拡張するアルゴリズムが図 12 であっに 対 応 す る 、既 に 与 え ら れ て い る コ ン パ イ ラ がた。従って、SML♯ コンパイラのカインド付け単一化

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

11

structure HashTbl =structtype hashtbl (= boxed)

val create: {hash: string -> word, eq: string * string -> bool} -> hashtbl

val default : unit -> hashtbl
val add: hashtbl -> string -> Dynamic.void Dynamic.dyn -> unit

end
structure Interoperable =structval find: ['a#reify, 'b#reify#{}. 'b -> string -> 'a]

end
図 18

ハッシュテーブルモジュールのインターフェース (一部抜粋)

アルゴリズムを、図 12 の通りに拡張した。

datatype rcexp =しかし、e l にハッシュテーブル型の式が渡された...

とき、ﬁnd e l と同じ意味を持つためには、e l の返り| RCSWITCH of {値の値に対して、動的型検査を必要とする。従って、exp : rcexp,

e l の返り値の型に、#reify カインドを付けた。

expTy : ty,
branches :4. 3 コンパイルアルゴリズムの実装{const : tlint, body : rcexp} list,

まず、SML コンパイラにおける C アルゴリズム

defaultExp : rcexp,を、図 16 の通りに拡張した。次に、ターゲット言語

resultTy : ty, ... }♯let,[]λにおいて拡張した、添字 −1 や、bltz I C l : τ

式に対応する表現を実装することを考える。
まず、添字 −1 の表現を与えるために、SML♯ に置

| ...
図 19

λlet,[] に相当するコンパイラ中間言語の分岐式のデータ型定義 (一部抜粋)

ける添字定数の定義について述べる。添字定数 ι は、

32 ビット符号なし整数である Word32 型の値として一致しない場合、defaultExp 式に分岐する。全ての表現されている。この値を、idx(l , τ ) 型にキャストすbody 式と defaultExp 式が持つ型は、resultTy 型でることで、添字定数として表現されている。従って、ある。

添字 −1 は、アンダーフローした 0wxﬀﬀﬀﬀ 値としてこの分岐式を用いて、bltz I C l : τ 式を次のように表現した。まず、添字 I を Word32 型に再度キャ表現し、これを idx(l , τ ) 型にキャストした。
次に、bltz I C l : τ 式の表現を与えるために、SML

ストし、exp 式とした。次に、branches を、constのターゲット言語 λlet,[] 上の分岐式について述べる。

が 0wxﬀﬀﬀﬀ ならば、 λlet,[] 言語上での e1 .[e2 ] 式に♯には、図 19 の分岐式

分岐する形で定義した。defaultExp 式は、 λlet,[]が存在する。それぞれのフィールドについて以下示

言語上でのレコードの射影操作式とした。結果の型♯

SML のターゲット言語 λlet,[]

let,[]す。 exp フィールドは、 λで表現される条件式

で、expTy 型を持つ。exp 式の値が、branches リス
ト内の const の値と一致する場合、対応する、 λlet,[]

で表現される body 式に分岐する。どの const の値に

resultTy は、型推論アルゴリズムで注釈されてる τとした。

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

実験 2: t を固定、n を変化

4. 4 性能の予備評価♯♯

本節では、我々の SML コンパイラと既存の SML

次に、t = 100000 に固定し、n を {5, 15, 32, 50} かコンパイラの性能を比較し、相互運用にかかるオー

ら選んで実験を行った。(ハッシュテーブルの初期容

バーヘッドを評価する。

量は 32 であり、n = 50 のときは容量は 64 である。)

本論文ではレコードやハッシュテーブルに対し共通

この実験の結果を図 21 に示す。この結果から、r.[e]の射影構文を与えることで相互運用を実現しているたの実行時間のみ n の増加に伴って大きくなる傾向が♯

め、拡張前後の SML それぞれでのレコードやハッ見られた。これはレコード型のサイズが大きくなる

シュテーブルへの射影関数の性能を評価することでにつれ、r.[e] の計算に必要なレコード型の動的な解

オーバーヘッド評価を行う。レコード r の射影操作

析にかかる時間が増え、オーバーヘッドが増加するた♯の評価として、我々の拡張 SML では式 r l と r.[e]♯めと考えられる。

にかかる実行時間を、拡張前 SML では式 r l にかか

図 20・図 21 の、拡張前後の測定結果を比較する

る実行時間をそれぞれ測定する。またハッシュテーブと、レコードの射影については、オーバーヘッドがほ♯ル h の射影操作の評価として、我々の拡張 SML でぼないことがわかる。ハッシュテーブルの射影につは式 h l と h.[e] にかかる実行時間を、拡張前 SML♯

いては、操作対象がレコードかハッシュテーブルかのでは式 h.[e] にかかる実行時間を測定する。

判定のために 4〜5.4 倍ほどのオーバーヘッドが生じ以上の式を評価する本論文での実験設定は次の通りていることが分かった。

である。本実験ではレコードやハッシュテーブルの値の数 n と、アクセスの繰り返し回数 t の値を変えて

5 関連研究評価を行う。n と t が与えられると、ラベル名・キー

本研究では、静的な構造を持つレコードと、動的な名だけが異なる 10 通りのレコード・ハッシュテーブ構造を持つハッシュテーブルの暗黙な相互運用を目ルを作成し、上記で述べた各式について、実行時間の標とした。この目標は、静的型付け言語と、動的型付

平均を計測する。

け言語を組み合わせた、Siek と Taha が提案した漸♯実験環境は以下の通りである。拡張前の SML

進的型付け言語 [8] [9] と理念を同じにする。漸進的型

として Version 4.0.0 を用い、我々の拡張も Version

付け言語では、静的型と動的型が利用でき、静的型検

4.0.0 を基に行う。測定する計算機の CPU は Intel(R)査と動的型検査を組み合わせて健全性を保っている。

Xeon(R) Gold 6226 で物理コア数 12、スレッド数 24、

この漸進的型付け言語を用いることで、開発の初期段

クロック周波数は 2.7GHz、計算機の主記憶容量は

階では、動的型を使った柔軟なプロトタイピングが可768GB である。OS は Ubuntu 18.04.6 LTS で、カー能になる。更に、開発が進み実装方針が固まり次第、

ネルバージョンは 4.15.0-167-generic である。計測時

動的型を静的型に漸進的に置き換え、頑健で効率の良間にはユーザー CPU 時間を用いる。

いプログラムへの移行が可能になる。漸進的型付け

実験 1: n を固定、t を変化

言語は、動的型と静的型を相互に運用できる 1 つのn = 5 とし、t を {1000, 10000, 30000, 50000, 100000}

言語体系を提案した。この一般化として、Pattersonから選んで実験を行った。その結果を図 20 に示す。

と Ahmed は、異なる言語同士を相互運用する仕組

図の縦軸は単位を秒として、t 回アクセスにかかったみ [4] を提案した。本研究では、漸進的型付けにおけ時間を対数目盛で示した。横軸はそれぞれのアクセる型の漸進的な相互運用を発展させ、データ構造も漸ス方法についてまとめた。この結果から、期待通り、

進的に相互運用出来る仕組みを提案している。

どのアクセス方法についても t の増加に比例して実行時間が増大する傾向があることがわかる。

Ohori の体系では、レコードを多相的に扱う問題に対し、カインドを用いた解決方法を提案した。同様の問題に対し、Wand は列変数を用いた解決方法 [11] [12]を提案している。列変数とは、ラベルと紐づく型の日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

図 20

図 21

13

n = 5 の時の測定結果

t = 100000 の時の測定結果

上を動く変数である。この列変数を含む制約集合を

ローディングとして捉えることも出来る。SML♯ で解くことで、型推論を行っている。この手法は Rémyは、多相レコード計算に基づく軽量な第一級オーバー

によって、フラグを用いる方法に拡張 [6] された。フローディング [13] が実現されている。この第一級オー

ラグとは、どのラベルが存在するべきか、存在しない

バーローディングは、型抽象によって、対応する型をべきかを保持する仕組みである。フラグと列変数を受け入れる関数を選択することで実現される。しか組み合わせることで、型システム上で未定義のラベル

し、多相型やレコード多相性を扱うことはできないたへのアクセスを防ぐことができるようになっている。

め、本研究の手法の実現方法にはならない。本研究の本研究における、異なる型を受け入れることが出来

暗黙な相互運用は、第一級オーバーローディングが行る、同一の名前の関数を実現することは、オーバーう関数の選択が、レコードの添字情報に基づいて実現日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集14

されていると考えることもできる。

6 おわりに
本研究では、ハッシュテーブルとレコードを暗黙に相互運用できるような ML の拡張を、Ohori の多相レコード計算の拡張として提案した。相互運用を可能にするために、レコード型とハッシュテーブル型を含むよう、カインドの意味を変更した。この変更は軽微なものであり、型推論アルゴリズムの変更も小さく済んでいる。また、効率的なレコード操作を可能にする

Ohori のレコードコンパイル手法の拡張を示した。これらの拡張を SML♯ コンパイラ上に実装し、予備実
験により、レコードに対するレコードアクセスのオーバーヘッドはほとんど生じていないことを確認した。
今後の課題として、理論面については、拡張した
let,

λ

の型システムの健全性、(拡張した)WK の健全性・完全性、 λlet,[] へのコンパイルが型付けを保存する、といった性質を示すことがあげられるが、既存の証明方法を適用して素直にできると考えている。
本研究では、レコードのフィールド更新操作やハッシュテーブルのキー追加・更新操作についての相互運
用性は扱っていない。Standard ML や SML♯ のレ
コードはイミュータブルで、ハッシュテーブルに通常備わる破壊的な更新操作と素朴に相互運用を行うことは問題があると考えられる。どのような形で相互運用を行うかを考える必要があるだろう。
謝辞
本研究を進める上で、実装に当たり、SML♯ の内部構造についてご教授いただきました新潟大学の上野雄大氏に心から感謝いたします。また、様々な助言をいた
だきました末永幸平氏、和賀正樹氏にも合わせてお礼
申し上げます。本研究は JSPS 科研費 JP20H00582、

JP19K20247 の助成を受けたものです。
参 考 文 献[ 1 ] Milner, R., Tofte, M., Harper, R., and MacQueen, D.: The Deﬁnition of Standard ML, MIT
Press, Cambridge, MA, USA, revised edition, 1997.
[ 2 ] Ohori, A.: A Compilation Method for ML-Style
Polymorphic Record Calculi, Conference Record of
the Nineteenth Annual ACM SIGPLAN-SIGACT

Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January
19-22, 1992, Sethi, R.(ed.), ACM Press, 1992,
pp. 154–165.
[ 3 ] Ohori, A.: A Polymorphic Record Calculus and
Its Compilation, ACM Trans. Program. Lang. Syst.,
Vol. 17, No. 6(1995), pp. 844–895.
[ 4 ] Patterson, D. and Ahmed, A.: Foreign Function
Typing: Semantic Type Soundness for FFIs, WGT
2020: First ACM SIGPLAN Workshop on Gradual
Typing, 2020.
[ 5 ] Pierce, B. C.: Types and Programming Languages, The MIT Press, 2002.
[ 6 ] Rémy, D.: Type Checking Records and Variants in a Natural Extension of ML, Proceedings ofthe 16th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’89,
New York, NY, USA, Association for Computing
Machinery, 1989, pp. 77–88.
[ 7 ] Robinson, J. A.: A Machine-Oriented Logic
Based on the Resolution Principle, J. ACM, Vol. 12,
No. 1(1965), pp. 23–41.
[ 8 ] Siek, J. G. and Taha, W.: Gradual Typing for
Functional Languages, In Scheme and Functional
Programming Workshop, 2006, pp. 81–92.
[ 9 ] Siek, J. G., Vitousek, M. M., Cimini, M., andBoyland, J. T.: Reﬁned Criteria for Gradual Typing, 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3–6, 2015, Asilomar,
California, USA, Ball, T., Bodı́k, R., Krishnamurthi, S., Lerner, B. S., and Morrisett, G.(eds.),
LIPIcs, Vol. 32, Schloss Dagstuhl–Leibniz-Zentrum
für Informatik, 2015, pp. 274–293.
[10] The SML# Development Team: SML#プロジェ
クト, https://smlsharp.github.io/ja/.
[11] Wand, M.: Complete Type Inference for Simple
Objects, Proceedings of the Symposium on Logic in
Computer Science (LICS ’87), Ithaca, New York,USA, June 22-25, 1987, IEEE Computer Society,1987, pp. 37–44.
[12] Wand, M.: Corrigendum: Complete Type Inference for Simple Objects, Proceedings of the Third
Annual Symposium on Logic in Computer Science(LICS ’88), Edinburgh, Scotland, UK, July 5–8,
1988, IEEE Computer Society, 1988, pp. 132.
[13] 上野雄大, 大堀淳: 多相レコード計算に基づく軽量な第一級オーバーロードの設計と実装, コンピュータソ
フトウェア, Vol. 29, No. 1(2012), pp. 191–210.