私が歌川です

@utgwkk が書いている

カインドを用いたレコード多相 (record polymorphism) の計算体系とその実装

これは KMC Advent Calendar 2018 - Adventar言語実装 Advent Calendar 2018 - Qiita 4日目の記事です.

3日目はそれぞれ,

でした.

自己紹介

id:utgwkk (うたがわきき) です.学部4回生になり,プログラミング言語に関する研究をすることになりました*1. KMC部員としての生活もついに4年目です.ふだんはお酒を飲んでいます.

概要

この記事では,大堀先生の多相レコード理論の論文[1] *2について,(数学的な議論は控えめに)どういうことをやっているのかについて紹介します. また,リファレンス実装のSML# と私が書いた実装について紹介します.

record polymorphismの理論

さて,読者のみなさまの中には record polymorphism と聞いて「ああ,アレね」とすぐに理解される方もいらっしゃるかと思われますが,わたしの理解の再確認も兼ねて,それぞれの要素に分解して説明していこうと思います. すなわち,

  • 「レコード」って何?
  • 「多相性」って何?
  • 「カインド」って何?

の順に説明していきます.

なお,

  • そもそも「計算体系」って何?
  • 「型」とか「型システム」って何?
  • 型推論」って何?どうやるの?

といったことについて掘り下げていくといくら時間があっても足りなくなる*3ため,ここでは参考となるサイトをいくつか挙げるにとどめておきます. この記事を読んでいて分からないことがあれば適宜あたっていくとよいでしょう.

レコード

レコードは,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 というフィールドの値を取得する関数について考えてみましょう*4OCaml風に書くならば次のように書けると思います.

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で公開されています.

github.com

menhirを入れて make すると prog が生成されます. ./prog を実行するとREPLが立ち上がります.

変換ステップは次のようになっています.

  • 字句解析と構文解析 (入力文字列を計算体系の項を表すデータ型に変換する)
  • 型推論 (項に型情報を付与する)
  • 型検査 (項の型情報が正しいか検査する)
  • コンパイル (項を低レベルの計算体系の項に変換する)

./prog --debug を実行すると,各変換ステップ後の内部表現を見ることができます.

文法はOCaml寄りになっています.READMEBNFを参照してください. この処理系では,

let name x = x.name in name;;

のように書くことで先述のname関数を実装できます.

おわりに

レコード多相を実現するための理論についてざっくりと触れてきました. 日頃,とくに動的型の言語では何気なく書いている x.name といった式に型を付ける方法としてこのようなものがあるといったことを知ったとき,目から鱗が出ました.

この記事では触れていない部分(型推論)や,数学的な定式化などについては論文を参照してください. この直観はさすがにずれているのではないか,などの指摘がありましたら id:utgwkk までよろしくお願いします.

余談:プログラミング言語処理系実装の実験について

京都大学工学部情報学科計算機科学コースでは,学生実験として3回生のうちに言語処理系を実装する機会が2回あります.

どちらも実験資料がインターネット上に公開されています.

参考文献

  1. Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, vol 17, no 6, pages 844-895, 1995.

次回予告

KMC Advent Calendar

明日は @opepeman_FE さんで「たぶん聖地巡礼記2018」です.

言語実装 Advent Calendar

明日は @h_sakurai さんで Prologによる多相レコード計算の実装(2) - Qiita です.

KMCM

KMCでは,プログラミング言語の実装がどうなっているのか気になって夜も寝られない部員を募集しています.KMCに入部制限はありません.どなたでも入部できます.詳しくは入部案内ページをご覧ください.

www.kmc.gr.jp

また,KMCはコミックマーケット95にも出展します.ゲーム・音楽CDの頒布を予定しています.ぜひお越しください.

さらに,去年に引き続き部員がイラストを描いて投稿するアドベントカレンダーが動いております.こちらもどうぞ.

adventar.org

*1:私の大学では4回生になると研究室に配属されます.

*2:厳密には論文の体系からヴァリアントを抜いたサブセット

