church-numerals1.hs

{-# LANGUAGE RankNTypes #-}

type Church = forall t. (t -> t) -> t -> t

--churchToInt' :: forall a. (Num	a) =>
--	((a -> a) -> a -> a) -> a
churchToInt' :: ((Int -> Int) -> Int -> Int) -> Int
churchToInt' c = c (+1) 0


zero' :: Church
--zero' = \f z -> z
zero' = flip const

one' :: Church
--one' = \f z -> f z
--one' f z = f z
one' f = f


two' :: Church
--two' = \f z -> (f . f) z
two' f = f . f

three' :: Church
three' f = f . f . f

four' :: Church
four' = succ' three'

--succ'    :: ((t -> t) -> t -> t) -> (t -> t) -> t -> t
succ' :: Church -> Church
--succ' c = \f o -> f $ c f o
--succ' c f o = f $ c f o
succ' c f = f . c f 

nthSucc' :: Int -> Church -> Church
--nthSucc' 0 c f o = c f o
--nthSucc' n c f o = f $ nthSucc' (n-1) c f o

nthSucc' 0 c f = c f
nthSucc' n c f = f . nthSucc' (n-1) c f


add :: Church -> Church -> Church
c1 `add` c2 = \f -> c1 f . c2 f 

prod :: Church -> Church -> Church
prod c1 c2 = c1 . c2

main :: IO ()
main = do 
	print $ churchToInt' zero'
	print $ churchToInt' one'
	print $ churchToInt' two'
	print $ churchToInt' three'
	print $ churchToInt' four'
	print $ churchToInt' $ nthSucc' 10 zero'
	print $ churchToInt' $ three' `add` two'
	print $ churchToInt' $ three' `prod` two'

church-numerals1.ls

{flip, map, id, curry} = require \prelude-ls

constant = (a, f) --> a


churchToInt = (c) -> c (+ 1), 0

zero = (f, z) --> z

one = (f, z) --> z |> f

two = (f, z) --> z |> f . f


incr = (c) ->
	(f, z) --> z |> f . c f
	# (f, z) --> f (c f, z)

three = incr two
four = incr three

add = (a, b) -->
	(f, z) --> z |> (a f) . (b f)


# church numeral (here a) is a function that takes f and z
# and it applies f as many times as the value of the numeral
# each time passing the previous result of the invocation to f
# starting from f z
add = (a, b) --> 
	(f, z) --> (b incr, a) f, z

mult = (a, b) -->
	(f, z) --> (b (add a), zero) f, z

pow = (a, b) -->
	(f, z) --> (b (mult a), one) f, z


console.log <| churchToInt one

console.log <| churchToInt three

console.log <| churchToInt (three `add` two)

console.log <| churchToInt (two `add` four)

console.log <| churchToInt (three `mult` four)

console.log <| churchToInt (two `pow` (incr four))



# eta reduced

add = (a, b) --> b incr, a

mult = (a, b) --> b (add a), zero

pow = (a, b) --> b (mult a), one


console.log <| churchToInt three

console.log <| churchToInt <| three `add` two

console.log <| churchToInt (two `add` four)

console.log <| churchToInt (three `mult` four)

console.log <| churchToInt (two `pow` (incr four))


console.log \----
# dec

suc = ([_, b]) -> [b, incr b]
dec = (b) -> 
	[x, _] = b suc, [undefined, zero]
	x

sub = (a, b) --> b dec, a



console.log <| suc [undefined, one] |> map churchToInt
console.log <| churchToInt <| dec four
console.log <| churchToInt <| (four `pow` two) `sub` three