Portability  portable 

Stability  experimental 
Maintainer  divip@aszt.inf.elte.hu 
Lazy Peano numbers including observable infinity value.
Several lazyness properties:

n + undefined >= n
, ifn
= 0, 1, 2, ...
but undefined + n >= n
raises an error.

compare (n + undefined) (n1) == GT
, ifn
= 0, 1, 2, ...
but compare (n + undefined) n
raises an error.

min n (n + undefined)
resultsn
, ifn
= 0, 1, 2, ... 
min (n + undefined) (n  1)
resultsn  1
, ifn
= 0, 1, 2, ...
but min (n + undefined) n
raises an error.

min n (m + undefined) >= m
, ifn
,m
= 0, 1, 2, ... For example,min 10 (5 + undefined) >= 5
. 
min (m + undefined) n >= m
, ifn
,m
= 0, 1, 2, ... 
max n (m + undefined) >= m
, ifn
,m
= 0, 1, 2, ... For example,max 10 (5 + undefined) >= 5
. 
max (m + undefined) n >= m
, ifn
,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
, because1 + infinity == infinity
.
Documentation
Natural numbers and infinity.
Observable infinity value.
The following values are True
:
infinity == infinity

0 < infinity
,1 < infinity
,2 < infinity
, ... 
n + infinity == infinity
, ifn
is not the inductive infinity. infinity + n == infinity

n * infinity == infinity
, ifn
is not the inductive infinity. infinity * n == infinity

n  infinity == 0
, ifn
is not the inductive infinity. 
infinity  n == infinity
, ifn
is not the inductive infinity and ifn /= infinity
.
The following values rais error messages:
infinity  infinity
fromEnum infinity
toInteger infinity
inductive_infinity :: NatSource
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 ofTrue
.
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 ofTrue
.
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
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
, becauseinfininty  (infinity  5) == 0 /= 5
.
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
, becauseinfininty  (infinity  5) == infinity /= 5
.