haskell-jp / icfp #1

@kakkun61 has joined the channel
@kakkun61 set the channel purpose: ICFP およびその併設催事について
@egisatoshi has joined the channel
自分は22日・23日と参加します
Haskell Symposium と Haskell Implementers' Workshop に
前乗りして20日夕方からベルリンいます
@igrep has joined the channel
@lotz has joined the channel
(行かないけど興味本位で覗きに来ました :eyes: )
set up a reminder “@igrep Add this channel to slack-log” in this channel at 9AM Monday, August 26th, Japan Standard Time.
@y_taka_23 has joined the channel
自分も行かないけどちょっと興味あるので。
@notogawa has joined the channel
@1to100pen has joined the channel
@ywataywatay has joined the channel
@msakai has joined the channel
ホテル着きました:hotel::de:
今年も安定の Unagi
ホテルのアメニティで歯ブラシとひげ剃りあるだろうと思ったらないみたい
@matsubara0507 has joined the channel
@fumieval has joined the channel
Haskell Symposium 2019 1日目2つめ。
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances
型クラスのlawは依存型を使えば証明できるけど、インスタンスごとに書くのはめんどうなのでGenericsで出来るようにしようという話
Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study
いろんな種類のEffectを扱う大きめのアプリケーションを実際にどう設計したか、みたいな話
with系の関数に異なるMonadのアクションを渡す場合の扱い方についても検討してる
私と同じでExplicit Dictionary Applications推しなのが好感持てる
午後のセッション1つめ
Verifying Effectful Haskell Programs in Coq
Free を使ったEffectの定理証明を試みるも、そのままでは停止性チェックに引っかかってしまうため、
class Container c where
    type Shape c :: Type
    type Pos c   :: Shape c -> Type

-- Concrete instance of a container
data Ext c a = Ext (s :: Shape c) (Pos c s -> a)

data Free c a = Pure a | Impure (Ext c (Free c a))

みたいな型を作ってどうにかする話らしい(どうしてこれでどうにかなるのかわからん
Writer みたいなMonadについてどうするか、って話もあったけど理解できず
最終的なゴールはimpureな遅延評価の挙動をモデル化(して証明)する、ところにあるのかな?
だからtraceやbottomについて検討してるっぽい
Solving Haskell equality constraints using Coq

Haskellで難しい証明はCoqでやろう => Coqで証明したlemmaをHaskellで利用できるようにするType Checker Pluginを作った
発表者、vimでCoq使ってる!
型と型レベル関数もちゃんと Coq に変換してくれるらしい
GADTs は 型族で置き換えられるの
Formal Verification of Spacecraft Control Programs: An Experience Report
REDFIN 固定小数演算と整数演算のために制限されて命令(の処理系)に対して
次の発表グループ「Paper Session 3: SMT & Arity」あんまり関係なさそうなのがまとめられててウケる
G2Q: Haskell Constraint Solving

HaskellのソースにQuasiQuoteで埋め込むDSL。Haskellで書いた条件式をsymbolic executionして、SMT solverに渡す式に変換して、SMT solverに条件を満たす関数を導出させる
前の方に座ってるとSimonに指されるリスクがあるのちょっと怖い :sweat_smile:
Making a Faster Curry with Extensional Types

「~>」という、arityの情報を型レベルで含んでいる関数を新しく作って、arityを(パフォーマンスを気にする)プログラマーが明示できるようにする
TYPE (a :: RuntimeRep (FunRep 2)) というような新たなポリモーフィズムが
η 変換してほしいところを明示したいという動機らしい
eta-expansionしてほしくないケースは割と想像つくし、実際に --fno-do-lambda-eta-expansion してるコードを見たことがあるんだけど、積極的にしたいケースってどんなだろう。
関数ににおける Int# みたいなのが出来るイメージっぽい?
論文もうちょっと読もう。
Multi-Stage Programs in Context

型付きのTemplate Haskell( TExp )において、splice時に型引数がどう具体化されたか(Context)をどうやって保存するか、という話。
直接Coreを吐いてしまえば、Coreはexplicitly typedだし解決できるんじゃない?
しかもspliceが多いmoduleはもっと速くコンパイルできるし、(splice前後のHaskellのソースに対する)型チェックを二重にする必要もなくなるよ!
2つ続けて同じ発表者となったことについてのいじりが:sweat_smile:
:man-raising-hand: 「前の発表者について質問なんだけど...」
そもそもそこでやらないと Template Haskell の展開でループができちゃうらしい