Daniel Fischer writes:
Due to lazyness, we can have infinite lists (and other infinite structures) in Haskell (of course, in finite time, only a finite portion of those can be evaluated), e.g. ns = [1 .. ] :: [Integer] is an infinite list which is often used. And now consider the property P that there exists a natural number n so that the list l has length n.
Obviously P holds for all finite lists, but not for the infinite list ns.
You can avoid some problems like that by using lazy naturals, e.g.:
data Nat = Zero | Succ Nat
instance Eq Nat where m == n = compare m n == EQ
instance Ord Nat where
compare Zero Zero = EQ
compare Zero (Succ _) = LT
compare (Succ _) Zero = GT
compare (Succ m) (Succ n) = compare m n
infinity = Succ infinity
length [] = Zero
length (x:xs) = Succ (length xs)
Everything terminates, as long as you don't try to compare two infinite
values.
--
David Menendez