Discussion: add pattern synonyms and a non-dependent eliminator to Numeric.Natural

[David Feuer]

Pattern synonyms:

pattern Successor :: Natural -> Natural
pattern Successor n <- (precMaybe -> Just n)
  where
    Successor n = n + 1

precMaybe :: Natural -> Maybe Natural
precMaybe 0 = Nothing
precMaybe n = Just (n - 1)

pattern Zero :: Natural
pattern Zero = 0

Eliminator:

toChurch :: Natural -> (a -> a) -> a -> a
toChurch 0 _ b = b
toChurch n f b = f (toChurch (n-1) f b)

There are several other possible argument orders, the most natural of which
is probably

natural :: a -> (a -> a) -> Natural

I don't have particularly strong feelings about whether we should pick one
or offer both.

There are two strictly accumulating versions, corresponding to different
versions of foldl'. But toChurch/natural is sufficient to define them:

toChurch', toChurch'' :: Natural -> (a -> a) -> a -> a
toChurch' n f = toChurch n (\r acc -> r $! f acc) id

toChurch'' n f = toChurch n (\r !acc -> r $ f acc) id

So we shouldn't necessarily feel obligated to include those. I doubt the
time is ripe for a dependent eliminator.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20161102/6003805d/attachment.html>