因为有人提到，所以复习了一下..
1. Y combinator in Haskell
Y combinator 在 untyped lambda calculus 中是
\f -> (\x -> f (x x)) (\x -> f (x x))
试着写成 Haskell:
y :: (a -> a) -> a
y f = (\x -> f (x x)) (\x -> f (x x))
f 的型别是 a -> a, 而 y 取 f 的 fixed-point，
所以 y 的型别是 (a -> a) -> a.
但是这个型别一看就有问题：把 type 看成逻辑的话，
这个 type 若有证明就会有 inconsistency. 果然， Haskell
不让这个程式 typecheck:
Occurs check: cannot construct the infinite type: t = t -> a
Probable cause: `x' is applied to too many arguments
In the first argument of `f', namely `(x x)'
In the expression: f (x x)
操作上的理由是：在 (x x) 之中，x 的型别又是 t -> a, 又是 t, 而
t = t -> a 递回定义。
解决方法也很简单，就头痛医头脚痛医脚，做一个 t 与 t -> a
同构的递回型别囉。
data Fix a = Rec (Fix a -> a)

Cool! Thanks!