I'm a beginner in haskell, and trying to implement the Church encoding for natural numbers, as explained in this guide. I used a definition of y combinator from this answer, but not sure how to apply it.
I'd like to implement a simple function in lambda calculus which computues the sum of [1..n] as demonstrated here.
{-# LANGUAGE RankNTypes #-}
import Unsafe.Coerce
y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))
true = (\x y -> x)
false = (\x y -> y)
newtype Chur = Chr (forall a. (a -> a) -> (a -> a))
zer :: Chur
zer = Chr (\x y -> y)
suc :: Chur -> Chur
suc (Chr cn) = Chr (\h -> cn h . h)
ci :: Chur -> Integer
ci (Chr cn) = cn (+ 1) 0
ic :: Integer -> Chur
ic 0 = zer
ic n = suc $ ic (n - 1)
-- church pair
type Chp = (Chur -> Chur -> Chur) -> Chur
pair :: Chur -> Chur -> Chp
pair (Chr x) (Chr y) f = f (Chr x) (Chr y)
ch_fst :: Chp -> Chur
ch_fst p = p true
ch_snd :: Chp -> Chur
ch_snd p = p false
next_pair :: Chp -> Chp
next_pair = (\p x -> x (suc (p true)) (p true))
n_pair :: Chur -> Chp -> Chp
n_pair (Chr n) p = n next_pair p
p0 = pair zer zer
pre :: Chur -> Chur
pre (Chr cn) = ch_snd $ n_pair (Chr cn) p0
iszero :: Chur -> (a->a->a)
iszero (Chr cn) = cn (\h -> false) true
unchr :: Chur -> ((a -> a) -> (a -> a))
unchr (Chr cn) = cn
ch_sum (Chr cn) = (\r -> iszero (Chr cn) zer (cn suc (r (pre (Chr cn)))))
So far so good, but how do I apply y
to sum
?
e.g.
n3 = ic 3
y ch_sum n3
causes a type mismatch:
<interactive>:168:3:
Couldn't match type ‘(Chur -> Chur) -> Chur’ with ‘Chur’
Expected type: ((Chur -> Chur) -> Chur) -> (Chur -> Chur) -> Chur
Actual type: Chur -> (Chur -> Chur) -> Chur
In the first argument of ‘y’, namely ‘ch_sum’
In the expression: y ch_sum n3
<interactive>:168:10:
Couldn't match expected type ‘Chur -> Chur’ with actual type ‘Chur’
In the second argument of ‘y’, namely ‘n3’
In the expression: y ch_sum n3
Y Combinator in Haskell provides the definition of y combinator, but doesn't explain how to use it.
I've introduced the function add
(which obviously adds two Church numerals) to simplify the ch_sum
's definition:
add :: Chur -> Chur -> Chur
add (Chr cn1) (Chr cn2) = Chr (\h -> cn1 h . cn2 h)
To create a recursive function using a fixed-point combinator, you need to write it as it was an ordinary recursive function (in a language with recursion), but as a last step add the explicit "self" argument as the first function's argument (r
in this case) and instead of a recursive call you just call "self" (r
). So ch_sum
can be written as
ch_sum :: (Chur -> Chur) -> Chur -> Chur
ch_sum = \r n -> iszero n zer $ add n (r $ pre n)
A couple tests in ghci:
λ> let n3 = ic 3
λ> ci (y ch_sum n3)
6
λ> let n10 = ic 10
λ> ci (y ch_sum n10)
55