peano-inf-0.5: Number/Peano/Inf.hs
{- |
Copyright : (c) Peter Divianszky 2008
Maintainer : divip@aszt.inf.elte.hu
Stability : experimental
Portability : portable
Lazy Peano numbers including observable infinity value.
Several lazyness properties:
* @undefined >= 0@,
* @n + undefined >= n@, if @n@ = 0, 1, 2, ...
but @undefined + n@ raises an error.
* @compare (n + undefined) (n-1) == GT@, if @n@ = 0, 1, 2, ...
but @compare (n + undefined) n@ raises an error.
* @min n (n + undefined)@ results @n@, if @n@ = 0, 1, 2, ...
* @min (n + undefined) (n - 1)@ results @n - 1@, if @n@ = 0, 1, 2, ...
but @min (n + undefined) n@ raises an error.
* @min n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @min 10 (5 + undefined) >= 5@.
* @min (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ...
* @max n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @max 10 (5 + undefined) >= 5@.
* @max (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ...
These properties makes the @Num@ data type ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@.
Note that the following equation does /not/ hold for this number type:
* @1 + a > a@, because @1 + infinity == infinity@.
-}
module Number.Peano.Inf
( Nat
, infinity
, inductive_infinity
, diff
, zeroDiff
, infDiff
, (-|)
, minimum'
) where
import Data.Ratio ((%))
{-
Implementation Notes
The observable infinity value has many representatives:
> Inf
> Succ Inf
> Succ (Succ Inf)
> ...
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
{- |
Observable infinity value.
The following values are @True@ for @n@ = 0, 1, 2,... :
* @infinity == infinity@,
* @n < infinity@,
* @n + infinity == infinity@,
* @infinity + infinity == infinity@,
* @infinity + n == infinity@,
* @n * infinity == infinity@,
* @infinity * n == infinity@,
* @infinity * infinity == infinity@,
* @n - infinity == 0@,
* @infinity - n == infinity@.
The following values raise error messages:
* @infinity - infinity@,
* @fromEnum infinity@,
* @toInteger infinity@.
-}
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
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 = fromIntegral n % 1
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
{- |
Minimum of the list elements.
Works also for empty lists.
-}
minimum' :: [Nat] -> Nat
minimum' = foldr min infinity