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.