Haskell における依存型プログラミングと証明の記述を用いた実用的なプログラミングって何
スマートコン @mr_konn Haskell における依存型プログラミングでは、大抵の場合安全性の"証明"として依存型を用いる場合が多いから、ひとたび証明が出来てしまえば、その証明に対応する実行時計算は無駄なんだよなあ。type erasure ならぬ proof erasure が出来ればよいのだが 2014-02-23 17:10:29 スマートコン @mr_konn 帰納法は O(n) 書かるし、二重帰納法なら O(n^2) だ。一回示せたら unsafeCoerce すりゃいいかもしれないけど、そういうのを自動的にやってくれるのを欲しい 2014-02-23 17:12:45
HaskellとOCamlの型の違い
Hideyuki Tanaka @tanakh 完全な型推論よりも、型システムの表現力が重要である、という考えは多分OCamlとは相容れない。そこがOCamlとHaskellの決定的な差であって、PureとかLazyとかの違いはそれに比べれば割りとどうでもいい。 2012-03-26 14:24:35 Jun Furuse 🐫🌴 @camloeba RT @tanakh 完全な型推論よりも、型システムの表現力が重要である、という考えは多分OCamlとは相容れない。そこがOCamlとHaskellの決定的な差であって、PureとかLazyとかの違いはそれに比べれば割りとどうでもいい。 2012-03-26 14:36:35
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
