Haskell Symposium 2019 レポート

Posted by Kazuki Okamoto (@kakkun61) on October 1, 2019Tags: ICFP, Haskell Symposium
投稿したい方はこちら

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

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

Link to
hereHaskell Symposiumとは

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

Link to
hereBidirectional Type Class Instances

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

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

data Term :: Type -> Type where
  Con :: a -> Term a
  Tup :: Term b -> Term c -> Term (b, c)

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

instance Show a => Show (Term a) where
  show (Con a) = show a
  show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
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)という関係である。

instance (Show a, Show b) => Show (a, b) where
  …

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

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

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

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

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

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

Link to
hereVerifying Effectful Haskell Programs in Coq

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

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

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

Link to
hereSolving Haskell equality constraints using Coq

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

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

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

type ProofName = Symbol

class c => Proven (prf :: ProofName) (c :: Constraint)
  where {}

applyProof :: forall prf c a. Proven prf c => (c => a) -> a
applyProof x = x

lemma3 = applyProof @"nonzero_pop" @(NNonZero (Popcount b) ~ True) Refl

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

Link to
hereFormal Verification of Spacecraft Control Programs: An Experience Report

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

Link to
hereG2Q: Haskell Constraint Solving

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

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

Link to
hereMaking a Faster Curry with Extensional Types

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

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

f1 = \x -> let z = h x x in \y -> e y z
f2 = \x -> \y -> let z = h x x in e y z

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

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

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

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

Link to
hereMulti-Stage Programs in Context

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

qshow :: Code (Int -> String)
qshow = [q| show |]

qread :: Code (String -> Int)
qread = [q| read |]

trim :: Code (String -> String)
trim = [q| $(qshow) . $(qread) |]

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

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

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

Link to
hereWorking with Source Plugins

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

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

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

Link to
hereSynthesizing Functional Reactive Programs

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

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

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

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

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

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

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

例えばcatchやlocalは代数的効果にできない。

Link to
hereScoping Monadic Relational Database Queries

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

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

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

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

SELECT a0, b0
FROM
  tableA
    LEFT JOIN
      (SELECT b0 FROM tableB WHERE a0 == b1)
  ON tableA.a2 == tableb.b2

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

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

do
  a0 :*: a1 :*: a2 <- from table0
  leftJoin $ do
    b0 :*: b1 :*: b2 <- from table1
    ristrict $ a0 .== b1
  on $ a2 .== b2

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

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

type family Cols a
type family Outer a
type family UnAggr a
type family FromRow a
HIW 2019で発表された、Copilotという内部DSLについて
トップに戻る
HIW 2019で発表された、Gibbonコンパイラーについて