Church Number

Church.hs

module Church where

import Prelude ((.), ($), id, fst, undefined, length)

zero  f = id
inc n f = f . n f

one   f = f
two   f = f . f
three f = f . f . f

succ n f   = f . n f
plus m n f = m f . n f
mult m n   = (n . m)        -- mult m n f = plus m (plus m ... ) f
                            --            = m f . m f . ...
                            --            = (m f)^n
                            --            = n (m f)
                            --            = (n . m) f

exp  m n   = n m            -- exp  m n   = (mult m (mult m ... ))
                            --            = m . m . ... = n m

-- next (x, y) = (y, succ y)
-- pred n = fst $ n next (undefined, zero)

cons x y = \m -> m x y
car z = z (\p q -> p)
cdr z = z (\p q -> q)

next z = cons (cdr z) (succ (cdr z))
pred n = car $ n next (cons undefined zero)

sub m n = n pred m -- 类型错误啊，坑爹！！！

true = \a b -> a
false = \a b -> b

isZero n a b = n (\_ -> b) a

and x y a b = x (y a b) b
or  x y a b = x a (y a b)
not x a b   = x b a
xor x y a b = x (y b a) (y a b)

ifElse m a b = m a b

showChurch n = length $ n (undefined:) []
showChurchBool n = length $ n [undefined] []

sub m n = n pred m有问题。

not working

*Main> (sub three one) (1+) 0
2
*Main> (sub three two) (1+) 0

<interactive>:15:12: error:
    • Occurs check: cannot construct the infinite type:
        b
        ~
        (((b -> b) -> b -> b)
         -> ((b -> b) -> b -> b) -> (b -> b) -> b -> b)
        -> (b -> b) -> b -> b
      Expected type: (((((((b -> b) -> b -> b)