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 <zednenem@psualum.com> | "In this house, we obey the laws <http://www.eyrie.org/~zednenem> | of thermodynamics!"