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. > > > > 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
