ジョットク発表 2020
『Haskell 言語拡張における型推論の再実装』
発表8分、質疑応答2分
多分その場にいる全員におれが何をやったかが伝わればいいのかな
どういう問題があって、それをどういうふうに解いたか
何をやったの?
Haskell の言語拡張に GADTs と TypeFamilies というのがある
そいつらの型推論パートを OutsideIn(X) の論文に沿って実装した
実装した結果、理解が深まっただけでなく論文の怪しい部分を見つけたりした
TODO: どこ?
説明しなければいけない前提知識
Haskell?
GADTs と TypeFamilies が何をする拡張なのか
OutsideIn(X) がなんなのか
HM(X) がなんでどう違うのか
HM が...
型推論が...
そのほか言いたいこと
動機的な?
宣伝したいところ
おもろい例
nat_add_props みたいなのは是非に出したい
Hasochismを読んだ上で先生に相談がいるね…
やフツーに typed interpreter でいい感ある
これからのはなし
Implement X with CHR?
↑コレで具体的に何を達成したいのか?
TODO: 何?
型クラス機能の拡張をザクザクやりたい
U: Into<T> => U: Into<Option<T>>
そもそも現行のソルバが何も良い性質がわかっていないからそこもなんとかしたい
Haskell (GHC)になるには何が足りないの?
Evidence generation
Optimized implementation?
Ad-hoc rules around floating...
TODO: GHC読んで喋れるようにしておく
デモ?
おもろいか?
考えた方がいいこと
どこまで前提知識を掘るのか
つまづきポイントについて詳しく話すべきか...
細かすぎて伝わらないあるあるシリーズ
アウトライン
前提知識 2m
Haskell とは
GADTs TypeFamilies の説明
それぞれ例
emulation of dependent type
Vec, Matrix
読んでおいた方がよさそう
Hasochism: the pleasure and pain of dependently typed haskell programming
こっちのアドはある?
lightweightと拡張性の両立
都合がいい
type-level language はすでに良い性質を持っていることが期待される
やったことの説明 5m
それらの型推論・型チェックパート
制約生成→制約解消
GADTs がいると local assumption のせいで型制約に implication がつくよ
特に考えずにimplicationつきの制約を解こうと、しかし主要型が…
→GHCで採用されている、保守的でアドホックだが実装が簡単なアプローチ: OutsideIn(X)
読んでおいた方がよさそう
Simple unification-based type inference for GADTs
Guarded recursive datatype constructors
TypeFamilies がいると non-syntactic な型の同等性の制約をとくことになるよ
特に考えずに...→?(どんな悪いことが...)
論文から; a ~ F a とか
(ここら辺やっただけだからもうちょっと調べた方がよさそう)
読んでおいた方がよさそう
Type Checking with Open Type Functions
実装した結果、理解が深まっただけでなく論文の怪しい部分を見つけたりした
何?
これから 1m
CHR
evidence