peano-inf 0.3 → 0.4

raw patch · 2 files changed

+132/−17 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Number/Peano/Inf.hs +131/−16
• peano-inf.cabal +1/−1

@@ -6,34 +6,41 @@  Lazy Peano numbers including observable infinity value. -Note that the following equation does /not/ hold for this number type:+Several lazyness properties: -* @1 + a > a@,  because @1 + infinity == infinity@.+* @n + undefined >= n@, if @n@ = 0, 1, 2, ... -The following operation is undefined:+but @undefined + n >= n@ raises an error. -* @infinity - infinity@+* @compare (n + undefined) (n-1) == GT@, if @n@ = 0, 1, 2, ... -There are variants of @(-)@ with different behaviour regarding this, see below.+but @compare (n + undefined) n@ raises an error. -The following operations are naturally undefined:+* @min n (n + undefined)@ results @n@, if @n@ = 0, 1, 2, ... -* @fromEnum infinity@+* @min (n + undefined) (n - 1)@ results @n - 1@, if @n@ = 0, 1, 2, ... -* @toInteger infinity@+but @min (n + undefined) n@ raises an error. -* @0 - n@, if @n > 0@+* @min n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @min 10 (5 + undefined) >= 5@. -* @fromInteger n@, if @n < 0@+* @min (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ... -* @toEnum n@, if @n < 0@+* @max n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @max 10 (5 + undefined) >= 5@. -* @pred 0@+* @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@@ -41,19 +48,90 @@     ) 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.+{- | +Observable infinity value. +The following values are @True@:++* @infinity == infinity@++* @0 < infinity@, @1 < infinity@, @2 < infinity@, ...++* @n + infinity == infinity@,  if @n@ is not the inductive infinity.++* @infinity + n == infinity@++* @n * infinity == infinity@,  if @n@ is not the inductive infinity.++* @infinity * n == infinity@++* @n - infinity == 0@,  if @n@ is not the inductive infinity.++* @infinity - n == infinity@,  if @n@ is not the inductive infinity and if @n /= infinity@.++The following values rais 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@:++* @0 < inductive_infinity@, @1 < inductive_infinity@, @2 < inductive_infinity@, ...++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@@ -112,7 +190,15 @@         Just i  -> show i         Nothing -> "infinity" --- | Difference of two natural numbers: the result is either positive or negative.+{- | +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@@ -126,7 +212,17 @@ Succ n `diff` Inf    = n `diff` Inf  --- | Variant of @diff@: @infDiff infinity infinity  ==  Left infinity@.+{- | +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@@ -139,7 +235,17 @@ Zero   `infDiff` m      = Right m  --- | Variant of @diff@: @zeroDiff infinity infinity  ==  Left 0@.+{- | +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@@ -198,6 +304,15 @@      enumFrom n = enumFromTo n Inf +    {- |+            @[inf.. inf] == [inf, inf, inf, ..@++        instead of ++            @[inf.. inf] == [inf]@++        Both are reasonable but the second solution would make @enumfrom@ much more eager.+    -}     enumFromTo n m = case m `infDiff` n of          Right _ -> []

@@ -1,5 +1,5 @@ name:           peano-inf-version:        0.3+version:        0.4 synopsis:       Lazy Peano numbers including observable infinity value. description:         Lazy Peano numbers including observable infinity value.