title: How to implement Church encoding division in haskell?
body: <p>I'm a beginner in haskell, and trying to implement the Church encoding for natural numbers, as explained in <a href="http://archive.is/dumJ2" rel="nofollow">this guide</a>.</p>
  
  <p>I'd like to implement a division between two church numerals.</p>
  
  <pre><code>{-# LANGUAGE RankNTypes #-}
  
  import Unsafe.Coerce
  
  y :: (a -&gt; a) -&gt; a
  y = \f -&gt; (\x -&gt; f (unsafeCoerce x x)) (\x -&gt; f (unsafeCoerce x x))
  
  true = (\x y -&gt; x)
  false = (\x y -&gt; y)
  
  newtype Chur = Chr (forall a. (a -&gt; a) -&gt; (a -&gt; a))
  
  zer :: Chur
  zer = Chr (\x y -&gt; y)
  
  suc :: Chur -&gt; Chur
  suc (Chr cn) = Chr (\h -&gt; cn h . h)
  
  ci :: Chur -&gt; Integer
  ci (Chr cn) = cn (+ 1) 0
  
  ic :: Integer -&gt; Chur
  ic 0 = zer
  ic n = suc $ ic (n - 1)
  
  
  -- church pair
  type Chp = (Chur -&gt; Chur -&gt; Chur) -&gt; Chur
  
  pair :: Chur -&gt; Chur -&gt; Chp
  pair (Chr x) (Chr y)  f = f (Chr x) (Chr y)
  
  ch_fst :: Chp -&gt; Chur
  ch_fst p = p true
  
  ch_snd :: Chp -&gt; Chur
  ch_snd p = p false
  
  next_pair :: Chp -&gt; Chp
  next_pair = (\p x -&gt; x (suc (p true)) (p true))
  
  n_pair :: Chur -&gt; Chp -&gt; Chp
  n_pair (Chr n) p = n next_pair p
  
  p0 = pair zer zer
  pre :: Chur -&gt; Chur
  pre (Chr cn) = ch_snd $ n_pair (Chr cn) p0
  
  iszero :: Chur -&gt; (a-&gt;a-&gt;a)
  iszero (Chr cn) = cn (\h -&gt; false) true
  
  unchr :: Chur -&gt; ((a -&gt; a) -&gt; (a -&gt; a))
  unchr (Chr cn) = cn
  
  ch_sub :: Chur -&gt; Chur -&gt; Chur
  ch_sub (Chr cn1) (Chr cn2) = cn2 pre (Chr cn1)
  
  -- only works if b is a multiple of a
  ch_div :: Chur -&gt; Chur -&gt; Chur
  ch_div a b = suc $ y div_rec a b n0
  div_rec :: (Chur -&gt; Chur -&gt; Chur -&gt; Chur)-&gt; Chur -&gt; Chur -&gt; Chur -&gt; Chur
  div_rec = (\r a b n -&gt; 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
  </code></pre>
  
  <p><code>ch_div</code> works when dividing multiples (e.g. <code>9 / 3</code>), but not for fractions (e.g. <code>9 / 2</code>).</p>
  
  <pre><code>*Main&gt; ci $ ch_div (ic 9) n3
  3
  *Main&gt; ci $ ch_div (ic 9) n2
  5
  </code></pre>
  
  <p>If I omit the <code>suc</code> before <code>div_rec</code>, it works for the latter, but not for the former.</p>
  
  <pre><code>*Main&gt; ci $ ch_div (ic 9) n3
  2
  *Main&gt; ci $ ch_div (ic 9) n2
  4
  </code></pre>
  
  <p>How do I define division to work for both cases?</p>