帰りの新幹線から書いています。次の日が普通に勤務があるので......(なぜ休みにしなかったのか)
7/11 7/12に開催された関数型まつりに参加登壇しました。
公式サイト
プロポーザル (fortee)
登壇資料 (SpeakerDeck)
登壇の感想
今回プロポーザル式かつ参加が基本有料なカンファレンスでの登壇が初めてということもあり、それなりに緊張や不安を抱えて臨みました。
結果としては特段大きな失敗がなく無事に発表ができたと思います。
裏番組がとても魅力的(分裂して聞きたかった......)なのもあり、自分の発表を応援しに来てくれた友人が来てくれたらいいかな、と思っていましたが自分の想定より多くの人に聞いてもらえたのがうれしかったです。
また発表のあとに話を聞きたい！と集まって議論ができたのも同じくうれしかったですし、登壇してよかったと思いました。
とはいえ、今回パーサをテーマにしたとはいえ、自分が調査した範囲はかなり基礎をなめているにとどめているので、発展的な話題を広げられなかったのは若干の反省かなと感じています、おすすめも教えてもらったのでまたそちらは勉強したいです。
Twitterの反応も登壇後に見ましたが、全体的に温かく見守ってもらえたので安心しています。
登壇した内容について
登壇内容の詳細は登壇資料に譲りますが、もともと関数型を体験する入口が少ない・あるいはあっても見つかりにくいということを感じていました、一つ目的として関数型を始まる入口が増やせたら、と思ったので今回「パーサやってみようかな」のようなフィードバックをいただけて達成できたと感じました。
関数型まつり全体の感想
自分は普段PHPCon・PHPerKaigiに参加することが多いのですが、そちらとはまた違った雰囲気があったと思います。
トークも実装やプロダクトよりは、理論的な技術に関する発表が多いのが特に印象的でした。自分が聞きに行ったセッションは何となく理解できたと思うので、自分が勉強してきた関数型の知識はちゃんと根付いてる......はず。
懇親会がDay1にあったのも初めてで、毎度ご飯と会話のバランスを見誤る悪癖があるのですが、今回も例にもれず話過ぎてご飯を取りに行こうとしたらすでにほとんどない、みたいな状況になりました。いったんご飯だけさっと取りに行くのが一番いいですね.......。
関数型の話はもちろん、カンファレンス運営の話なんかも聞けてとても有意義な時間でした。
個人の反省としては、登壇資料を当日まで作成していたのでそちらに集中してトークが聞けなかったり交流が少なかったのがつらかったので、今度登壇するときは前日までに作ります。
聞いたトーク
実際に聞いたトークはこちらです
なぜ関数型プログラミングで「型」と「証明」が語られるのか
https://speakerdeck.com/kajitack/fpmatsuri-functional-programming-types-proofs-connection
関数型プログラミングとは何をするのか、どう活かせるかについてのセッションでした。個人的にはこのトークが関数型まつりの最初の入口になると思います(もちろん普段プログラムを書いている方向けにはなりますが)
型推論入門 ― Hindley-Milnerの仕組みと実装の違い
型推論の入門の入門の入門の話です。何を言ってるんだとなるかもしれませんが、型推論の入門書って入門向けではないんですよね......私も挫折経験があります(TAPLって入門書でしたっけ......)
そんな型推論の概説と、型推論を実現するアルゴリズムの紹介、さらにその中で簡素な実装のHM型推論について実装している言語がどのように実装・利用しているのかを解説しています。
個人的な発見は型推論アルゴリズムがたくさんあることで、同じ関数型パラダイムをサポートしていたとしてもその裏にある型推論・検査の実装の毛色が異なり、それはそれぞれがコンセプトにしている別の性質を保証することを優先した結果だったりするというのが面白かったです。
Algorithm WというHM型推論の実装があるとのことなので、ちょっとこれは調べてみたいです。
型は壁、Rustでもバグを直すな、表現できなくせよ
Rustでのコードを題材に、型をバグを表現させないための壁として扱う話です。
具体的な話は資料そのまま読んだ方がいいと思うので、個人的な収穫を話すと、実際に使っている型関連でのマクロやクレートの実例をいろいろしれて非常に勉強になりました。
型を表現をしすぎた場合に、結局読むコストが上がってしまうというところで、これについてはその表現した型でどの程度の不正な状態などが表現できなくなり、バグを減らせるのかの部分で取捨選択していく、というところなどは、現実的な解を探っていく泥臭い部分のエンジニアリングだと感じました。
本物のプログラマーは unsafe と型システムを使う 〜拡張可能レコードを作って学ぶ黒魔術入門〜
HaskellにおけるUnsafeと、型システムを使うことで、本物プログラマーになるためのセッション。
この発表の肝はUnsafeのような危険な操作だから無条件に採用しないのではなく、そのUnsafeに該当する操作はどんなリスクがあるのか、そのリスクを回避しながらどう有意義に使用するかという姿勢だと思います。
Haskellのコードが題材で、内容もかなり玄人向けですが、根底の思想の部分はどのエンジニアも持っていた方がうれしいはずです。
Leanで学ぼう等式推論（証明もあるよ！）
定理証明支援系の言語であるLeanで等式推論を学ぶセッションで、実際にどのように証明していくかをライブコーディングしながら体感できました。
こうした証明によって網羅的に動作を保証するのは強力ですが、はたしてその証明した命題は実際の計算と同じなのか？という部分はやはり開発する人間がきちんとデザインして確認するのが大事ですね。セッション中ではフェルマーの最終定理をLeanで証明しています。
Haskellと圏論：パフォーマンス改善からKan拡張へ
Haskellのパッケージkan-extensionの中のRanが、圏論における右Kan拡張と同型であるというのを実際に証明していくセッションです。
入口自体は、fmapに重い処理が入っていた場合に複数回適用してもfmapが重複して呼ばれないことなどをYonedaという道具を使ってパフォーマンスを改善する実例から始まり、そうした合成を入れ替えても結果が変わらない動作を実現できるRanが、圏論の右Kan拡張に接続できるというもので、圏論と実世界の道具が実際につながるところを見れるという稀有な(?)体験ができて面白かったです。
後にも紹介しますがDay2の圧縮代数にもつながる話でもあるなと個人的に思いました。
Haskell/Servantを通してWebミドルウェアを捉え直す
認証ミドルウェアのような、ミドルウェアとして組み込みたいけど、実際の実装だと受け取る方が変わってしまい合成がコンパイラや型検査機に問題がないのにエラーとして解釈される問題を、HaskellのServantはどのようにそうした問題を解消しているのかの解説。
多くのWebフレームワークのミドルウェア実装は、Handler -> Handlerとなる関数にそろえることで、それぞれを合成可能にして複数のミドルウェアをかませているが、Servantはハンドラーを合成するのではなく、一段上？のAPI仕様からAPI仕様を返し、その仕様が合成可能かつそれぞれからハンドラーを生成するアプローチをとるという形で実現できていた、というのが面白かったです。
ほしい性質も満たすために空間(型)と動作を構成し、実際に扱う空間とやり取りするケースの具体化かも。
なぜ多くの言語はHigher Kinded Typesをサポートしないのか
Rustに厳密なMonadが欲しいのにHKTsがないから無理だよドラえも～～ん、となっていたので聞きに行きましたが、HKTsが何か、どんな性質が必要なのかを見ていくとそれはかなり難しい要求だったんだな、となるセッションでした。
そもそも多くの人間が解決したい課題は十分HKTsなしでも解決できるので、わざわざ実現したいモチベが上がらないのもそうですが、そもそもコンパイラやランタイムがきちんと推論を完璧にするのが無理、というのが分かり、そうなってくるときちんと型注釈をプログラマが与えないといけないというのがポイントだと感じました。専門性とはこういうところに生まれそう(こなみ)。
継続モナドとリアクティブプログラミング
リアクティブプログラミングの概要から、リアクティブプログラミングにおけるリソース管理や依存を型で実現していくと、継続モナドで実現可能であり、またそうした実現の活用例としてエージェントの操作をシンプルな構成で実現可能といった話でした。
リアクティブプログラミングも継続モナドも自分はきちんと知らなかったのですが、解説が分かりやすく、マネできそうなところは使ってみたいとなるセッションでした。
パッケージマネージャー Nix はなぜ純粋関数型言語で設定を記述するのか
最近アツいパッケージマネージャであるNixはNix言語という純粋関数型言語で設定を記述するのですが、それがなぜなのかをビルドの仕組みなどから解説していくセッションです。
Nixは少ししか触れていませんでしたが、こうしてビルドの仕組みを聞いているとかなりの浪漫を力技で実現しているすごい技術だと改めて感じます。とはいえTwitterの反応でも容量問題は結構注目されていたり、まだまだ盛り上がりそうだなと感じました。
暗号実装における辛さを関数型によって解決してみよう
(登壇資料はのちほど上がるようです)
暗号実装の脆弱性を関数型アプローチでどのように解決できるかという話です。
暗号実装は触れたことはなかったですが、内容としてはやはり入力・出力のとりうる値をどう型に表現するか、計算のとりうる作用をどうやってシグネチャに起こすのか、という話だったので分かりやすかったです。
アルゴリズムは何を圧縮しているのか: Haskell から育った「圧縮代数」というメンタルモデル
競技プログラミングで典型となっている問題の実装を手続き的・操作的な視点ではなく、意味的な視点で捉えなおすことで、アルゴリズムが何を実現するためにどういった情報を保ちながら効率的なパフォーマンスを出す演算を行うのかというのを具体例とともに解説するセッションです。
ある種のパラダイムシフト的な印象を自分はこのセッションに感じていて、このセッションにおける「圧縮」は空間を一定の方向につぶしてより小さな別の空間で答えを導くことで、つぶした分元の空間における煩雑だった部分の苦しみから脱却できるという解釈をしているのですが、そのために意味論としてとらえなおしてみようという切り口が、すごく刺さったと思います。
聞いた発表の多くに共通していたのは、自分の登壇も一部そうですが、実装に入った暗黙な操作を型として表現することをコンセプトにしていたと感じました。
プログラムのコードの動作を分かりやすくするためには、暗黙な操作をつぶしていくことに着目するのが効率のいい戦略であり、そのために関数を軸に考える関数型パラダイムはそうした戦略をかなえやすいのかもしれません。
Blogを書くまでがカンファレンス
今回なんと関数型まつりの参加ブログを書くと抽選で次回の関数型まつりの割引クーポンがもらえるそうです。自分はBlogを書くまでがカンファレンスだと思っているので、もしこれを見ている方でまだ書いていないかたは是非書いてみてください。トーク聞いたけどわからなかった単語集とかでも多分対象になれます(要検証)。インプットしたらアウトプットすると定着しやすいと古事記にも書かれています()