*3:そもそもわたしが説明しきれない気がするのだよな…….

*4:これは論文でも同様の例が取り上げられている.

*5:たとえば SML/NJでは実装できない

*6:OCamlでは name を含むレコード型を定義すれば関数を定義できるようになる.

*7:レコードがなくて配列がある.

*8:私のMacではビルドすることができた.

区切りの効能

わたしはもともと作業に没頭するとなかなか抜け出せないタイプだった. そのため研究室でコードを書いていたところ気がついたら20時を過ぎていたとか,あるいは家で続きを書いていたら朝になっていた,ということがあった.

/remind me 定時です at 18:00 every weekday

ここでは定時の概念はSlackのリマインダーとして顕現する. 平日の18時には必ず定時が知らせられ,気持ちに対する割り込みが起こる. 作業が終わりつつあるときには,それでは今日はここまでやってしまって終わりにしようとなり,あるいは定時近くになると,とりあえずあのタスクぐらいはやってしまおうとなる.

これは時間的な区切りの概念だいたいについて同じようなことが言えるのではないかと思う. 大きな区切りは遠くに見えるけど,どれくらい遠いのかが分からない. したがって小さな区切りによって少しずつ近づいていくのがいいのではないか.

いまは可変でない「定時」という区切りを導入し,まあうまくいっているのではないだろうかという段階. まだ運用を開始して1週間も経過していないので引き続き経過を見ていこうと思う.

皮膚科の効能

5月末ぐらいにもらった薬がなくなって,寒くなって表面がぼろぼろになってきたのでついに皮膚科に行った. 今までどおりの薬をもらって塗ってきたところかなり回復した.

まだ大丈夫とか,お金がもったいないとか,適当に薬だけ買えばいけるやろとかそういうことはないと思っていて,専門家に見てもらって適切な処理を受けるのがいちばんはやいし安い. いま行っている皮膚科は,診察のときにめちゃくちゃ長い世間話とかはなくて,

  • 最近どのようになっていますか
  • このようになっています
  • ではこうしましょう
  • ところで今ほかに困っていることはないですか

で終了するので,会話が苦手な身としてはかなり助かるし,なにより時間がかからない.

wsl-terminal が chsh 認識してくれない問題 (解決編)

utgwkk.hateblo.jp

この記事の続き.

いつの間にか -l オプションで起動したのち exec /bin/zsh が効かなくなったのでいろいろ調べてたところ,なんと -l で起動されるシェルは chsh で指定したものとは関係ないことがわかった!

github.com

そしてよく見ると,この設定ファイルは (wsl-terminalのroot dir)/etc/wsl-terminal.conf のことを指しているらしい. 当該ファイルの shell オプションを書き換えると無事にzshが起動された.

そしてさらに驚くべきことに,当該事項はちゃんとREADMEに書いてあった……. 丁寧にログインシェルを /etc/passwd のものに書き換えるバッチファイルまで添えてあった.

github.com

教訓

READMEを読もう.

ISUCON8 :thinking_face: 本戦に出て14位だった #isucon

チーム :thinking_face: *1 として学生枠でISUCON8の本戦に出場しました. 今回のお題は「仮想椅子取引サービス ISUCOIN」でした.

結果は5,981点で14位(ベストスコアは6,324点)でした. 学生の中では5位だったけれどそれ以前に学生のレベルがめちゃくちゃ高かったですね……*2

やったこと

予選とだいたい同じで,

  • id:wass80 がアプリを概観したのちやっていきのある実装をやる
  • id:nonylene がインフラまわりの作業をぜんぶやる
  • id:utgwkkSQLを改善したり,すぐできる実装をぱっとやる

という分担になりました.

他のふたりがやったことはそれぞれのブログを読んでもらうとして,ここでは私がやったことを書きます.

scrapbox.io

nonylene.hatenablog.jp

N+1クエリの解消

model/ 以下にDBの各tableに対応するモデルファイルが置いてあり,クラスが定義されていました(なんと型アノテーション付き!). じつはこれは罠で,とくにOrderとTradeにN+1が埋め込まれていました.

