peano-inf-0.4: Lazy Peano numbers including observable infinity value.

Portability portable experimental divip@aszt.inf.elte.hu

Number.Peano.Inf

Description

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

Synopsis

# Documentation

data Nat Source

Natural numbers and infinity.

Instances

 Bounded Nat Enum Nat Eq Nat Integral Nat Num Nat Ord Nat Real Nat Show 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`

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

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`

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

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 -> NatSource

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