昨日の Y combinator を Haskell に入れてみたけど、無限型を生じるからと言って拒否される。問題は Y=λg.g( (λx.λh.h(xxh)) (λx.λh.h(xxh)) g )の xxh の部分。x::X, h::H と仮定すると、xxh という表現が意味をもつには X = X -> H -> a という型等式が成…

挑戦した。解いた顛末をそのまま dump するという、まさしく (そして珍しく)「日記」な内容。 ∀f, f(Yf) = Yf ←これを逆から読む。すると Y = λg.g(Yg) になることがわかる。これをさらに naïve に展開すると Y = λg.g(Yg) = λg.g(λh.h(Yh))g = λg.g(λh.h((λ…