Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何

スマートコン @mr_konn

Haskell における依存型プログラミングでは、大抵の場合安全性の"証明"として依存型を用いる場合が多いから、ひとたび証明が出来てしまえば、その証明に対応する実行時計算は無駄なんだよなあ。type erasure ならぬ proof erasure が出来ればよいのだが

スマートコン @mr_konn

帰納法は O(n) 書かるし、二重帰納法なら O(n^2) だ。一回示せたら unsafeCoerce すりゃいいかもしれないけど、そういうのを自動的にやってくれるのを欲しい

スマートコン @mr_konn

"proof erasure" で検索するとだいぶ引っ掛かるな

スマートコン @mr_konn

Attributive Types というらしい。やはり既に考えているひとがいるのか

スマートコン @mr_konn

むしろ、(a :=: b) → f a -> f b でその実体最終的に書き換え規則で unsafeCoerce に置き換えるのがよい気がする

スマートコン @mr_konn

証明それじたいを unsafeCoerce するのではなく、型レベルで保証された unsafeCoerce

スマートコン @mr_konn

これならいけるか？

スマートコン @mr_konn

最近は強制法を応用して型システムを拡張しようなんていう話まであるというではないですか。

スマートコン @mr_konn

a :=: b がわかってるなら f a -> f b をするのは簡単だけれど、型制約があって……という場合が面倒だな

スマートコン @mr_konn

取り敢えず :=: と RULE を使った coercion による実装と、旧来の実装とでベンチとってみるか

スマートコン @mr_konn

[type-natural] https://t.co/yY3Jx3QRPh Hiromi Ishii - Rewrriten with ekmett's `constraints' package.

スマートコン @mr_konn

[equational-reasoning-in-haskell] https://t.co/EArwmiFTTo Hiromi Ishii - Added coercion function with proof erasure using RULES pragma

スマートコン @mr_konn

今気付いたけど、 RULES プラグマじゃなくて INLINE でやるべきだな…

スマートコン @mr_konn

[equational-reasoning-in-haskell] https://t.co/sWH9YgVzWv Hiromi Ishii - changed to use INLINE pragma

スマートコン @mr_konn

[equational-reasoning-in-haskell] https://t.co/VO0f4hyT57 Hiromi Ishii - version bumped

スマートコン @mr_konn

[type-natural] https://t.co/yY3Jx3QRPh Hiromi Ishii - Rewrriten with ekmett's `constraints' package.

スマートコン @mr_konn

[sized-vector] https://t.co/Jo71b4kK8S Hiromi Ishii - added bench

スマートコン @mr_konn

[sized-vector] https://t.co/2RVNLPjPfQ Hiromi Ishii - added benchmarks result

スマートコン @mr_konn

[sized-vector] https://t.co/wAvtjrCNlS Hiromi Ishii - version bumped

スマートコン @mr_konn

えっ……この時点でこんなに時間食うの……

スマートコン @mr_konn

ここ変えたところでショージキ余りオーバーヘッド変わらん気がするし、一々ベンチ取るまでもない気がしてきたなあ

スマートコン @mr_konn

ねむい

スマートコン @mr_konn

一通り書き直したぞ

スマートコン @mr_konn

これでうまくいくと思うんだがなあ

スマートコン @mr_konn

そしてどうせこの実装は正当な筈なので、これもなんか RULES じゃなくて INLINE でやったほうがよさげ