#fix f = let x = f x in x
#が
#fix f = f (fix f)
#と同じになる理由を教えて下さい。
#ここで、let と letrec を区別すると、
#fix f = letrec x = f x in x
#となり。
#let v = B in E == (\v -> E) B
なので、
#fix f = let x = fix (\x -> f x) in x
#となり
#letrec v = B in E == let v = fix (\v -> B) in E
#なので
#fix f = (\x -> x) (fix (\x -> f x))
#となります。
#"=" の右側が (\x -> f x) になればいいのですが、(\x -> x) になってしまいました。
#どこが間違っていますか?
#(RankNTypes のように)型推論がうまくいかないところに、型レベルλを書けるような拡張を入れれば type synonym の部分適用ができるだろうという意見が来ていますが、そうなると部分適用できてもあんまり嬉しくないかもしれませんね……。
##うれしくないのはなぜですか?
#型レベルλを(自分の意思ではなく)コンパイラに強制されて型を合わせるために書きたいですか? もちろん、記述がどのくらい煩雑になるかにもよりますが。
#任意に型レベルλを書けないということですか?