-- | See 'Peano'. module Data.Peano ( Peano (Zero, Succ), infinity ) where import Data.Data ( Data, Typeable ) import Data.Ix ( Ix( index, inRange, range, rangeSize ) ) -- | The natural numbers in (lazy) unary notation. data Peano = Zero | Succ Peano deriving (Eq, Ord, Typeable, Data, Read, Show) instance Enum Peano where succ = Succ pred (Succ n) = n pred Zero = error "Data.Peano.pred Zero" toEnum = fromInteger . toEnum fromEnum = fromEnum . toInteger instance Bounded Peano where minBound = Zero maxBound = infinity instance Ix Peano where range = uncurry enumFromTo index (l, _) n = fromEnum (n - l) inRange (l, u) n = l <= n && u >= n rangeSize (l, u) = fromEnum (Succ u - l) instance Num Peano where Zero + n = n Succ m + n = Succ (m + n) m - Zero = m Succ m - Succ n = m - n Zero - _ = error "Data.Peano.(-): underflow (negative)" Zero * _ = Zero Succ m * n = n + m * n abs = id signum Zero = Zero signum _ = Succ Zero fromInteger n = case compare n 0 of LT -> error "fromInteger n | n < 0" EQ -> Zero GT -> Succ (fromInteger (n - 1)) instance Real Peano where toRational = toRational . toInteger instance Integral Peano where toInteger Zero = 0 toInteger (Succ n) = toInteger n + 1 Zero `quotRem` Zero = error "Data.Peano.quotRem: zero divided by zero" m `quotRem` n = case compare m n of LT -> (Zero, m) _ -> let (q, r) = quotRem (m - n) n in (Succ q, r) divMod = quotRem -- | The infinite number (ω). infinity :: Peano infinity = Succ infinity