#なんかリファクタリングの際に型しかみなくなってきた・・・
#型とロジックって一対一に対応しやすいな。もちろん全部とは言わないけど、「fstやsndがそれしかない」みたいなのがなんか分かるような気がしてきた。
#こういうのって型を書いた瞬間に標準実装が生成できたりしないものだろうか。
#誰か研究しててもよさそうだけど。
#つか標準実装を書かなくても自動導出とかな。
#なんか面白そうだけど。
#型だけでは情報が足りない気が。a -> a -> a の標準実装って? とか。
#というか、型を与えられてそれを満たす実装を見つけるっていうのは、命題を与えられて証明を示すのと同値ではありませんか。つまり自動導出が出来るなら自動証明が出来ることに。
#つAgda 完全自動とはいかないまでも，証明支援をするシステム．
#簡単な型だけならdjinnというのもあります。カリー・ハワード対応の話は知ってはいたものの実感としては薄かったのですが、#coqtのおかげでようやく身についたという感じがします。
#Djinn> f ? a -> a
f :: a -> a
f a = a
Djinn> f ? a -> a -> a
f :: a -> a -> a
f _ a = a
#darcsで取ってきてちょろっと弄ると動くようです。
#かっこいい。djinnだから3回しか使えない、なんてことはないですよね。
#逆に、どういう時に自動生成できないんでしょう。
#Djinnは昔試したことがあります。 http://t.co/kQjVoVx #直観主義命題論理の決定可能性を利用しているはずので、自動生成できるのは基本的には、型変数と関数型と再帰的でない代数的データ型だけからなる型のときのはず。その範囲でも何故か自動生成できなかったりもしたけど。
#そいうばこの前、日比野さんと話してホーア検証は型づけと一緒といわれた ですぞ。[アルゴリズム勉強会 http://bit.ly/iNwJdw ] #具体的な型ではなく、型変数だからこの引数しかないってのはありそうだな。
#同じ型変数を使われるとまた区別がつかなくなるから困るけど。
#f :: a->a->aとかはf _ a = aもありだけど f a _ = aもありなわけで。
#なんでf _ a = aを導出したのかは良く分からんが。
#f :: a -> b -> aなら f a _ = aってのがデフォルト実装（自動導出）でよさげ。
#まぁfstだな。
#curry fst。
#型に対してプログラムがユニークってFree Theorem? ですぞ。[アルゴリズム勉強会 http://bit.ly/iNwJdw ] #「Theorems for free」か、これって確かmr_konnさんが読んだっていってた気が… ですぞ。[アルゴリズム勉強会 http://bit.ly/iNwJdw ] #これってパラメトリシティとかいう話でしょうか。キーワードだけ聞いたことありますが情報が見つからなくて実際どういうものなのかさっぱり理解してないです。 Theorems for free ってのを読めばいいのかな？
haskell-ja > Archives > 2011/06/16