Parametricity、Genericity

GHC.Baseの定義見ると、

foldr            :: (a -> b -> b) -> b -> [a] -> b
build 	:: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]

ってなってんだよね。forall付けていいときとダメな時の差がわかんねーと思って、
Theorems for free(P.Wadler)
http://www.informatik.uni-bonn.de/~loeh/ST-05-2003.pdf
あたりを眺めて見た。よく理解できなかったけど、色々あるのだなーと思った(小学生の感想か

Theorems for freeでは、foldの型が

fold : forall X.(forall Y.(X->Y->Y)->Y->[X]->Y

となってるぜ。なんでだろう。(==)の型が、forall x.x->x->Boolでないというのは、関数とかだと等しいことの判定ができるとは限らないので、当然じゃない？という気もしなくもない。型だけ見て定理が導けるというのは面白いね。全然理解してないが、こういう話はだ〜いすき。型情報利用して、動的にルールを生成するとかいうのも、GHCではやられてるんだろうか。あと、⊥=forall x.xの理由は何となく分かった気がしたよ。つうか、このへんの知識が全然ないよな〜、むー