[Haskell-cafe] Re: Why purely in haskell?

[Jonathan Cast]

On 10 Jan 2008, at 7:55 AM, Achim Schneider wrote:

> "Daniel Yokomizo" <daniel.yokomizo at gmail.com> wrote:
>
>> On Jan 10, 2008 3:36 PM, Achim Schneider <barsoap at web.de> wrote:
>>> jerzy.karczmarczuk at info.unicaen.fr wrote:
>>>
>>>> Niko Korhonen writes:
>>>>
>>>> ...
>>>>> Although it could be argued that laziness is the cause of some
>>>>> very obscure bugs... <g>
>>>>> Niko
>>>>
>>>> Example, PLEASE.
>>>>
>>> [1..] == [1..]
>>>
>>> , for assumed operational semantics of ones own axiomatic semantics.
>>> Bugs are only a misunderstanding away.
>>
>> It has nothing to do with laziness, but with using an algebraic
>> function (==) with a codata structure (stream). If Haskell kept
>> laziness but enforced separation of data and codata such code  
>> wouldn't
>> compile. Lazy lists or streams never are a problem, but you can't
>> (generically) fold codata.
>>
> Exactly. Denotationally it hasn't, but axiomatically it has.  
> Because it
> looks like mathematical terms one can easily get lost in believing it
> reduces like mathematics, too.

What kind of mathematics?  I don't know of any mathematics where  
algebraic simplifications are employed without proof of the  
underlying equations (in some denotational model).

jcc