Life Goes On

まあまあだけど楽しんでる方です

SKS = I

なんで SKK = I なんだっけと考えていて、SKKx = Kx(Kx) = x で (Kx) は無視されるから、二つ目の K は他のコンビネータ(例えば S)でもいいよなと思ったわけです。

s x y z = x z (y z)
k x y = x

というように、Haskellで定義して実行すると、上手くいきません。
S の型は (a->b->c)->(a->b)->a->c なので、第一引数は a->b->c という型でないと NG な訳です。

*Main> putStrLn $ s k k "w"
w
*Main> putStrLn $ s k s "w"

<interactive>:1:17:
    Couldn't match expected type `t -> t1 -> t2'
           against inferred type `[Char]'
    In the third argument of `s', namely `"w"'
    In the second argument of `($)', namely `s k s "w"'
    In the expression: putStrLn $ s k s "w"

じゃあ、型がなければいいのかと考えて Grass でも実行。

wv		: I
wwWWWwwv		: K
wwwWWWwWWWwwWWwv	: S
WwwWwwWwwwwwwwwWWWWWWWw	: out (SKS double)
C:\grass>runghc grass sks.txt
w

今度はうまくいきました。
SKS = I と書ける「場合もある」と。
ってことは、型付きラムダ計算と型なしラムダ計算とでは、コンビネータの体系も変わってくるということなのかな。
その辺、整理した本とかないものかしら。