-- Нумерали на Чърч

c 0 = \f x -> x
-- c 1 = \f x -> f x
-- c 2 = \f x -> f (f x)
c n = \f x -> f (c (n-1) f x)

c5 = c 5

  c5 ( +1 ) 0 --- > 5
  c5 ( +2 ) 3 --- > 5 * 2 + 3 = 13

printnum c = c (+1) 0

  printnum c5 --- > 5
-- printnum (c n) ---> n

s = \n f x -> f (n f x)
  printnum ( s ( c 20 ) ) --- > 21

plus = \n m f x -> n f (m f x)
  printnum ( plus ( c 2 ) ( c 3 ) ) --- > 5

mult = \n m f x -> n (m f) x
  printnum ( mult ( c 2 ) ( c 3 ) ) --- > 6

ifthenelse = \x -> x

true = \x y -> x
false = \x y -> y

printbool b = b True False

iszero = \n -> n (\x -> false) true
-- printbool (iszero (c 0)) ---> True
-- printbool (iszero (c 10)) ---> False

cons = \x y b -> b x y

car = \z -> z true
cdr = \z -> z false

printnumpair z = (printnum (car z), printnum (cdr z))

z34 = cons (c 3) (c 4)

  printnumpair z34 --- > ( 3,4 )

p = \n -> cdr (n (\z -> cons (s (car z)) (car z)) (cons (c 0) (c 0)))
  printnum ( p ( c 10 ) ) --- > 9

-- "фалшива" реализация на Y комбинатора
      
  понеже директната дефиниция не е типизируема
y f = f (y f)

-- не можем да реализираме рекурсивен оператор дефиниращ f(x) = x!
  понеже директната дефиниция не е типизируема ! ! !
  но иначе би изглеждала подобно на това :
  factop =     ( iszero x ) ( c 1 ) ( mult x ( f ( p x ) ) )
-- fact = y factop

-- вижте num_types.hs за повече подробности чрез анотации на типове

 Нумерали на Чърч
 c 1 = \f x -> f x
 c 2 = \f x -> f (f x)
- > 5
- > 5 * 2 + 3 = 13
- > 5
 printnum (c n) ---> n
- > 21
- > 5
- > 6
 printbool (iszero (c 0)) ---> True
 printbool (iszero (c 10)) ---> False
- > ( 3,4 )
- > 9
 "фалшива" реализация на Y комбинатора
 не можем да реализираме рекурсивен оператор дефиниращ f(x) = x!
 fact = y factop
 вижте num_types.hs за повече подробности чрез анотации на типове

c 0 = \f x -> x
c n = \f x -> f (c (n-1) f x)

c5 = c 5


printnum c = c (+1) 0


s = \n f x -> f (n f x)

plus = \n m f x -> n f (m f x)

mult = \n m f x -> n (m f) x

ifthenelse = \x -> x

true = \x y -> x
false = \x y -> y

printbool b = b True False

iszero = \n -> n (\x -> false) true

cons = \x y b -> b x y

car = \z -> z true
cdr = \z -> z false

printnumpair z = (printnum (car z), printnum (cdr z))

z34 = cons (c 3) (c 4)


p = \n -> cdr (n (\z -> cons (s (car z)) (car z)) (cons (c 0) (c 0)))

      
  понеже директната дефиниция не е типизируема
y f = f (y f)

  понеже директната дефиниция не е типизируема ! ! !
  но иначе би изглеждала подобно на това :
  factop =     ( iszero x ) ( c 1 ) ( mult x ( f ( p x ) ) )

