On 5/2/05, Daniel Fischer
Am Montag, 2. Mai 2005 16:16 schrieb Daniel Carrera:
Henning Thielemann wrote:
Well, I also omited the word "countable". I figure it's understood since computers only deal with finite data. And given an infinite list, any finite "head" of it would meet the criteria, so the distinction is moot. Unless Haskell has some neat property I am not aware of :-)
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.
This property clearly violates the assumption for mathematical induction that if P(x) is true for all x < y, then P(y) is true.
If you don't take care you may end up "proving" that e.g. repeat 1 ++ [0] == repeat 0 because for the first list you can prove that every reachable element is equal to its neighbour and the "last" element is 0.
Note: I'm totally new at Haskell.
What does ++ do?
append two lists: [1,2] ++ [3,4] == [1,2,3,4]
What does 'repeat' do?
create an infinite list with one distinct element:
repeat 1 = [1,1,1,1,1,1,1, ... ad infinitum
Cheers, Daniel.
ditto
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe