SKコンビネータ

ski.hs

{-# OPTIONS -fglasgow-exts #-}

i :: forall a. a -> a
i = \x -> x

k :: forall a b. a -> b -> a
k = \x -> \y -> x

s :: forall a b c. (a -> b -> c) -> (a -> b) -> a -> c
s = \x -> \y -> \z -> x z $ y z

ks :: forall a b c d. d -> ( (a -> b -> c) -> (a -> b) -> a -> c )
ks = k s

zero :: forall a. (a -> a) -> a -> a
zero = k i 
--one :: (a -> a) -> a -> a
--one = \f -> \x -> f x
--two :: (a -> a) -> a -> a
--two = s (s ks k)i -- S(S(KS)K)I

suc :: forall a. ( (a -> a) -> a -> a ) -> ( (a -> a) -> a -> a )
-- suc = \l -> \f -> \x -> l f $ f x
suc = s (s ks k) -- S(S(KS)K)

_1 :: forall a. (a -> a) -> a -> a
_1 = suc zero

_2 :: forall a. (a -> a) -> a -> a
_2 = suc _1

_3 :: forall a. (a -> a) -> a -> a
_3 = suc _2

_4 :: forall a. (a -> a) -> a -> a
_4 = _2 _2

_8 :: forall a. (a -> a) -> a -> a
_8 = _3 _2

_16 :: forall a. (a -> a) -> a -> a
_16 = _4 _2

_256 :: forall a. (a -> a) -> a -> a
_256 = _4 _4

true :: forall a b. a -> b -> a
true = k

false :: forall a b. a -> b -> b
false = \x -> \y -> y

cons :: forall a b c. a -> b -> (a -> b -> c) -> c
cons = \x -> \y -> s (s i (k x)) (k y)
--cons = s(k(s(k(s i))k))

car :: forall a b. ((a -> b -> a) -> a) -> a
car = \z -> z true

cdr :: forall a b. ((a -> b -> b) -> b) -> b
cdr = \z -> z false

--cdar :: forall a b c. (c -> ((a -> b -> a) -> a) -> a) -> a
cdar = \z -> car $ cdr z
cddr = \z -> cdr $ cdr z
cddar = \z -> car $ cdr $ cdr z
cdddr = \z -> cdr $ cdr $ cdr z

_if :: (a -> b -> c) -> a -> b -> c
_if = \c -> \x -> \y -> c x y

--nil :: ()
--nil = ()

nil = false

_not :: ((a -> b -> b) -> (a -> b -> a) -> c) -> c
_not = \x -> _if x false true 


--main = print $ (car (cons 2 1)) -- (succ) 0

-- B ( λxyz. x(yz) )
-- C ( λxyz. xzy )
-- W ( λxy. xyy )