Number.Peano.Inf

Lazy Peano numbers including observable infinity value.

Several lazyness properties:

• n + undefined >= n, if n = 0, 1, 2, ...

but undefined + n >= 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.

Documentation

data Nat

Natural numbers and infinity.

Instances

Bounded Nat

Enum Nat

Eq Nat

Integral Nat

Num Nat

Ord Nat

Real Nat

Show Nat

infinity :: Nat

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

inductive_infinity :: Nat

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.

diff

Arguments

:: Nat

n

-> Nat

m

-> Either Nat Nat

n >= m: Left (n-m), n < m: Right (m-n)

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

zeroDiff

Arguments

:: Nat

n

-> Nat

m

-> Either Nat Nat

n >= m: Left (n-m), n < m: Right (m-n)

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.

infDiff

Arguments

:: Nat

n

-> Nat

m

-> Either Nat Nat

n >= m: Left (n-m), n < m: Right (m-n)

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.

(-|) :: Nat -> Nat -> Nat

Non-negative subtraction. For example, (5 -| 8 == 0).