yx-eq-x(yx).md

y x = x (y x)の型推論

1. y :: bとおく。
2. x :: cとおく。
3. y x :: dとおく。
4. (1.)(2.)(3.)よりbとc -> dは等しい。
5. (4.)よりy :: c -> dである。
6. x (y x) :: aとおく。
7. (2.)(3.)(6.)よりcとd -> aは等しい。
8. (2.)(7.)よりx :: d -> aである。
9. (5.)(7.)よりy :: (d -> a) -> dである。
10. (6.)(8.)より\x -> x (y x) :: (d -> a) -> aである。
11. (9.)(10.)よりdとaは等しい。
12. (11.)よりy :: (a -> a) -> aである。