-- |Support for natural numbers. module Data.Natural ( Natural, monus, View (Zero, Succ), view, fold ) where import Data.Monoid {-FIXME: Maybe, we should have more rewrite rules. See and . Should we also include an alternative of plus/minus with swapped order of (+)-arguments? -} {-# RULES "pred/succ" forall nat . pred (succ nat) = nat "minus/plus" forall nat1 nat2 . (nat1 + nat2) - nat2 = nat1 "monus/plus" forall nat1 nat2 . (nat1 + nat2) `monus` nat2 = nat1 "signum/succ" forall nat . signum (succ nat) = Natural 1 "fromInteger/toInteger" forall nat . fromInteger (toInteger nat) = nat "view/succ" forall nat . view (succ nat) = Succ (uncheckedPred nat) #-} -- An unchecked version of pred, which is only used internally for the rewrite rule view/succ. uncheckedPred :: Natural -> Natural uncheckedPred (Natural integer) = Natural (pred integer) {-| The type of natural numbers. Note that matching a natural number against a negative pattern might not work as you expect. For example, evaluating the following expression results in a run-time error, instead of the result @\"plus five\"@: @ case 5 :: Natural of -5 -> \"minus five\" 5 -> \"plus five\" @ The reason is that the @==@ operator of @Natural@ is used for checking if the patterns match, making it necessary to convert @-5@ to Natural. -} newtype Natural = Natural Integer deriving (Eq, Ord) {- We do not just provide a minimal complete definition. The reason is that all default implementations use toEnum and fromEnum internally. Unfortunately, these use Int instead of Integer, which can lead to overflows. Furthermore, we can avoid the negativity check in some methods. -} instance Enum Natural where succ (Natural integer) = Natural (succ integer) pred = fromInteger . pred . toInteger toEnum = fromInteger . toEnum fromEnum = fromEnum . toInteger enumFrom (Natural start) = map Natural (enumFrom start) enumFromThen (Natural start) (Natural next) = map Natural $ if start > next then enumFromThenTo start next 0 else enumFromThen start next enumFromTo (Natural start) (Natural end) = map Natural (enumFromTo start end) enumFromThenTo (Natural start) (Natural next) (Natural end) = map Natural $ enumFromThenTo start next end instance Show Natural where showsPrec prec (Natural integer) = showsPrec prec integer instance Read Natural where readsPrec prec str = map (first fromInteger) (readsPrec prec str) where -- This is Control.Arrow.first, specialized to (->). first :: (val -> val') -> (val,other) -> (val',other) first fun (val,other) = (fun val,other) instance Num Natural where Natural integer1 + Natural integer2 = Natural (integer1 + integer2) Natural integer1 - Natural integer2 = fromInteger (integer1 - integer2) Natural integer1 * Natural integer2 = Natural (integer1 * integer2) abs = id signum (Natural integer) = Natural (signum integer) fromInteger integer | integer >= 0 = Natural integer | otherwise = error "Data.Natural: natural cannot be negative" instance Real Natural where toRational = toRational . toInteger instance Integral Natural where quotRem (Natural integer1) (Natural integer2) = let (quot,rem) = quotRem integer1 integer2 in (Natural quot,Natural rem) {- Although an implementation of divMod is generally not needed for a minimal complete definition, we have to include one, since the default implementation relies on negative numbers being available. -} divMod = quotRem toInteger (Natural integer) = integer {-| Yields the monus of two natural numbers, which is their difference if the first number is greater than the second, and zero otherwise. -} monus :: Natural -> Natural -> Natural monus (Natural integer1) (Natural integer2) | integer1 > integer2 = Natural (integer1 - integer2) | otherwise = Natural 0 {-| A data type for views of natural numbers. -} data View = Zero | Succ Natural {-| Yields the view of a natural number. -} view :: Natural -> View view (Natural 0) = Zero view (Natural integer) = Succ (Natural (pred integer)) {-| Folding of natural numbers. -} fold :: accu -> (accu -> accu) -> Natural -> accu fold zeroAccu _ (Natural 0) = zeroAccu fold zeroAccu succAccu (Natural integer) = succAccu $ fold zeroAccu succAccu (Natural (pred integer))