[Haskell-cafe] Re: Haskell serialisation, was: To yi or not to yi...

[Tom Schrijvers]

> Tom Schrijvers wrote:
>>> I understand that, depending on what the compiler does the result of :
>>>
>>> do
>>>    let  f = (*) 2
>>>    print $ serialise f
>>>
>>> might differ as, for example, the compiler might have rewritten f as
>>> \n ->
>>> n+n.
>>>
>>> But, why would that make equational reasoning on serialise not valid?
>>>
>>> Isn't that true for all functions in the IO monad that, even when
>>> invoked with the same arguments, they can produce different results?
>>
>> Not if you take the ``state of the world" to be part of the arguments.
>> If two programs behave differently for the same arguments and the same
>> state of the world, then they're not equivalent. You do want your
>> compiler to preserve equivalence, don't you?
>
> You can put the internal representation of the argument into the "state
> of the world".

That wouldn't make a difference. If, from the pure Haskell point of view 
we can't tell the difference between two expressions that denote the same 
function, then operations in the IO monad should not be able to do so 
either. Otherviews a whole lot of program transformations based on 
rewriting of expressions would be invalid. How do you account for that?

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be