これは KMC Advent Calendar 2018 - Adventar と 言語実装 Advent Calendar 2018 - Qiita 4日目の記事です．
3日目はそれぞれ，
- id:nojima718 さんの ぷよぷよのプレイ動画を解析して棋譜を生成する - @nojima's blog (KMC)
- @yhara さんの Shiika進捗(2018) - yhara.jp (言語実装)
でした．
自己紹介
id:utgwkk (うたがわきき) です．学部4回生になり，プログラミング言語に関する研究をすることになりました*1．
KMC部員としての生活もついに4年目です．ふだんはお酒を飲んでいます．
概要
この記事では，大堀先生の多相レコード理論の論文[1] *2について，(数学的な議論は控えめに)どういうことをやっているのかについて紹介します． また，リファレンス実装のSML# と私が書いた実装について紹介します．
record polymorphismの理論
さて，読者のみなさまの中には record polymorphism と聞いて「ああ，アレね」とすぐに理解される方もいらっしゃるかと思われますが，わたしの理解の再確認も兼ねて，それぞれの要素に分解して説明していこうと思います． すなわち，
- 「レコード」って何？
- 「多相性」って何？
- 「カインド」って何？
の順に説明していきます．
なお，
- そもそも「計算体系」って何？
- 「型」とか「型システム」って何？
- 「型推論」って何？どうやるの？
といったことについて掘り下げていくといくら時間があっても足りなくなる*3ため，ここでは参考となるサイトをいくつか挙げるにとどめておきます． この記事を読んでいて分からないことがあれば適宜あたっていくとよいでしょう．
- 住井先生による「ラムダ計算入門」 (計算体系について)
- 「型システム入門 プログラミング言語と型の理論」の第1章 (型システムについて，日本語訳が無料で公開されている)
- 五十嵐先生の講演スライド「ＭＬ型推論の光と影」 (型推論について)
レコード
レコードは，MLのような言語でよく用いられるデータ構造です．
{name = "utgwkk" ; age = 17}
のように書くことでレコードをつくることができ，たとえばOCamlでは x.name のように書くことでフィールドの値を取り出すことができます．
イメージとしては構造体に近いです．
多相性
多相性について説明する前に，もしも多相性がなければなにが起こるのかについて考えていきましょう．
もしもOCamlに多相性がなければ，次の式は型エラーになります．
let id = fun x -> x in if id true then id 2 else id 3
何が起こっているのでしょうか？ 順番に見ていきましょう．
letで関数idを定義する．型は'a -> 'a('aは未知の型変数)ifの条件節のid trueという式を見て'a = boolという代入をすればいいことがわかった．やったね！- ところが
id 2という式もあるので'a = intでなければいけない？？？ - 🔜型エラー
多相性がない型システムでは，型変数は「いずれ型が確定するかもしれない」「使い方が確定したら即座に置き換えられる」というものになります． 多相性があれば，「この型変数の使い方はなんでもよい」ということを表現することができるようになります．
カインド
ここでは論文で取り上げられている「カインド」についてざっくりと説明していきます．
さて，多相性があると書けるプログラムが多くなるという実感を前節で得てもらえたと思いますが，残念ながらレコードに対してはこの多相性ではまだ柔軟性が足りません．
たとえば，レコードの name というフィールドの値を取得する関数について考えてみましょう*4．OCaml風に書くならば次のように書けると思います．
let name x = x.name
ところがこの関数はStandard MLでは*5定義することができません． x のレコードとしての型を決定することができないためです．
型を明示すれば name を定義することができます*6が，その型に ぴったりはまる レコードしか受け付けてくれなくなります．
われわれは name 以外のフィールドには関心を持たないつもりでいるのに，これでは不便です．
この問題を解決するために，論文ではカインドという仕組みを使っています．
カインドはざっくり言うと，型変数のとりうる範囲の制約です．
nameというstring型のフィールドを含むレコードを表すカインドを {{name:string}} のように書きます．たとえば {name:string, age:int} や {name:string, roomno:int} のようなレコードはこのカインドが付けられます．
カインドを使うと，先述した関数nameについて forall 'a,'b::{{name:'a}}.'b -> 'a のような型を付けることができます．
この関数nameは {name = "utgwkk", age = 21} や， {name = "hoge", roomno = 404} のような，nameというフィールドを含むあらゆるレコードに対して適用することができます．便利ですね．
レコード多相のコンパイル
論文では，ここまで述べてきたレコード多相の計算体系を，より低レベルな計算体系*7にコンパイルする手法を与えています． 基本的なアイデアは次の2つです．
- レコードを配列に変換する
- レコードへのフィールド名を用いたアクセスをインデックスアクセスに変換する
型情報を用いることによってこれらの変換を実現しています．
実装
SML#
論文のリファレンス実装は SML# として公開されています． 2018/12/4現在，ビルドにはやや古いバージョンのLLVMが必要とされています．バージョンさえ揃えればビルドできます*8．
SML#では，
fun name (x) = #name x;;
のように書くことで先述のname関数を実装できます．
SML# にはレコード多相のほかにもさまざまな拡張機能が実装されています．詳しくはドキュメントをご覧ください．
私の実装
私の実装はGitHubで公開されています．
menhirを入れて make すると prog が生成されます．
./prog を実行するとREPLが立ち上がります．
変換ステップは次のようになっています．
- 字句解析と構文解析 (入力文字列を計算体系の項を表すデータ型に変換する)
- 型推論 (項に型情報を付与する)
- 型検査 (項の型情報が正しいか検査する)
- コンパイル (項を低レベルの計算体系の項に変換する)
./prog --debug を実行すると，各変換ステップ後の内部表現を見ることができます．
文法はOCaml寄りになっています．READMEのBNFを参照してください． この処理系では，
let name x = x.name in name;;
のように書くことで先述のname関数を実装できます．
おわりに
レコード多相を実現するための理論についてざっくりと触れてきました．
日頃，とくに動的型の言語では何気なく書いている x.name といった式に型を付ける方法としてこのようなものがあるといったことを知ったとき，目から鱗が出ました．
この記事では触れていない部分(型推論)や，数学的な定式化などについては論文を参照してください．
この直観はさすがにずれているのではないか，などの指摘がありましたら id:utgwkk までよろしくお願いします．
余談:プログラミング言語処理系実装の実験について
京都大学工学部情報学科計算機科学コースでは，学生実験として3回生のうちに言語処理系を実装する機会が2回あります．
- MLのインタプリタ・型推論器の実装 (3回前期)
- MLのコンパイラの実装 (3回後期)
どちらも実験資料がインターネット上に公開されています．
参考文献
次回予告
KMC Advent Calendar
明日は @opepeman_FE さんで「たぶん聖地巡礼記2018」です．
言語実装 Advent Calendar
明日は @h_sakurai さんで Prologによる多相レコード計算の実装(2) - Qiita です．
KMCM
KMCでは，プログラミング言語の実装がどうなっているのか気になって夜も寝られない部員を募集しています．KMCに入部制限はありません．どなたでも入部できます．詳しくは入部案内ページをご覧ください．
また，KMCはコミックマーケット95にも出展します．ゲーム・音楽CDの頒布を予定しています．ぜひお越しください．
◎あなたのサークル「京大マイコンクラブ」は、日曜日 東地区“タ”ブロック－31a に配置されました。
— 京大マイコンクラブ (@KMC_JP) 2018年11月2日
さらに，去年に引き続き部員がイラストを描いて投稿するアドベントカレンダーが動いております．こちらもどうぞ．
