# 懒惰的自然数 Lazy natural numbers

## 激励性的例子 Motivating example​

checkLengthBiggerThan :: [a] -> Int -> Bool
checkLengthBiggerThan xs n = length xs > n

Examples:

*Main> :set +s
*Main> checkLengthBiggerThan [1..10^6] 3
True
(0.04 secs, 72,067,432 bytes)
*Main> checkLengthBiggerThan [1..10^7] 3
True
(0.19 secs, 720,067,488 bytes)
*Main> checkLengthBiggerThan [1..10^8] 3
True
(1.47 secs, 7,200,067,600 bytes)
*Main> checkLengthBiggerThan [1..10^9] 3
True
(14.35 secs, 72,000,067,640 bytes)

checkLengthBiggerThan' :: [a] -> Int -> Bool
checkLengthBiggerThan' [] 0 = False
checkLengthBiggerThan' xs 0 = True
checkLengthBiggerThan' [] n = False
checkLengthBiggerThan' (x:xs) n = checkLengthBiggerThan' xs (n-1)

Example:

*Main> checkLengthBiggerThan' [1..10^9] 3
True
(0.01 secs, 68,408 bytes)

## 懒惰的自然数 Lazy natural numbers​

data Nat = Zero | Succ Nat deriving (Eq,Ord)

Zero
Succ Zero
Succ (Succ Zero)
Succ (Succ (Succ Zero))
...

one, two, three :: Nat
one = Succ Zero
two = Succ one
three = Succ two

toNat :: Int -> Nat
toNat 0 = Zero
toNat n = Succ (toNat (n-1))

infty = Succ infty

length' :: [a] -> Nat
length' [] = Zero
length' (x:xs) = Succ (length' xs)

For example, we have that

• length [0..] loops without giving any answer, but
• length' [0..] = infty.

biggerThan :: Nat -> Nat -> Bool
Zero biggerThan y = False
(Succ x) biggerThan Zero = True
(Succ x) biggerThan (Succ y) = x biggerThan y

*Main> infty biggerThan three
True

checkLengthBiggerThan'' :: [a] -> Int -> Bool
checkLengthBiggerThan'' xs n = (length' xs) biggerThan (toNat n)

For example:

*Main> checkLengthBiggerThan'' [1..10^9] 3
True
(0.02 secs, 69,032 bytes)

checkLengthBiggerThan''' :: [a] -> Int -> Bool
checkLengthBiggerThan''' xs n = length' xs > toNat n

*Main> checkLengthBiggerThan''' [1..10^9] 3
True
(0.01 secs, 70,200 bytes)