N+1のある関数が呼ばれるのは精々数回だったので,丁寧に切り出してJOINに書き換えました.

Fix N+1 on /info by utgwkk · Pull Request #7 · wass88/isucon8-final · GitHub

Fix N+1 query on GET /orders by utgwkk · Pull Request #9 · wass88/isucon8-final · GitHub

_get_latest_trade()LIMIT 1 を付ける

_get_latest_trade() は文字通り最新のTradeを取ってくる関数なのですが,じつは最新の1件しか使わないのでクエリに LIMIT 1 を付け加えました. 確かこれがいちばん効いて,それまで1000点も出なかったのが突然3000点ぐらいまで上がったと思います.

LIMIT 1 · wass88/isucon8-final@9783f73 · GitHub

SettingsをRedisから取ってくる

Settingsは GET /initialize でのみsetされ,あとはgetしか行われないので,ここをDBから外す作業をしました. はじめはグローバル変数dict に乗せていたのですが,そうするとgunicornで起動したときに /initialize を受けたプロセスでしか初期化されずFAILしていました. そのため各サーバにRedisを入れ,そこにSettingsを格納しました.

Do not use database for settings by utgwkk · Pull Request #4 · wass88/isucon8-final · GitHub

always get settings from Redis · wass88/isucon8-final@24c80be · GitHub

やらなかったこと

インデックスを貼る

今回はインデックスにはとくに手をつけませんでした. 各所に重たいクエリがあるのでまずそちらをどうにかしなければなーと思っていたら競技が終了していました.

ろうそくの改善

ろうそくを出すときにかなり重たそうなクエリが投げられていることは分かっていたのですが,最後までどうにもなりませんでした. MySQL 8.0なのでwindow functionが使えるしなんとかならないか!? と思ったけれどすぐにできるものではなかった…….

SNSシェアを有効にする

終了30分前ぐらいに,SNSシェアしたらどうなるか見てみましょうということで,

res["enable_share"] = True

をやってみたところ当然failしたのですぐに差し戻しました.

懇親会で聞いたところ,appサーバのうちどれか1つだけでSNSシェアを有効にするとか,一定確率で有効にするとかの戦略を取るのが正しかったようです. 巷ではこれをA/Bテストと呼びます.概念は知ってたけどそうする発想が出なかったのでめちゃくちゃ悔しい…….

サーバのリソースにはわりと余裕があったので,少しだけ有効にしてたら10000点は出ただろうなーと思っています.

ユーザのBAN

これも終了30分前ぐらいにエイヤッとやったところ当然failしたのですぐに差し戻しました. そもそもSNSシェアがかなりの割合で有効になってきてから効くようになるとのことだったので,早とちりでしたね…….

感想

テーマとしても面白く,かなり考えられた問題だなーというのが分かりました. 現代のwebサービスはアプリ内部だけ完結せずに外部APIと連携するものが多く,それを踏まえたテーマとなっていたように感じます. 懇親会で他のチームの方や出題者の方々とお話をしたところ目から鱗となる戦略がどんどん出てきて,やはり実力があるなーと思いました.

チームメイトの id:wass80 id:nonylene ,運営の皆様,他チームの皆様,そしていろいろなところでISUCONを支えてくださった皆様ありがとうございました.めちゃくちゃ楽しかったし勉強になりました. 学生のレベルがだんだん上がっており,しかも来年から学生枠がどうなるか不明という話を耳にしてビクビクしていますが来年も出たいです.

*1:team id:18

*2:もちろん社会人枠の方々のレベルもかなり高かった.

KMCの例会講座で「ラムダ計算のインタプリタを実装してみる」話をした

speakerdeck.com

KMCの例会講座で,型無しラムダ計算についての軽い説明と,そのインタプリタを実装した話をしました. できた実装はこちらです.

github.com

講座の流れ

  • ラムダ計算について知ろう
    • ラムダ項
    • 束縛変数と自由変数
    • 変数の置換(代入)
    • α変換
    • β簡約
  • ラムダ計算のインタプリタを実装しよう
    • 仕様の決定
    • データ型の定義 (syntax.ml)
    • 構文解析の実装 (parser.mly)
    • 字句解析の実装 (lexer.mll)
    • De Bruijn indexへの変換の実装 (deBruijn.ml)
    • β簡約の実装 (deBruijn.ml)
    • デモ

動機

ラムダ計算を実装するという体験の共有

ラムダ計算は計算体系の1つで,

  • 関数抽象(関数をつくること)
  • 関数適用

2つの操作によって構成されており,これだけでチューリング完全になります.

わたしは研究分野の性質上,ずっとラムダ計算を拡張した体系の論文を読んでいます. しかし今まで,その数学的な性質を確かめていても,簡約が機械的に行われることは自分の手で確かめていませんでした.

そんなわけで 論文を読むのがダルいときに 実装を進めていました. できあがったものの共有というのが講座をやった動機の1つです.

実際,じぶんの知っているラムダ計算の知識だけではうまく簡約ができず,試行錯誤する必要がありました. そういったつまずき体験を共有し,解決策についても共有する*1ことに講座のもう1つの意味があります.

プログラミング言語の処理系について意識してもらう

プログラミング言語コンパイラインタプリタがどのように実装されているか,というのは,普段のプログラミングではなかなか意識しないことだと思います. そこに少しだけ意識を向けてもらって,ザ・メイキングを見るときのような気持ちになってもらったり,よくわからないけどいろいろな世界があるのだなと思ってもらったりする,というのが講座の動機のもう1つです.

質問

講座のあとに出てきた質問とその回答,フィードバックを記録します.

β簡約のステップがよくわからなかった

私も最初はなぜこれでうまくいくのか全くわかりませんでした*2. 簡約のステップをスライドに示しつつやっていたので,そのスライドを再掲してゆっくり追ってもらいました.

じつはスライドに示した規則はβ簡約の規則の1番目に過ぎません. 項全体だけではなく,項のある一部分だけについても同様にβ簡約してよい,という規則があります. これは住井先生の「計算機ソフトウェア工学」の講義資料などにより正確な説明があります.

今回の講座ではそれを含めずにβ簡約について説明していたので,含めたほうがよかったですね*3

実装期間はどれくらいか

2週間ぐらいで実装しました.10/7には作業をした形跡があったのでそれぐらいの時期からやっていたようです*4

今後どこまで実装していくのか

ひとまずは「今後の課題」に挙げたものが解決できるとよいなーと思っています.

型を付けることに関しては,いちおう単純型の型推論がすでに実装されています. しかし講座でそこまで取り上げると型の説明のために時間が長くなってしまうとみて今回は割愛しました.

De Bruijn indexにおける自由変数の扱いについて,どうにかしたいと書いていましたが,諦めるしかないという結論になってきました. そもそも自由なので外部環境が変化すればindexも変化するため,外部環境が不明な状況では放っておくしかないでしょう.

その後

例会後に今更SICP読書会というSICPを読む会がありましたが,そこでチャーチ数に関する練習問題が登場し,人々が格闘していました.

わたしはWikipediaをチラ見しつつ階乗を求めるラムダ式を書いていました. Y (\fn. IFTHENELSE (ISZERO n) (\fn.fn) (MULT n (f (PRED n)))) を少し簡約したのが以下の式になります.

ところでこの階乗関数からYコンビネータを取り除いても型検査に落ちるのですが,そういうものなのでしょうか.

追記

発表原稿を公開しました

*1:あるいは解決できなくても試行錯誤の過程を共有する

*2:今もぜんぶ分かっているかについては自信がない.

*3:実際に,スライドの参考資料[1]ではβ簡約をleast compatible relation satisfying ~というふうに定義しています.compatible というのが今回示さなかった規則にあたります.

*4:commit logはいちど消し飛ばしてしまった…….