Comment implémenter la division d'encodage d'église dans haskell?

Question

Je suis un débutant dans haskell, et en essayant de mettre en œuvre l'encodage de l'église pour les nombres naturels, comme expliqué dans this guide.

Je voudrais implémenter une division entre deux nombres d'église.

{-# 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 travaux lors de la division multiples (par exemple 9/3), mais pas pour les fractions (par exemple 9/2).

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

Si j'omettent le suc avant div_rec, il travaille pour ce dernier, mais pas pour la première.

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

Comment définir la division pour fonctionner dans les deux cas?

Answer 1

Vous pouvez implémenter < directement (en utilisant la récursivité), puis l'utiliser pour définir la fonction de division. Voici un exemple:

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 

Et (comme on l'a déjà mentionné dans les commentaires) au lieu de y il est préférable d'utiliser un combinateur sûr point fixe.

Je dois ajouter que la récursivité n'est pas nécessaire pour implémenter lt. Cela peut être fait comme suit:

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