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

[Robert Dockins]

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

> minh thu wrote:
>> 2006/6/22, Brian Hulley <brianh at metamilk.com>:
>>> 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