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

2007-06-21 Thread 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: [EMAIL PROTECTED]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


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

2007-06-21 Thread Neil Davies

Ah -

   The "state of the world" serialized into your representation.

That would be interesting to see

Neil

... ah you meant something different?

On 21/06/07, apfelmus <[EMAIL PROTECTED]> wrote:

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".

Regards,
apfelmus

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


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

2007-06-21 Thread Jon Cast
On Thursday 21 June 2007, Tom Schrijvers wrote:
> 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.

This doesn't make any sense to me.  IO is a non-determinism monad (among many 
other things).  That's already true --- randomIO is one example; 
Control.Exception.evaluate is another (and is already dependent on the 
particular compilation choices made).  I think of Haskell `values' as sets of 
legal representations anyway --- why shouldn't serialize be free to make a 
non-deterministic choice from among those sets, just like evaluate can make a 
non-deterministic choice from the set of exceptions an expression can throw?

Sincerely,
Jonathan Cast
Computer Programmer
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


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

2007-06-21 Thread Tom Schrijvers



On Thursday 21 June 2007, Tom Schrijvers wrote:

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.


This doesn't make any sense to me.  IO is a non-determinism monad (among many
other things).  That's already true --- randomIO is one example;
Control.Exception.evaluate is another (and is already dependent on the
particular compilation choices made).  I think of Haskell `values' as sets of
legal representations anyway --- why shouldn't serialize be free to make a
non-deterministic choice from among those sets, just like evaluate can make a
non-deterministic choice from the set of exceptions an expression can throw?


Good point. I agree, if the specification is non-deterministic, this 
should be alright.


Tom

--
Tom Schrijvers

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

tel: +32 16 327544
e-mail: [EMAIL PROTECTED]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


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

2007-06-21 Thread Brandon Michael Moore
On Thu, Jun 21, 2007 at 04:37:20PM +0200, Tom Schrijvers wrote:
> 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?

In the same way we don't mind if "const getChar" can "tell a difference"
between the value () (and itself). Also think of imprecise exceptions -
really the pure code hitting the exception does all the usual stuff with
stack walking, but semantically the pure expression evaluates to a set
of exception, catch makes a nondeterministic choice of which one to handle,
and it just happens that catch always picks the one that you run into first
given the evaluation order that happend in this particular execution.

I think it would be safe to treat serialize the same way.

Brandon
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe