Haskell Symposium 2019 レポート

Posted by Kazuki Okamoto (@kakkun61) on October 1, 2019Tags: ICFP, Haskell Symposium

Haskell Symposium 2019IIJとして参加してきました。

聴講した発表についての概要をまとめましたので、どの論文を読んでみるか決めるなどの際にご活用ください。内容については私の聞きまちがい・読みまちがいなどあると思いますのでご了承ください。

Link to
here
Haskell Symposiumとは

International Conference on Functional ProgrammingICFP)に合わせて開催されるHaskellに関する国際会議です。Haskellに関する研究を発表したり、実践的な経験や将来の言語の開発について議論したり、その他の宣言的プログラミングを促進したりします。

Link to
here
Bidirectional Type Class Instances

GADTと型クラスはそれぞれ便利だが混ぜると問題が起きる場合がある。

次のようなTermがあるとき、そのShowインスタンスを考える。

次のようにShowインスタンスを定義すると型エラーになる。

Could not deduce (Show b) arising from a use of `show'
from the context (Show a) or from (a ~ (b, c))

これはShow (b, c)ならばShow bという関係がないために起こる。

一方タプルについてのShowは、Show aかつShow bならばShow (a, b)という関係である。

この「ならば」を両方向にすれば問題は解決できるのではないかというのが、この論文の主張である。

Link to
here
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances

型クラスの法則は依存型を使えば証明できるが、インスタンスごとに書くのはめんどうなのでGenericsで出来るようにしようという話である。

Link to
here
Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study

様々な種類の効果が複雑に絡み合うアプリケーションを整理するために、「効果を伴う処理を持った辞書」を明示的に渡す方式の提案である。

提案した方式によってVeriFastを再実装してみることで、実際に発生した問題と解決方法を解説している。

Link to
here
Verifying Effectful Haskell Programs in Coq

Coqによる、効果を伴うプログラムの証明に関する話。

効果について直接証明することはせず、Freeモナドを用いての証明を試みても、そのままCoqに翻訳すると停止性チェックによってエラーになってしまう。

そのために行った工夫に加え、具体例として、traceや(部分関数による)エラーなど、Haskellにおいて暗黙に発生する効果を考慮したモデル化について検討した。

Link to
here
Solving Haskell equality constraints using Coq

data kindstype familiesといったGHC拡張によって厳格なデータ型を定義できるが、それに対する操作を定義するとGHCには解けない型レベルの等式が生成されることがある。

制約カインドの型に対する型クラスとしてProvenを提供し、この制約がある箇所をGHC型検査プラグインが検出して対応するCoqコードのテンプレートを生成する。

そのCoqコードに証明がなければ警告を表示する。

いくつか制約があるがHaskellの型をCoqに自動的に変換している。

Link to
here
Formal Verification of Spacecraft Control Programs: An Experience Report

REDFINという固定小数演算と整数演算のための処理系があるのだが、そのアセンブリーコードに対して形式検証をしたという報告である。

Link to
here
G2Q: Haskell Constraint Solving

G2QHaskellのソースにquasi quoteで埋め込むDSLである。

Haskellで書いた条件式をsymbolic executionして、SMT solverに渡す式に変換して、SMT solverに条件を満たす関数を導出させる。

Link to
here
Making a Faster Curry with Extensional Types

パフォーマンスのためにη変換してほしいところを明示したいことがある。

例えば、次のような意味論上は等価な関数f1f2があるとする。

実際はf1は引数xを取った後クロージャー生成のためにヒープ確保するのに対して、f2はアリティが2の関数と解釈されて中間のクロージャーが必要なくなる。

~>というアリティの情報を持った関数型を新たに導入して->の代わりに使えるようにする。

TYPE (a :: RuntimeRep (FunRep 2))というような新たなポリモーフィズムを導入する。ここでの2がアリティ。

Intに対してInt#があるように基本的にはパフォーマンスが必要なライブラリーなど内部的に使用する想定。

Link to
here
Multi-Stage Programs in Context

次のような準引用があったときに、組み合わせると元々あったはずの情報が欠落する場合がある。

qshowqreadにあったIntという情報が、組み合わせてtrimとすると欠落してコンパイルエラーになってしまう。

spliceするときにHaskellソースコードの構文木ではなくCoreに対するものを出力すればそれは型が明示されているし問題がない。

しかも、splice後の型検査を省略できるのでコンパイルの高速化にも寄与する。

Link to
here
Working with Source Plugins

souce pluginsのしくみや、書き方、実装時のテクニックの紹介である。

Link to
here
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism

同じ時刻のHIWの発表を聴講していたためこちらは聴講していません。

Link to
here
Synthesizing Functional Reactive Programs

同じ時刻のHIWの発表を聴講していたためこちらは聴講していません。

Link to
here
The essence of live coding: Change the program, keep the state!

同じ時刻のHIWの発表を聴講していたためこちらは聴講していません。

Link to
here
Monad Transformers and Modular Algebraic Effects: What Binds Them Together

モナドトランスフォーマーと代数的効果との対比である。

モナドトランスフォーマーから代数的効果への変換またその逆のときにどういう手法があって、それぞれを構成する要素がどう対応しているかを説明している。

モナドトランスフォーマーと代数的効果だとモナドトランスフォーマーの方が表現できるものが大きいのでモナドトランスフォーマーから代数的効果へはどんなものでも変換できるわけではない。

例えばcatchlocalは代数的効果にできない。

Link to
here
Scoping Monadic Relational Database Queries

モナドはHaskell界隈で非常に普及しているのでSQLに対するEDSLとしてモナドの構造を採用したい。

このときSQLの結合を表現すると、SQLとしてはスコープ外にもかかわらずEDSLとしてはスコープ内となって使える変数ができてしまう。

これをEDSLとしてもエラーとしたい。

例えば、次のような例で実行時エラーとなってしまう。ここでa0tableAの列とする。

SELECT b0 FROM tableB WHERE a0 == b1の部分でスコープ外のa0を参照しているためエラーとなる。

単純なモナドEDSLだと次のようになりコンパイルが通る。

ristrict $ a0 .== b1の部分においてa0Haskellとしてはスコープ内にある。

この問題を次のような型レベル関数を駆使することでEDSLにおいてもコンパイル時エラーとすることができた。