[Haskell-cafe] Clarification on proof section of HS: The Craft of
FP
Daniel Fischer
daniel.is.fischer at web.de
Mon May 2 10:51:40 EDT 2005
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
More information about the Haskell-Cafe
mailing list