<p dir="ltr">Pattern synonyms:</p>
<p dir="ltr">pattern Successor :: Natural -> Natural<br>
pattern Successor n <- (precMaybe -> Just n)<br>
  where<br>
    Successor n = n + 1</p>
<p dir="ltr">precMaybe :: Natural -> Maybe Natural<br>
precMaybe 0 = Nothing<br>
precMaybe n = Just (n - 1)</p>
<p dir="ltr">pattern Zero :: Natural<br>
pattern Zero = 0</p>
<p dir="ltr">Eliminator:</p>
<p dir="ltr">toChurch :: Natural -> (a -> a) -> a -> a<br>
toChurch 0 _ b = b<br>
toChurch n f b = f (toChurch (n-1) f b)</p>
<p dir="ltr">There are several other possible argument orders, the most natural of which is probably</p>
<p dir="ltr">natural :: a -> (a -> a) -> Natural</p>
<p dir="ltr">I don't have particularly strong feelings about whether we should pick one or offer both.</p>
<p dir="ltr">There are two strictly accumulating versions, corresponding to different versions of foldl'. But toChurch/natural is sufficient to define them:</p>
<p dir="ltr">toChurch', toChurch'' :: Natural -> (a -> a) -> a -> a<br>
toChurch' n f = toChurch n (\r acc -> r $! f acc) id</p>
<p dir="ltr">toChurch'' n f = toChurch n (\r !acc -> r $ f acc) id</p>
<p dir="ltr">So we shouldn't necessarily feel obligated to include those. I doubt the time is ripe for a dependent eliminator.</p>