[Haskell-cafe] Clarification on proof section of HS: The Craft of FP

[David Menendez]

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