[Haskell-cafe] Clarification on proof section of HS: The Craft of
FP
David Menendez
zednenem at psualum.com
Mon May 2 21:48:48 EDT 2005
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!"
More information about the Haskell-Cafe
mailing list