{- | Copyright : (c) Peter Divianszky 2008 Maintainer : divip@aszt.inf.elte.hu Stability : experimental Portability : portable Lazy Peano numbers including observable infinity value. Properties of @Num@ can be found in the source of 'Number.Peano.Inf.Test'. The lazy operations of @Num@ makes it ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@. -} module Number.Peano.Inf ( Nat , infinity , inductive_infinity , diff , zeroDiff , infDiff , (-|) ) where import Test.LazySmallCheck (Serial(..), cons0, cons1, (\/)) {- Implementation Notes The observable infinity value has many representatives: > Inf > Succ Inf > Succ (Succ Inf) > ... The representatives are needed to keep (+) lazy in its second argument. Multiple representatives need extra caretaking: Every function on @Nat@ must be well defined. A function @f :: Nat -> Nat@ is well defined if for all @n@ and @m@ which are representatives of the observable infinity, both @f n@ and @f m@ should be * either @0@, @1@, @2@, ..., @bottom@, @Succ bottom@, @Succ (Succ bottom)@, ... * or (maybe different) representatives of the observable infinity The functions in this module obey this rule. The abstract @Nat@ data type ensures that the users should not take care of this rule. -} -- | Natural numbers and infinity. data Nat = Zero | Succ Nat | Inf instance Serial Nat where series = cons0 Zero \/ cons1 Succ \/ cons0 Inf {- | Observable infinity value. -} infinity :: Nat infinity = Inf {- | Traditional infinity value: @let n = Succ n in n@. For every function @f :: Nat -> Bool@, @f infinity@ and @f inductive_infinity@ gives the same result, provided that the results are not bottom. Use @infinity@ instead. Lots of the given properties of @infinity@ is not true for @inductive_infinity@. For example, * @inductive_infinity == inductive_infinity@ is an endless computation instead of @True@. However, the following values are @True@: * @n < inductive_infinity@, @n@ = 0, 1, 2,... Note also: * @inductive_infinity == infinity@ is an endless computation instead of @True@. -} inductive_infinity :: Nat inductive_infinity = let n = Succ n in n instance Eq Nat where Zero == Zero = True Succ n == Succ m = n == m Inf == Inf = True Succ n == Inf = n == Inf Inf == Succ m = Inf == m _ == _ = False instance Ord Nat where Zero `compare` Zero = EQ Zero `compare` _ = LT _ `compare` Zero = GT Succ n `compare` Succ m = n `compare` m Inf `compare` Inf = EQ Inf `compare` Succ m = Inf `compare` m Succ n `compare` Inf = n `compare` Inf _ < Zero = False Zero < _ = True Succ n < Succ m = n < m Inf < Inf = False Inf < Succ m = Inf < m Succ n < Inf = n < Inf n > m = m < n n <= m = not (m < n) n >= m = not (n < m) Zero `max` m = m n `max` Zero = n Succ n `max` Succ m = Succ (n `max` m) _ `max` _ = Inf Zero `min` _ = Zero _ `min` Zero = Zero Succ n `min` Succ m = Succ (n `min` m) Inf `min` m = m n `min` Inf = n toInteger' :: Nat -> Maybe Integer toInteger' n = f 0 n where f i Zero = Just i f i (Succ m) = i' `seq` f i' m where i' = i+1 f _ Inf = Nothing instance Show Nat where show n = case toInteger' n of Just i -> show i Nothing -> "infinity" {- | Difference of two natural numbers: the result is either positive or negative. implementation of @(-)@ is based on @diff@. The following value is undefined: * @diff infinity infinity@ -} diff :: Nat -- ^ n -> Nat -- ^ m -> Either Nat Nat -- ^ n >= m: Left (n-m), n < m: Right (m-n) n `diff` Zero = Left n Zero `diff` m = Right m Succ n `diff` Succ m = n `diff` m Inf `diff` Inf = error "Number.Peano.Inf: infinity - infinity." Inf `diff` Succ m = Inf `diff` m Succ n `diff` Inf = n `diff` Inf {- | Variant of @diff@: * @infDiff infinity infinity == Left infinity@. Note that if the implementation of @(-)@ would be based on @infDiff@, the following equations would not hold: * @(a - b) - (a - c) == c - b@, @a >= c >= b@, because @(infininty - 5) - (infinity - 10) == infinity /= 10 - 5@. * @a - (a - b) == b@, @a >= b@, because @infininty - (infinity - 5) == infinity /= 5@. -} infDiff :: Nat -- ^ n -> Nat -- ^ m -> Either Nat Nat -- ^ n >= m: Left (n-m), n < m: Right (m-n) Inf `infDiff` _ = Left Inf Succ n `infDiff` Succ m = n `infDiff` m Succ n `infDiff` Inf = n `infDiff` Inf n `infDiff` Zero = Left n Zero `infDiff` m = Right m {- | Variant of @diff@: * @zeroDiff infinity infinity == Left 0@. Note that if the implementation of @(-)@ would be based on @zeroDiff@, the following equations would not hold: * @(a - b) - (a - c) == c - b@, @a >= c >= b@, because @(infininty - 5) - (infinity - 10) == 0 /= 10 - 5@. * @a - (a - b) == b@, @a >= b@, because @infininty - (infinity - 5) == 0 /= 5@. -} zeroDiff :: Nat -- ^ n -> Nat -- ^ m -> Either Nat Nat -- ^ n >= m: Left (n-m), n < m: Right (m-n) n `zeroDiff` Zero = Left n Zero `zeroDiff` m = Right m Succ n `zeroDiff` Succ m = n `zeroDiff` m Inf `zeroDiff` Inf = Left Zero Inf `zeroDiff` Succ m = Inf `zeroDiff` m Succ n `zeroDiff` Inf = n `zeroDiff` Inf -- | Non-negative subtraction. For example, @(5 -| 8 == 0)@. infixl 6 -| (-|) :: Nat -> Nat -> Nat n -| m = case n `diff` m of Left k -> k Right _ -> Zero instance Num Nat where n - m = case n `diff` m of Left k -> k Right _ -> error "Number.Peano.Inf: 0 - succ n." Zero + m = m Succ n + m = Succ (n + m) Inf + _ = Inf Succ n * m = m + n * m Zero * _ = Zero _ * Zero = Zero Inf * _ = Inf fromInteger i | i < 0 = error "Number.Peano.Inf: fromInteger on negative value." fromInteger i = iterate Succ Zero !! fromInteger i abs n = n signum Zero = Zero signum _ = Succ Zero instance Enum Nat where succ = Succ pred Inf = Inf pred (Succ n) = n pred Zero = error "Number.Peano.Inf: pred 0." toEnum i | i < 0 = error "Number.Peano.Inf: toEnum on negative value." toEnum i = iterate Succ Zero !! i enumFrom n = enumFromTo n Inf {- | @[inf.. inf] == [inf, inf, inf, ..@ instead of @[inf.. inf] == [inf]@ Both have sense, but the second solution would make @enumfrom@ more eager. -} enumFromTo n m = case m `infDiff` n of Right _ -> [] Left k -> f k n where f Zero l = [l] f (Succ j) l = l: f j (Succ l) f Inf l = iterate Succ l enumFromThen n n' = case n `zeroDiff` n' of -- constant sequence Left Zero -> n: repeat n' -- decreasing sequence Left d -> n: n': f (n' `zeroDiff` d) where f (Right _) = [] f (Left j) = j: f (j `zeroDiff` d) -- increasing sequence Right d -> n: iterate (d +) n' enumFromThenTo n n' m = case n `zeroDiff` n' of -- [n, n' .. m] -- constant sequence Left Zero -> n: repeat n' -- decreasing sequence Left d -> case m `compare` n of EQ -> [n] GT -> [] LT -> n: f (n' `zeroDiff` m) n' where -- n' >= m ? n'-m = (-(m-n)) - (n-n'), if n,m < inf f (Right _) _ = [] f (Left j) l = l: f (j `zeroDiff` d) (l - d) -- increasing sequence Right d -> case m `infDiff` n of Right _ -> [] Left k -> n: f (k `infDiff` d) n' where f (Right _) _ = [] f (Left j) l = l: f (j `infDiff` d) (d + l) fromEnum n = f 0 n where f i Zero = i f i (Succ m) = i' `seq` f i' m where i' = i+1 f _ Inf = error "Number.Peano.Inf: fromEnum infinity." instance Real Nat where toRational n = toRational (fromIntegral n :: Integer) instance Integral Nat where toInteger n = case toInteger' n of Just i -> i Nothing -> error "Number.Peano.Inf: toInteger infinity." quotRem _ _ = error "Number.Peano.Inf: quotRem not implemented." instance Bounded Nat where minBound = Zero maxBound = Inf