Number.Peano.Inf

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.

Documentation

data Nat

Natural numbers and infinity.

Instances

Bounded Nat

Enum Nat

Eq Nat

Integral Nat

Num Nat

Ord Nat

Real Nat

Show Nat

Serial Nat

infinity :: Nat

Observable infinity value.

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:

• n < inductive_infinity, n = 0, 1, 2,...

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).