haskell.org

Haskell流に自分の足を撃つ方法が、Y-combinatorの定義だったなんて!

Haskellでは、実にElegantにLambda Calculusを実装できます。これをご覧になれば少しうっとりできるでしょう。

-- church numerals
ch_0 = \f x -> x
ch_1 = \f x -> f x
ch_2 = ch_succ ch_1
ch_3 = ch_succ ch_2
ch_4 = ch_succ ch_3
ch_5 = ch_succ ch_4
ch_6 = ch_succ ch_5
ch_7 = ch_succ ch_6
ch_8 = ch_succ ch_7
ch_9 = ch_succ ch_8
ch_succ  = \ n f x   -> f (n f x)
ch_add   = \ m n f x -> m f (n f x)
ch_mul   = \ m n f   -> m (n f)
ch_pow   = \ m n     -> n m
ch_pred  = \ n f x   -> n (\ g h -> h (g f)) (\ u -> x) (\ u -> u)
numify n = n (+1) 0
-- church bools
ch_true   = \ x y   -> x
ch_false  = \ x y   -> y
ch_and    = \ p q   -> p q ch_false
ch_or     = \ p q   -> p ch_true q
ch_not    = \ p     -> p ch_false ch_true
ch_xor    = \ p q   -> p (q ch_false ch_true) (q ch_true ch_false)
ch_if     = \ i t e -> i t e
boolify n = n True False
-- predecates
ch_iszero = \ n  -> n (\ x -> ch_false) ch_true
STICKITINURARS

ところがぎっちょんぎっちょんちょん。これが出来ないのです。

ch_y = \ f -> (\ x -> f (x x)) (\ x -> f (x x))

こんな風にしかられちゃいます。

    Occurs check: cannot construct the infinite type: t = t -> t1
      Expected type: t
      Inferred type: t -> t1
    In the first argument of `x', namely `x'
    In the first argument of `f', namely `(x x)'

こういう風に定義しちゃえばOKですが、こんなTrivialなのなら別にHaskellでなくたっていいもん。

ch_y  f =  f (ch_y f)
-- sub Y { my $f = shift; $f->(Y($f)) } # ひきょうもの〜!

ここにdefinitiveな解答が書いてありました。

The Evolution of a Haskell Programmer
Also note that we cannot define the Y combinator in terms of the others without running into typing problems (due essentially to issues of self-application).

な、なんかおいらはな、なっとくいかねーぞー!

識者のつっこみ激ヴォンヌ。→のようにつっこんで下さってもこの際OK!

(革命の日々さんより無断でお借りしております)

Dan the Y-discombinator