Y combinator (続き)
昨日の 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 という型等式が成り立つ必要がある。Y は再帰 combinator なんだから、当り前。考えたけどこれを回避する方法は思いつかなかったので Wikipedia を見てみると "simply-typed" なλ算法では「再帰型」を定義しないと Y は書けないそうで。それ Y の意味無い。ネタ元の link を載せてた nuc さんが Haskell を弱くした言語が欲しいと言ってたのはこの事か。んで Wikipedia に載ってる Haskell 博士の解答例が目に映ってしまったけど、何か形というか幅が違う。急いで目を逸したので詳しくはわからず。自分の結果に納得したらまた見てみるべし。見たいけど見たくない、この葛藤。本物の数学者とかは見たくないとしか思わないのだろうか。
で、Scheme というか正格な言語で動かないのはなぜか。Hand-assemble ならぬ hand-interpret してみれば xxh を遅延してないからだとわかる。
a := λx.λh.h(xxh)
Y := aa
aaf = f (xxf) {自由変数束縛: x = a}で、eager に評価するなら xxf (= aaf) の部分が aaf の評価時に評価される。つまり無限再帰。しかも末尾じゃない。考えてみたら当り前の事で、"Yf = f(Yf)" を文字どおりに実装しようとすると遅延が足りません。Applicative-order では遅延されてない全ての表現を喰い尽くすまで評価器が走るので、f(Yf) の一番左の f の適用は実行されざるを得ない。よって monad 的(?)*1な考え方で、再帰するという処理の流れを作り出してそれをλでくるんで (遅延して) 返す、みたいな。あー正確に言葉にできん。というかできたら多分もう答えが出てる。
今日はもう遅いのでまた明日。考えながら寝るべ。
