How to implement Church encoding division in haskell?

Question

I'm a beginner in haskell, and trying to implement the Church encoding for natural numbers, as explained in this guide.

I'd like to implement a division between two church numerals.

{-# 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_sub :: Chur -> Chur -> Chur
ch_sub (Chr cn1) (Chr cn2) = cn2 pre (Chr cn1)

-- only works if b is a multiple of a
ch_div :: Chur -> Chur -> Chur
ch_div a b = suc $ y div_rec a b n0
div_rec :: (Chur -> Chur -> Chur -> Chur)-> Chur -> Chur -> Chur -> Chur
div_rec = (\r a b n -> iszero (ch_sub a b) n $ r (ch_sub a b) b (suc n))

n0 = zer
n1 = ic 1
n2 = ic 2
n3 = ic 3
n4 = ic 4

ch_div works when dividing multiples (e.g. 9 / 3), but not for fractions (e.g. 9 / 2).

*Main> ci $ ch_div (ic 9) n3
3
*Main> ci $ ch_div (ic 9) n2
5

If I omit the suc before div_rec, it works for the latter, but not for the former.

*Main> ci $ ch_div (ic 9) n3
2
*Main> ci $ ch_div (ic 9) n2
4

How do I define division to work for both cases?

Answer 1

You can implement < directly (using recursion) and then use it to define the division function. Here is an example:

type ChBool a = a -> a -> a

-- 'less than' function
lt :: Chur -> Chur -> ChBool x
lt = y (\r a b -> iszero a (iszero b 
                                   false           -- a = 0 & b = 0
                                   true)           -- a = 0 & b > 0
                           (r (pre a) (pre b)))    -- lt (a - 1) (b - 1)

ch_div :: Chur -> Chur -> Chur
ch_div = y (\r a b -> lt a b
                         zer
                         (suc (r (ch_sub a b) b)))

Tests:

λ> ci $ ch_div (ic 9) (ic 1)
9
λ> ci $ ch_div (ic 9) (ic 2)
4
λ> ci $ ch_div (ic 9) (ic 3)
3
λ> ci $ ch_div (ic 9) (ic 4)
2
λ> ci $ ch_div (ic 9) (ic 5)
1
λ> ci $ ch_div (ic 9) (ic 9)
1
λ> ci $ ch_div (ic 9) (ic 10)
0

And (as was already mentioned in comments) instead of y it's better to use a safe fixed-point combinator.

I must add that recursion is not necessary for implementing lt. It can be done like so:

-- boolean negation
ch_not a = a false true

-- greater or equal
ge a b = iszero $ ch_sub b a

-- less than
lt a b = ch_not (ge a b)