2024年3月22日に『PPL 2024 非公式ふりかえり会』を開催しました。イベントでお話した内容を文字起こし形式で紹介します。こちらは後編です。
前編はこちら▼ product.st.inc
量子論理、型のエイリアス
藤村：次は『Automated Quantum Program Verification in Dynamic Quantum Logic』ですね。量子論理で形式検証するのは大変そうだし、どうするのかなと思ったんですけど、量子論理と動的論理っていうのがまずわからない。わからないものが2個接続されていて、なかなか難しかったです。まず量子論理自体が何なのかっていうのをよく理解するところから始めないといけないのでハードルは高いですけど、面白そうだなと思った領域ではありました。
笹田：なかなか縁遠い感じですね。（資料を見ながら）検証をちゃんとするんですね。検証しないといけない分野ではありますけど、モチベーションは理解できます。
藤村：『Untangled: A Complete Dynamic Topological Logic』は、僕は哲学の方しか知らないんですけど、様相論理の方法を拡張してるってことだけはよくわかって、オペレーターが2個増えてたなっていうのはわかった。でも様相論理を拡張するといろんなことができるっていうのはそれはそうだが、道具としてはなかなか難易度が上がるんだろうなって思いましたね。ちょっとだけ雰囲気がわかる話でした。
午後の発表で印象に残ったものはありましたか？
笹田：『型別名を保存する型推論アルゴリズム』ですね。型のエイリアスを入れておくと展開されてエラーメッセージがつらい。
藤村：わかる。わかるというか、こういう型が凝った言語をやると誰もが苦しみそうな話で、メンテナビリティ的にわかるとなっていた人が多かったのではないだろうか。
遠藤：動機はすごくわかりやすくて、アプローチは思ったよりはるかに難しかったのでびっくりした覚えがありますね。
yubrot：めっちゃ素朴な疑問ですけど、TypeScriptってこういうのをどうやってるんですかね？
遠藤：TypeScriptだと、エイリアスは尊重されたエラーになるんですか？
藤村：どうだったかな。展開されたら困っちゃいますもんね。それは誰もがわかってる課題ではあるんだよな。
yubrot：たまにTypeScriptで展開されたエラーがでてきて、展開されてるなという気持ちになったことがある。
藤村：一見簡単そうに見えるし、誰もが抱くニーズなんだが解決するのは難しい課題の一個なんですね。
遠藤：今試してみたけど、展開されますね。簡単な例では展開されてエラーになっているような気がする。
藤村：どの言語でも悩まされてる課題なんですかね。普通にエイリアスがちゃんと保存されてついたらエンジニアの生産性も上がりそうですけどね。
PIMアーキテクチャ
yubrot：『Nested Data Type における多相再帰のための主要型付けを持つ型システム』はモチベーションはわかるんですが、こんなに難しくなっちゃうのかと。
藤村：そうですね。これはPPLに参加されてたり興味を持ったりする方はなんとなく想像がついているのかもしれないけど、一般の人はそう思わないかもしれないですね。素朴にできてほしいなって思いそうな気がする。
『多相型に基づく型エラー診断の定式化』は記憶があります。
笹田：SATysFi が出すエラーをいい感じにしましょうって話でしたっけ。エラーのカスタマイズか。やってることは大変そうだなと思いました。
藤村：そうですね。 『PIMアーキテクチャ上の探索木B+-forestにおけるデータの動的な再配置』は、産業界でアプリケーションコードをただ書いてる自分は全然知らないものでした。そういう仕組みにすると色々な課題があるだろうなって、なんというか引き出しが増えてよかったなっていう話でもありましたね。
笹田：これが一番PPLの中でハードウェアに近い発表でわかりやすかったですね。新しいコンピュータアーキテクチャの上でどうソフトウェアを作るかみたいな話でしたね。
藤村：テックジャイアントが実用化してたりしたら面白いですけどね。
遠藤：並列計算をやるよりも、こういう使い方の方がいいんですかね。
笹田：並列計算機の一つのやり方だと思うんですけど、メモリの方に計算機が付いていて、そこにメモリに直結した小さな計算機に何かさせるっていうアプローチですけど、インターネットワイドでもエッジコンピューティングとかありますよね。スケールを変えていろんなことを今試している中のひとつっていう話だと思います。
藤村：エッジコンピューティングのもっとミクロなやつって感じですよね、抽象的には。
笹田：いろんなつなぎ方があるので、その中でそういう計算機を作ったというか、どこかにあるのでそれのためにいい感じのアルゴリズムを作ったという話でしたね。
遠藤：一つのクエリで、一つのPIMのノードだけが計算するわけですよね。他はそういう意味だと遊ぶというか、他のクエリが来たらそっちを並列に走らせられるかもしれないわけですけど。背景が目新しくてすごいなって感じです。
藤村：触れるものがあったら面白いですけど、一般人が試せることはなさそうだと思いました。インターネット業界だとエッジコンピューティングは1年で急速に普及していて、みんなCDNにある小さいWasmとかのランタイムで何かの仕事をするっていうのがポピュラーになった。なので、どこかで流行ったら面白いですね。あとはプログラミング言語の作り方も変わりそうだと思いました。
証明木の教育に使うツール、Rubyのスレッドをどう作るか
藤村：次が『定義のデータ化による証明木可視化システムMikiβの拡張』。証明木を書くのは大変っていうのがモチベーションなのは、そうだろうなと。使いやすい中間データ構造があるんじゃないかと思うんですけど、そうもいかないし、使いやすい中間データ構造の簡約を進めていくとそのまま可視化できるんじゃないかと思いましたが、そんな簡単でもないんでしょうね。あとは現場でアプリケーションコードを書いている人間から見ると、UI開発の難易度が高い部類のものなので、中身もさることながらUIの開発が本当に大変そうだなって思いましたね。yubrotさんも思いませんでしたか？
yubrot：大変そうな感じがしましたね。
藤村：あれは難しいですよ、大変だと思いますね。複雑なGUIの極地みたいな感じで動的な要素も多いんでそうですよね。
笹田：こういう証明木とかを使う教育はまだまだホワイトボードとかなんですかね？
藤村：どうなんでしょうね。ワープロソフトやエクセル、組版のソフトでうまくできるかっていうと難しそうですよね。
笹田：パワーポイントにアニメーションをつけているのかもしれないですけど。そういう教育を受けたことがないので知らないんですが。
藤村：一方でああいうのって、絵に書いてあるものが動いて減ったり増えたり、進んだりすると理解しやすいので、教育上は重要なんだろうなと思いました。笹田さん、発表はどうでしたか？
笹田：『Rubyにおける M:N スレッドの実装』というテーマでお話しました。言語処理系を実際にどう作るかの話は多分私だけだったんじゃないかな。泥臭いところをどう実装するかですね。Rubyのスレッドをどう作るかという話で、スレッドローカルストレージっていうものの実装にちょっと困難があって、こんな感じでごまかしているという話をしたんですが、その辺にちゃんと質問をいただけてよかったです。
藤村：そういう面ではGo言語が先輩なんですか？
笹田：そうですね、Goの真似をして、真似しきれてないところは結構あります。PPLで並列並行っていうと、いろいろな抽象化を使ってどう証明しましょうかという話になることが多いので、同期のためのプリミティブで命令数が何命令減りましたといった話はあんまりなくて、場違い感があってある意味面白かったです。
バージョン管理に夢を感じた
藤村：『Compilation Semantics for a Programming Language with Versions』は、現実的に仕事で大変困っている人間としては夢を感じましたね。
yubrot：本当にそうでしたね。
笹田：発表者がいらっしゃいますね。
田邉さん：ありがとうございます。まだ議論先行で使えるものになってないので、次はもうちょっと実用的な方に近づけようかなと思っております。
笹田：この辺に着目されたのはどういう経緯なんですか？バージョンで困ってたんですか？
田邉さん：もともと僕が学部生の時にテーマを投げられた時は、もっと理論先行だったんですけど、それにどちらかというと学生の身分で実用的なモチベーションを見つけてきてくっつけたという感じですかね。徐々にそっちに移行してきたくて、今はあんまり理論の話とか発表でもほぼせずに、実用的な使い方とかモチベーションの話ばっかりしてるっていう感じですかね。
遠藤：これって先行研究とかあるんですか？
田邉さん：ないですね。結構サーベイしましたけど、同じようなことやってる研究は多分ないと思いますね。なのでむしろ論文を書きにくいというか。
遠藤：そうなんですか。真似するところが難しいというのは確かにそうかもしれないですけど。先ほどみんなも褒めてましたけど、僕もPPLの中で今回一番実用に近い課題を扱ってる感じだなというので面白かったです。ラムダ計算してたけど。
藤村：PPLのSlackでもコメントさせていただいて、お返事ありがとうございました。そのアプリケーションコードでレガシーなんとかっていうのとか、バージョン1っていうサフィックスをつけるとかで徐々に切り替えてくるみたいなことは頻繁にあって、嬉しくはないんですけど、またライブラリの更新とかも毎日やっているチームがうちでも何チームかあるレベルで溜めると本当に大変で、で溜めると本当に予想外のことが起きたり起きなかったりして苦しいので、Rubyにも入ってほしいなぐらいの気持ちを持ちながら聞いていました。
田邉さん：PythonじゃなくRubyで。
藤村：これはRubyにあるとキラー機能だと思うんですけどね。毎日アプリケーションコードを書いてデプロイしてる人から見ると嬉しいと思うんだよな。実用的なニーズがめちゃあるだろうなって思いました。お話いただきありがとうございました。
後方参照のある正規表現
遠藤：論文賞をとっていた『Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness』ですね。学生の頃からなんとなく後方参照のある正規表現ってどういう表現力なのか気になっていたんで、それを真面目に研究されてて面白かったですね。後方参照のある正規表現って、文字列の長さが素数長か判定するのに使えるというのがあって、表現力が気になってました。
藤村：Googleが出してるRE2は後方参照までないんでしたっけ？
遠藤：後方参照はないですね。
藤村：ですよね。後方参照の扱いが上手になると、正規表現のエンジンがもっと違う方法で書けるようになって世の中のプログラムが速くなるのかもしれないですね
笹田：この研究自体はある種のREwB（Regular Expression with Backed Recreation）というクラスを作って、それの表現力を評価したっていう話ですよね。こういう研究はちょっとずつ広がっていきますよね、科学の進歩みたいな感じがしてかっこいい。
藤村：当たり前なのかもしれないですけど、計算機の理論の研究って進化しているんだなっていう感覚をつかめただけで僕はすごいありがたかったところもあるし、そういうのはもっといろんな人に味がってもらえるといいんじゃないかなと思いましたね。
余談ですけど僕はちょっと初心者向けのPPLみたいなのがあったら、職業エンジニアの人がいっぱい来るんじゃないかな、そういうのがあるといいのかなと思いました。
笹田：PPLって、わかってる人向けに喋るので、難しいところがあるんで、初心者向けのPPLがあるといいですね。
藤村：CTOという立場からも「行ってきなよ」と言いやすいですね。
笹田：ソフトウェア学会でチュートリアルとかを時々やってるので、近いのかもしれない。
藤村：そういうのは産業界にとっても喜ばれそうな気がしましたけど、それは僕がこの手のジャンルに興味があるからっていうバイアスがかかってるような気がしました。
「変なところでマッチする正規表現を書いたことがない人だけが石を投げなさい」
遠藤：実用性っていう話だと、『文字検査可能・区分検査可能・一般化有限確定言語における可測性の計算量解析』は面白かったですね。理論的に興味があるんだろうなっていうのが正直な印象ではあったんですけど、それを使って正規表現のマッチングをフィルタリングのように使うという応用を示して話しているのが印象的でした。
藤村：しかもそれに着地するためのルートはすごく抽象的なものじゃないですか。それもまた面白かったですね。現実につながるのかぁという面白さがあった。
遠藤：現実につなげるというストーリーをつけて話していたのが面白かった。
笹田：これに関しては本当に素人なんですけど、計算量の解析をするっていう話だと思うんですけど、ここで計算量がわかるとどういう嬉しさがあるんですかね？
遠藤：なにかのルールで書かれた言語のマッチング判定をしたい時に、それよりもうちょっと簡単に、下から近似するのと上から近似するので、これにマッチしないんだったらマッチしないとか、これにマッチするんだったらこれにはマッチしないっていうのを無限に狭められる性質を研究しましたという話だったと理解しています。つまりフィルタリングに使うという話なのかなと。
笹田：こういう研究のモチベーションっていうのはちゃんと明らかにすることが大事っていうのもわかるんだけど、どういうところから興味がわくのかに興味がありました。
藤村：僕は『正規表現技術入門』のファンだったので、直接話が聞けて嬉しかったですね。
『Regular Expressions with Backreferences on Multiple Context-Free Languages, and Star-Closedness』と『Repairing Regular Expressions for Extraction』のセッションは、正規表現の捉え方が違って、ボトムアップで理論的なアプローチだが現実的なモチベーションに向かうのと、生の仕事での正規表現の観点から向かうコントラストが面白かったです。意図と違う正規表現が書かれるっていうこと自体が言語表現として面白いなと思いました。意図と違うものを書きやすいっていうのは自然言語だとそうかもしれないですけど、正規表現もそうなんだというのが個人的に興味深かったです。
遠藤：正規表現は難しいですよね。変なところでマッチする正規表現を書いたことがない人だけが石を投げなさいって感じで。
藤村：最近、人々は正規表現をLLMで書くんですよね。ChatGPTに「こういう正規表現を書いて」という手法が知られているらしい。僕もそうなんですけど。
遠藤：人間が書いても間違えるんだからっていうのはあるかもしれないですね。
藤村：ということで、3日目でした。
fluent interfaceに対する気持ち
笹田：ポスターも色々ありましたね。わかりやすい発表が多くてよかったです。
藤村：遠藤さんはポスター発表『型注釈のないRubyプログラムのデータフロー解析に基づいたIDE支援』をしてみてどうでしたか？
遠藤：色んなコメントをいただきました。
笹田：たくさん来てくれましたよね。
遠藤：ツールの穴を見つけてくれる人がPPLならいるんじゃないかと予想していたんですが、3名くらいいました。再帰呼び出しをすると型推論の結果がおかしくなるんじゃないですかと言ってくれた方がいました。この割り切り方だとスケーラビリティもでますね、とか、フィードバックをもらいました。
笹田：10番の『LLMを用いたトランスパイラの正確性向上と、その評価について』は高校生の方でびっくりしました。先生に言われて発表したのかを聞いたら、自分で発表することにしたとのことでした。
藤村：yubrotさんは、ポスター発表でどれが面白いと思いましたか？
yubrot：どれが面白いというか、印象的なことの一つに『代数的エフェクトにおけるエフェクトのperformを可視化するシステムの開発』ですね。代数的エフェクトという言葉を現実世界で目にすることがあるんだなって。
藤村：物理的なものに書いてあるのを初めて見たっていう。
yubrot：37番の『演算子オーバーロードを利用したfluent APIとその型付け』はライブラリでも見かけるなぁと思いました。
遠藤：メソッドチェーンをいっぱい書くような形じゃなく、メソッドチェーンじゃなく式を結合して書きましょうという話でしたよね。
笹田：fluent APIが研究分野になっているんですね。
遠藤：1日目の19番『どのような文法からflat/sub-chainingのfluent interfaceを生成できるかを考える』もfluent APIの発表でしたね。
藤村：fluent interfaceなぁ。アプリケーションエンジニアとしてはそんなに気持ちがない手法ですね。
笹田：みんながActive Recordを好きなのはそれが理由じゃないんですか？
藤村：Active Recordも難しくなるとすぐSQL書いちゃうんで。SQLとかO/Rマッパーをfluent interfaceとか埋め込みDSLで書こうというモチベーションは気持ちとしてはわかるんですけど、どうなんだろうな。仕事ではあんまりハマらなかったんだよなって気持ちがある。
yubrot：今あるプログラミング言語側にfluentに書けるような言語機能が乏しいっていう考え方もできるかなと思っていて、例えばD言語のUniform Function Call Syntaxがあると、ネストした関数呼び出しの構造をチェインしたような形で書けて、見やすくなる、そういうのがあると今fluent interfaceって名前が付いてるけど、もっと普通に使えるのかなとか。
藤村：それで一番実用的かつ使われてるのはHaskellのdo notationだと思うんですよね。もうあれでよくない？みたいな気持ちがあって。他の言語でやろうとするとfluent interfaceになりますよね。最近Goでも頑張ってやろうとしてるライブラリがあります。
ただの感想ですけど、スマートコントラクトやブロックチェーンの話は意外とちょっとしかなかったですね。Haskellの人々はブロックチェーンの会社にたくさん行ってたなとか、僕が一緒に働いていた知人は今ドバイに移住して、スマートコントラクトの検算をするソフトウェアを作る会社をやり始めたそうで、産業的にもホットな感じでしたけどね。
遠藤：59番の『Postの対応問題に対する様々なアプローチ』は、個人的に好きなパズルみたいな問題で、色々と解決していたのでかっこよかったですね。
藤村：確かに面白かったですね。
遠藤：マイクロとペアの順番を構成して、ペアの中身を完全に一致させることができますかっていうようなパズルで決定することが知られているので、解けないということを証明するのが大変で恐らく解けないだろうとされている問題が山のように転がっているんですけど、それらを賢い方法で解けない証明をどんどん作ったという話でしたね。
藤村：1個解決できるものが見つかったってやつですよね。
遠藤：3000とか、そのくらいだいぶまとめて解決していたのでかっこよかったですね。残り8個と言ってたような気がします。
コード補完を中断する理由、プログラマーがコードを書く時に持っている意図
遠藤：66番の『プログラマーがコード補完を中断する理由の調査』も面白かったですね。
藤村：面白かったですね。
yubrot：観点が面白かったですね。コード補完を中断する理由って、その発想はどこから出てきたんだろうって思いました。
藤村：候補を調べるためにコード補完させたりもするんですよっていう話もあって、実際そうなんですよねみたいな話になって面白かったですね。
笹田：そういうデータが公開されているというのをちゃんと調べてるという点がなるほどとなりました。昨日聞いたんですが、この研究自体は続けないそうです。せっかくここまでやったんだから残念だなって。
岩田さん：こんばんは、岩田です。
笹田：もうやらないんですか？
岩田さん：この研究は大学でやる研究として見ると、それより先をもっと深掘りして、この人がどういう意図を持ってコード補完をしてるのかを調べようとすると、どうしても既存のデータセットでは足りないんですね。意図をねちねちと聞き取るような集め方をしたデータ セットがどうしても必要になると思っています。ちょっと風呂敷を広げたはいいものの、お先まっくらだなと思っているところです。
藤村：それも面白そうですけどね。ユーザビリティテストみたいな手法を使って、今なんで 止めました？ってずっと聞き続けると、いろいろ出てきそうだなって。想像とは違うものも出てきそうですね。
岩田さん：そういうデータセットを作ってしまえば、それは大きな成果にはなりそうな気がしますね。
藤村：これは僕、個人の思いですけど、プログラマーがコードを書いているときに持っている意図は一体何なのかっていうのは、哲学的にも面白いなと思いますね。こうしたいっていうのが明確にあるわけじゃない状態でコード書いている人も多いだろうから、そういう場合の意図っていうのをいったいどういうふうに表現できるんだろうとか、どうやって知ることができるんだろうっていうのも面白そうです。
岩田さん：または意図がないというか何も考えずにやってしまったというのは、そういうジャンルだと割り切って研究するのもまたありかもしれないですね。
藤村：意図がない実装中の行動の一段データセットがあるだけでかなり面白そうです。
笹田：書いてる人も言語化するのは難しそうですよね。
藤村：それが面白いなと思う。お話いただき、ありがとうございました。
岩田さん：ありがとうございました。
藤村：ということで気がつけばもう終わりに近づいたので、PPL 2024 非公式ふりかえり会を終わろうと思います。参加していただいたみなさん、お話いただいたみなさん、ありがとうございました。（完）
ポテンシャル採用のお知らせ
26年卒の学生の方、既卒、第二新卒の方を対象としたポテンシャル採用をしています。中長期実務インターンも通年で募集しています。ぜひご応募ください。詳しくは下記のサイトをご覧ください。
