diff --git a/Number/Peano/Inf.hs b/Number/Peano/Inf.hs --- a/Number/Peano/Inf.hs +++ b/Number/Peano/Inf.hs @@ -6,37 +6,9 @@ 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: +Properties of @Num@ can be found in the source of 'Number.Peano.Inf.Test'. -* @1 + a > a@, because @1 + infinity == infinity@. +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 @@ -47,10 +19,10 @@ , zeroDiff , infDiff , (-|) - , minimum' ) where -import Data.Ratio ((%)) +import Test.LazySmallCheck (Serial(..), cons0, cons1, (\/)) + {- Implementation Notes @@ -61,6 +33,8 @@ > 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 @@ -80,38 +54,12 @@ | Succ Nat | Inf -{- | -Observable infinity value. +instance Serial Nat where + series = cons0 Zero \/ cons1 Succ \/ cons0 Inf -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@. +{- | +Observable infinity value. -} infinity :: Nat infinity = Inf @@ -286,9 +234,10 @@ Succ n + m = Succ (n + m) Inf + _ = Inf - Succ n * m = m + n * m - Zero * _ = Zero - 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 @@ -378,7 +327,7 @@ instance Real Nat where - toRational n = fromIntegral n % 1 + toRational n = toRational (fromIntegral n :: Integer) instance Integral Nat where @@ -392,13 +341,6 @@ minBound = Zero maxBound = Inf - -{- | -Minimum of the list elements. -Works also for empty lists. --} -minimum' :: [Nat] -> Nat -minimum' = foldr min infinity diff --git a/Number/Peano/Inf/Functions.hs b/Number/Peano/Inf/Functions.hs new file mode 100644 --- /dev/null +++ b/Number/Peano/Inf/Functions.hs @@ -0,0 +1,33 @@ +module Number.Peano.Inf.Functions + ( minimum + , maximum + , length + ) where + +import Number.Peano.Inf + +import qualified Prelude as P +import Prelude hiding (minimum, maximum, length) + +{- | +Minimum of the list elements. +Works also for empty lists. +-} +minimum :: [Nat] -> Nat +minimum = foldr min infinity + + +{- | +Maximum of the list elements. +Works also for empty lists. +-} +maximum :: [Nat] -> Nat +maximum = foldr max 0 + +length :: [a] -> Nat +length [] = 0 +length (_:t) = succ (length t) + + + + diff --git a/Number/Peano/Inf/Test.hs b/Number/Peano/Inf/Test.hs new file mode 100644 --- /dev/null +++ b/Number/Peano/Inf/Test.hs @@ -0,0 +1,84 @@ + +{-# LANGUAGE ScopedTypeVariables #-} + +module Number.Peano.Inf.Test + ( test + ) where + +import Number.Peano.Inf + +import Test.LazySmallCheck hiding (test) + +default (Nat) + +test :: IO () +test = do + +-- Several lazyness properties + + smallCheck 10 $ + + undefined >= (0::Nat) + + smallCheck 10 $ \(n::Nat) -> and + + [ n + undefined >= n -- but @undefined + n@ raises an error. + + , n /= infinity ==> (1 + n + undefined) `compare` n == GT -- but @compare (n + undefined) n@ raises an error. + + , n `min` (n + undefined) == n + + , (1 + n + undefined) `min` n == n -- but @min (n + undefined) n@ raises an error. + ] + + smallCheck 10 $ \(m::Nat) (n::Nat) -> and + + [ (m + n) `min` (m + undefined) >= m + + , (m + undefined) `min` (m + n) >= m + + , n `max` (m + undefined) >= m + + , (m + undefined) `max` n >= m + + ] + +-- Properties of infinity + + smallCheck 10 $ and + + [ infinity == infinity + + , 0 * infinity == 0 + + , infinity * 0 == 0 + + ] + + smallCheck 10 $ \(n::Nat) -> and + + [ n /= infinity ==> n < infinity + + , n + infinity == infinity + + , infinity + n == infinity + + , n /= 0 ==> n * infinity == infinity + + , n /= 0 ==> infinity * n == infinity + + , n /= infinity ==> infinity - n == infinity + + ] + + +{- +The following values raise error messages: + +* @infinity - infinity@, + +* @fromEnum infinity@, + +* @toInteger infinity@. +-} + diff --git a/peano-inf.cabal b/peano-inf.cabal --- a/peano-inf.cabal +++ b/peano-inf.cabal @@ -1,5 +1,5 @@ name: peano-inf -version: 0.5 +version: 0.6 synopsis: Lazy Peano numbers including observable infinity value. description: Lazy Peano numbers including observable infinity value. @@ -21,9 +21,12 @@ library ghc-options: -Wall -fno-warn-overlapping-patterns -fno-warn-incomplete-patterns build-depends: - base + base, + lazysmallcheck exposed-modules: - Number.Peano.Inf + Number.Peano.Inf, + Number.Peano.Inf.Test, + Number.Peano.Inf.Functions