[Haskell-cafe] Clarification on proof section of HS: The Craft
of FP
robert dockins
robdockins at fastmail.fm
Mon May 2 11:24:00 EDT 2005
>>>>>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.
The problem here is that the haskell [] type is not actually an
inductive type, but a coinductive type (which means one can construct
infinite objects of that type). The proof tools available to work with
coinductive types differ somewhat from the tools used on inductive
types. In "Craft of FP", the author works with scheme, which has eager
evaluation and thus cannot construct objects with coinductive type: thus
the usual, familiar induction principles just work. Haskell has lazy
evaluation which allows the construction and manipulation of
coinductive-typed objects.
Short story: when working with finite objects, regular induction works.
When working with infinite objects, be careful and read up on coinduction.
More information about the Haskell-Cafe
mailing list