Re: [Haskell-cafe] Functional progr., images, laziness and all therest

On Jun 22, 2006, at 10:16 AM, Brian Hulley wrote:

minh thu wrote:

...

2006/6/22, Brian Hulley :

...

Jerzy Karczmarczuk wrote:

...

Brian Hulley wrote: [snip] y IS NOT a longer list than yq, since co-recursive equations without limiting cases, apply only to *infinite* streams. Obviously, the consumer of such a stream will generate a finite segment only, but it is his/her/its problem, not that of the producer. I still don't understand this point, since y = (a*x0 : yq) so surely by induction on the length of yq, y has 1 more element? y and yq are infinite...

But how does this change the fact that y still has 1 more element than yq? yq is after all, not a circular list. I don't see why induction can't just be applied infinitely to prove this.

Induction doesn't apply to co-inductive objects, such as infinite lists AKA streams. I particular, the "length" of an infinite list is undefined, much as the "size" of an infinite set is undefined. The only think you can discuss, a la Cantor, is cardinality. In both cases, as mentioned by another poster, it is aleph-null. <aside> Every few months a discussion arises about induction and Haskell datatypes, and I feel compelled to trot out this oft-misunderstood fact about Haskell: 'data' declarations in Haskell introduce co- inductive definitions, NOT inductive ones. Induction, in general, does not apply to ADTs defined in Haskell; this is in contrast to similar-looking definitions in, eg, ML. This is a common source of confusion, especially for mathematically-inclined persons new to Haskell. Does anyone know of a good reference which clearly explains the difference and its ramifications? I've never been able to find a paper on the topic that doesn't dive head-first into complicated category theory (which I usually can't follow) ... </aside> Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG