こんにちは､びしょ～じょです｡ 気づけば2021年も4月なんですが､3月に開催されたPPL 2021の話をします｡ 今回はもう学生ではないんですが､弊株式会社HERPがゴールドスポンサーになったので､その参加枠を使わせてもらいました｡
去年のPPLはちょうどコロナがやばまる時期でオンラインでも発表なし､資料のみという悲しい感じでしたが､今回は基本Zoomによるオンライン開催でした｡ ポスター発表+いつもの懇親タイムはGatherでおこなわれ､オンラインイベントとしても洗練されて面白かったです｡
全発表を逐一書いてくのもアレなんで､印象に残った発表を2つ紹介します｡
control/prompt の仮想機械導出
論文はこちら
すでに shift/reset での研究はあり､今回は control/prompt｡ control/promptはcontrolをときの文脈としてtrailという継続の列をもち､これを仮想機械に落とすには shift/reset のようなconsでつなげていくリストではなくappend操作が必要になる｡ この研究で導出される仮想機械は､いつどのタイミングでスタックをヒープにコピーするかを明確にモデル化したものとなり､control/promptをもつ言語の処理系の低レベルな部分の実装の基礎になることが期待できる｡
コントロールオペレータキッズなんで単純に気分がアガった｡ プログラム変換を一応やってたけど仮想機械導出という分野には明るくなかったので知らん話が結構でてきて面白かった｡ ぶっちゃけ継続の列がtrailと呼ばれてるのも知らんかった｡ 変換のパイプラインがきれいに別れていて分かりやすく追えてよかった｡
同浅井研の"A Functional Abstraction of Typed Trails"(from PEPM 2021)もcontrol/promptに型を付ける発表で面白かったです｡ "様々な限定継続演算子のための型システムの｢決定版｣を作る"という激アツな野望を掲げていてめちゃくちゃ良い｡ 浅井研は発表がうまい｡
Signature Restriction for Polymorphic Algebraic Effects (ICFP 2020)
論文(arXiv)はこちら
Polymorphic effectsとpolymorphic typesを合わせるとだいたい事故ることが知られており､その問題に対して様々なアプローチがある(e.g. ref, value restriction)｡ この研究では､effect interfaceを特定の形に制限することで(signature restriction)問題解決を図る｡ ある型変数\(a\)を持つeffect signature\(\mathit{op}:\forall a. \tau_1\rightarrow\tau_2\)に対し､
- \(\tau_1\)に\(a\)が現れるのはnegative or strictly postive positionのみ
- \(\tau_2\)に\(a\)が現れるのは(non-strictly) positive positionのみ
という極めて簡単な制限｡ ところでpolarityはざっくり述べると､ある型\(\left(\tau_1\rightarrow \tau_2\right)\rightarrow \tau_3 \)に対して
- \(\tau_1\) は(non-strictly) positive position
- \(\tau_2\) はnegative position
- \(\tau_3\) はstrictly-positive position
定義の詳細は論文を御覧ください｡
小粒だけどめちゃめちゃ効いてくるアハ体験的な研究が好きなので良かった｡
ポスターはEffektとかKokaに関するものがあって､今年もalgebraic effects元年来たな!! という感じで面白かったです｡ 元指導教員様とも一瞬同一のポスターセッションで会って背筋がピンとなりました｡
他にもよくわかんないけどすげーとなる発表が多々あり､非常に面白かったです｡ 同時に､大学卒業してから論文を全然読めてないので話に追いつくのがやっとだったり大学いた頃よりもわかるようになった話無いなとか自分に対して危機感を覚えました｡ 上記の語彙や理解力が危機感の象徴です｡ PPL2022はまた例年どおり温泉街で飲酒および歓談ワークショップとして開催されることを切に願います｡
ここでCMです｡ PPL2021のゴールドスポンサーである株式会社HERPはプログラミングおよびプログラミング言語に詳しい人材を募集しています｡ 型と値の安全性と表現力の間をかいくぐってウェブアプリケーションを開発してみませんか｡ つくばオフィスは3時間並ぶラーメン屋まで徒歩10分弱で､閉店間際に行くとほとんど並ばずに食べられます｡
この記事は業務時間中に書かれました｡