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

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

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