module Algorithms.Nat.BasicOperations.Add where
import GHC.Natural
import Data.Functor.Foldable
Addition can be represented as catamorphism.
-- | >>> addCata 1 2
-- 3
addCata :: Natural -> Natural -> Natural
addCata n = cata \case
Nothing -> n
Just m -> 1 + m
Mendler-style implementation[^1]
-- | >>> addMCata 1 2
-- 3
addMCata :: Natural -> Natural -> Natural
addMCata n = mcata f . refix
where
f _ Nothing = n
f g (Just m) = 1 + g m
[1] Uustalu, Tarmo, and Varmo Vene. “Mendler-style inductive types, categorically.” Nord. J. Comput. 6.3 (1999): 343.