module Data.Natural where

import Control.Functor
import Data.Fixpoint
import Data.Function
import Data.Monoid
import Data.Wrapper

data Natural = Zero | Succ Natural

instance Fixpoint Hask Natural where
    data Pre Natural a = S a | Z

    project Zero = Z
    project (Succ n) = S n

    inject Z = Zero
    inject (S n) = Succ n

instance Functor Hask (Pre Natural) where
    _ $> Z = Z
    f $> S x = S (f x)

newtype NaturalSum = NaturalSum { getNaturalSum :: Natural }

instance Wrapper NaturalSum where
    type Inner NaturalSum = Natural
    wrap = NaturalSum
    unwrap = getNaturalSum

instance Magma NaturalSum where
    a `op` b = wrap . cata addPre . unwrap $ a
        where addPre Z = unwrap b
              addPre (S n) = Succ n

instance Semigroup NaturalSum

instance Unital NaturalSum where
    unit = NaturalSum Zero

instance Monoid NaturalSum

infinity :: Natural
infinity = Succ infinity