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 <[EMAIL PROTECTED]> | "In this house, we obey the laws <http://www.eyrie.org/~zednenem> | of thermodynamics!" _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe