HIW 2018・Haskell Symposium 2018に行ってきた
2018年10月16日 火曜日
CONTENTS
HIW 2018・Haskell Symposium 2018 とは
HIW 2018 (Haskell Implementors’ Workshop 2018)とHaskell Symposium 2018は、ICFP (International Conference on Functional Programming)という関数型プログラミングについての国際会議に併設された、Haskell専門のワークショップと国際会議です。
Haskell Symposiumは投稿されたHaskell全般についての論文の発表会です。
一方HIWは、名前通りのHaskellの実装（主にGHC）にフォーカスを当てた「Haskellの処理系の開発状況報告会」だけでなく、割と緩いテーマのLT (Lightning Talk)コーナーがあったり、GHCの今後の開発について自由に議論する時間があったりと、バラエティーに富んだ会でした。
今回はそれらで行われた発表のうち、特に印象に残ったものを紹介したいと思います。
残念ながら、会場に向かう途中乗り継ぎの飛行機がキャンセルされるというトラブルで遅刻したり、時差ぼけに勝てなかったりそもそも私のリスニングスキルが足りなかったといったこともあり、聞き逃してしまった発表も多くありますので、そのあたりは特に論文を詳しく見直しながら書きます。
いずれにしても詳しい内容は、HIWについてはこちらと、Haskell Symposiumについてはこちらをご覧ください。
Haskellに詳しくなければ難しい内容が多いですが、一から説明するとそれだけで記事がいくつも書けてしまうような話題が大半なので、あらかじめご了承ください。
hask(_ _)eller
HIW 2018 での発表
Invited Talk: Let’s Go Mainstream with Eta!
JVM向けHaskell実装で、GHCのフォークある「Eta」について。
去年個人的に少し触ったことがあったのですが、その時からまたいろいろ進化しているようです。
これまでに知らなかったEtaの特徴のうち、印象的なものは以下の通り。
- 型エラー時のエラーメッセージをよりわかりやすくした。
- AnonymousRecordsやRowTypePolymorphismといった、GHCにはない、独自の言語拡張を追加しようととしている点。
単純にGHCをJVM向けに移植したものとして、GHC本体に追従するのではなく、固有の機能をたくさん追加しているみたいですね。
互換性のことを考えると個人的にはちょっと残念な気もしますが、スライドのタイトルの通り「メインストリームにしたい！」という思いを考えると当然なのかもしれません。
ちなみに、探してみたところ発表の書き起こしとおぼしき記事がありました。ありがたや。
HIW’18: Let’s Go Mainstream with Eta! : Inside 245-5D
また、Etaについての日本語の情報はこちらのスライドもどうぞ。
Haskell + Scala ハイブリッド開発大作戦 #ScalaMatsuri / Operation Haskell + Scala – Speaker Deck
文字通りGHCの最近の更新、とりわけ2017年7月にリリースされたGHC 8.2以降の更新について。
GHC 8.2以降、最新版のリリース頻度が上がって半年に一度になり、ちょっと追うのをサボり気味でしたので、ありがたいまとめでした。
毎バージョンのように追加される新しい言語拡張が目を引く一方、昨今と今後のバージョンではコンパイル速度に特に重きを置いているようです。
GHC 8.6のスライドとGHC 8.8のスライド両方で「Performance, performance, performance (esp. compile times)」と書いているのが印象的でした。
特にスライドでは言及してませんが、GHC 8.2でもコンパイル速度の改善はありましたし、GHC 8.4のスライドにも「Perf improvements in large projects」とあることからして、GHC開発者自身もコンパイル速度には頭を悩ませているのでしょう。
GHCのソースプラグインの紹介。
GHCのソースプラグインとは、GHCのパーサーや型チェッカーをHaskellのコードで拡張できる機能です。
型チェック時にソースコードを独自に解析したり、まだ実装されていない言語拡張を実験したり、様々なことができます。
Generalized Abstract GHC.Generics
GHCの「Datatype-generic programming」という機能に欠かせないGenericという型クラスは、データ型の構造を表すメタデータ（どんな値コンストラクターがあってどんなフィールドを持っているのか）を専用の型を組み合わせて表現するようインスタンスを定義することで、任意のデータ型に対する処理を簡単に書けるようにしてくれます（詳しくはこの発表のスライドでも触れられています）。
そんなGenericですが、従来よりGADTsというGHCの言語拡張を用いて定義されたデータ型については、インスタンスを定義できません。
それを解決するためのあれこれの提案です。
Haskell Symposium 2018で発表される論文でもある、Generic Programming of All Kindsの成果も用いられているようです。
GHCの、内部で使用している中間言語から表層言語まですべてに「依存型」という機能を加える「Dependent Haskell」という取り組みの一環です。
「Dependent Haskell」がGHCで実現されると、今までバラバラに存在していた各種の型レベルプログラミング関係の言語拡張をすっきりとさせたり、値レベルのプログラミング（要するに通常プログラムを書くときに行う普通のプログラミング）でのテクニックを再利用しやすくなります。
この発表では、「Dependent Haskell」を実現するに当たり肝要な、「homogeneous equality」、つまり同じカインドの型の等価性、という性質をどのようにして実装するのか、という問題を論じています。
GHCにlinear type, すなわち「線形型」という機能をどうやって追加するのか、その実装方法の詳細について。
Asterius: Bringing Haskell to WebAssembly
Asteriusという、HaskellをWebAssemblyにコンパイルするコンパイラーの紹介。
Clash: a practical Haskell to circuit compiler
HaskellのサブセットをVHDLやVerilogに変換する処理系、Clashの紹介。
門外漢なんで詳しくはわからないのですが、Haskellでハードウェアのデジタル回路を記述できるようにしてくれるそうです。
Haskell Symposium 2018 での発表
Neither Web nor Assembly (Invited Talk)
WebAssemblyのこれまでとこれからについての発表です。
話題がいろいろあったので断片的なメモを共有します。
- タイトルの通りWebAssemblyはWeb（つまりブラウザ）だけのものではなく様々なプラットフォームで動かしうるものであるし、仮想マシン向けの抽象化された命令セットなので、Assemblyでもない。
- セマンティクスはIsabellなどの定理証明器によって証明されている。
- これまでは低レイヤーなプログラミング言語のための機能を定義してきたが、今後はより高レイヤーなプログラミング言語向けの機能を定義していくつもり。
- pthreadを模したマルチスレッド機能とか
- ガーベジコレクションとか
- フィードバック求む！今の議論はC++な人たちに偏りがちなので！
AutoBench: Comparing the Time Performance of Haskell Programs
QuickCheckによる入力データの自動生成と、Criterionというベンチマーク用のライブラリーを組み合わせて、ベンチマークを簡単に実行するライブラリーを作った、という話です。
二つの関数に同じ入力を与えて、実際に片方の関数がもう片方の関数と同じ振る舞いをして、なおかつもう片方の関数よりも有意に速い関数かといったことも自動で調べてくれます。便利！
加えて、関数の実行速度を回帰分析することで、「この関数は入力サイズNに対してlog(N2)の実行時間がかかる」といった、計算量の推定まで自動で行ってくれます。さらに便利！
Ghosts of Departed Proofs (Functional Pearl)
関数の引数が守るべき事前条件をいかにして守らせるか、また、守られなかったときにいかにして型エラーにするか、という話。
以下のように、「幽霊型（Phantom type。型パラメーターには表れるけど、実際の値には現れない型のこと）」という機能を使用したテクニックです。
- 関数の戻り値が満たしている条件（事後条件）を、幽霊型として関数の戻り値にくっつけることで、関数の型宣言で事後条件を表明する。
- 「例えば、この関数の戻り値は第1引数に渡した関数でソート済みである」と言った条件を、型に付与することで、型宣言で明示します。
- 引数が事前条件を満たす必要がある関数は、引数の型に、幽霊型として明示された条件をくっつけます。
- 「例えば、この関数の引数はソート済みである必要がある」と言った条件を、同様に型に付与します。
- 結果、事前条件を表す幽霊型を付与した引数は、「事後条件を守ることで指定した幽霊型を付与された引数」しか受け取らなくなります。
実際にこの発表で提案されたテクニックは、gdp（文字通り「Ghosts Departed Proofs」の略）というパッケージで使うことができます。
コード例がないのでわかりづらいという方は論文と併せて読んでみてください！
Generic Programming of All Kinds
前述のGeneralized Abstract GHC.Genericsでも言及した、「Datatype-generic programming」機能を改善するための提案です。
従来のGHC.Genericsの機能では表現できない型の例（と、それをいかに表現できるよう拡張するか）が、より詳細に述べられています。
Suggesting Valid Hole Fits for Typed-Holes (Experience Report)
「Typed-Holes」という機能を、より親切な機能に拡張しようという提案です。
従来「Typed-Holes」では例えば map (length . _someFunc) [True, False, True] などと書いた場合Found hole: _someFunc :: Bool -> [a0]というように、「_someFuncの型は Bool -> [a0]（Boolを受け取って何かのリストを返す関数）だよ」と教えてくれます。
このように、ソースコードの中にアンダースコア _ で始まる名前（識別子）を書いておくと、その名前の式がどんな型であるべきなのか、推測して教えてくれる機能です。
今回の提案では、型を推測してくれるだけでなく、実際に推測した型にマッチする関数を列挙してくれる、という機能が紹介されました。
単純に型が完全にマッチする関数だけでなく、「引数をさらに追加すればマッチする」関数も教えてくれるそうです。
論文では具体的にどのようなケースでどんな風に役に立つか、様々な例が列挙されています。
Branching Processes for QuickCheck Generators
QuickCheckによる入力データの自動生成は、型情報に応じたテストデータをランダムに自動で生成してくれるので便利なものです。
しかし、木構造のような、再帰的なデータ型に対しては、ちょっと工夫が要ります。
愚直に実装すると無限再帰呼び出しになってしまってすぐにスタックがあふれてしまうし、無限再帰呼び出しを避けるために再帰する回数を制限しても、生成されるデータは再帰しない値コンストラクター（木構造で言うところの葉に相当するもの）に偏ってしまいます。
今回提案された方法は、そうした従来の方法における、生成されるデータの偏りを防ぐために、各値コンストラクターをどのような確率で生成すれば、各値コンストラクターが最終的にどのような比率で生成されるのか、定式化しています。
実際に生成したテストデータで、bashのパーサーのテストを行ってみると、従来よりも遙かに高いテストカバレッジを得られたそうです。
この論文の通り実装されたライブラリーはこちらのリポジトリーで利用できるみたいです。
個人的にも使ってみたいので早くhackageに公開していただきたいですね！
Coherent Explicit Dictionary Application for Haskell
長年いくつもの案が提案されては却下されてきた、「型クラスのインスタンスの動的な定義」についての提案です。
従来の案が却下される原因となった、「自由に型クラスのインスタンスが定義できてしまうと、『同じ型に対する同じ関数は常に同じように振る舞う』という原則に依存した処理が正しく動かなくなってしまう」という問題に真正面から取り組み、具体的に「どういう状況ならばインスタンスの動的な定義を認めて良いか」を詳細に考察しています。
実装のプロトタイプがこちらにあります。
ただ、個人的には新しく提案された構文がなんだかイマイチで、もっとこなれたものにならないかと感じたので、過去の提案を顧みつつ、よりよい仕様になることを願っています。
Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl)
Liquid Haskellという、SMTソルバーを使って「Refinement Types（篩型）」を実現する型チェッカーです。
Liquid HaskellについてはLiquid Haskell のインストールと学習方法をご覧ください。
この論文では、このLiquid Haskellの力を利用して「Equational reasoning（等式推論）」の正しさを自動でチェックすることで、定理証明に応用する方法を紹介しています。
こちらのページで実際に論文を読みながら体験できるようになっています。
ちなみに、こうした等式推論によるソフトウェアによる定理証明は、CoqやAgdaなどといった言語が、従来より強くサポートしています。
興味を持った方はプログラミング Coqや、Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証するをご覧ください。
所感
以上、HIW 2018およびHaskell Symposium 2018で発表された内容について、手短に紹介いたしました。
具体例など詳しい説明を省いたのでわかりづらい点が多かったかもしれませんが、何かしら新しい興味を持つきっかけになっていれば幸いです。
個人的な感想としては、もっと有意義な交流なり議論なりがしたかった、という後悔が一番大きいです。
これまでの反省を生かし、事前に投稿された論文を一部とは言え読み込んでおけたからか、比較的内容をよく理解できたようには感じます。
ただ、単に内容を知るだけなら、わざわざ現地に足を運ばなくとも事前や事後に公開される論文やスライドを読めば十分可能です（現に私は自分が参加していなかった発表についても論文やスライドを見直してここで紹介できていますし）。わざわざ高い飛行機代や参加費を出して行って得られる成果としては、あまりにも小さなものだと思います。
論文や発表の内容自体はインターネットでスライドやPDFをダウンロードすれば読めるのに、なぜそれでも多くの人が参加するのかと言えば、それは直接会って話ができるからです。
HIWやHaskell Symposium 2018には、Simon Peyton JonesさんをはじめとするGHCの開発に関わる著名なHaskellerのほか、世界中から熱心なHaskellerが出席されます。
こうした機会はそうそう多くありません。
にも関わらず、私は英語力の不足もあり、発表を聞いても質問も思いつかず、実のある話を日本人以外とできませんでした（一緒にいた日本人の友人とはそれなりに議論できましたが）。
こうした失敗は、これまでも何度もありました。
私は今回を含め、このような海外のカンファレンスに3回参加しましたが、いずれでも似たような後悔をしていました（発表がより多く聞き取れるようになったはずなのでその点は成長かな！）。
3回目にして、加えて会社のお金で参加するというある種のプレッシャーを抱えてようやく気づきましたが、こうした問題を乗り越えるには、やっぱり話しかける目的を自分から用意すべきでした。
特に情熱を傾けられる動機を用意できれば、伝えようという思いが強まり、英語も積極的に使うきっかけとなったことでしょう。
HIWで開催された、LTで発表する理由にもなりえます。
具体的には、私の場合、来年、あるいはその後でも機会があれば、自分が今個人的に作っているHaskellの教育用コンテンツの完成度の高いものにして、宣伝したいです。
Haskell Day 2018の初心者向けハンズオンで使用する予定であるにもかかわらず、現状あまりできていません。
しかしこれを十分に自信を持てる仕上がりにすれば、よい名刺代わりになるはずです。
もっと頑張ろう。
みなさんも、カンファレンスに参加する際は、特に宣伝したいものとかでなくとも、何か話したい話題をあらかじめ決めておくといいかもしれません。
