Как реализовать разделение колоний в хэскелле?

Question

Я новичок в haskell и пытаюсь внедрить церковную кодировку для натуральных чисел, как объясняется в this guide.

Я хотел бы осуществить разделение между двумя церковными цифрами.

{-# 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 работы при делении кратные (например 9/3), но не для фракций (например 9/2).

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

Если я опустить suc перед тем div_rec, он работает для последнего, но не бывший.

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

Как определить деление для работы в обоих случаях?

Answer 1

Вы можете реализовать непосредственно < (используя рекурсию), а затем использовать его для определения функции деления. Вот пример:

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))) 

Тесты:

λ> 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 

И (как уже упоминалось в комментариях) вместо y лучше использовать безопасный комбинатор неподвижной точки.

Должен добавить, что для реализации рекурсия не требуется. Это можно сделать так:

-- 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)