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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
