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

[robert dockins]

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