Re: [Haskell-cafe] Re: Haskell serialisation, was: To yi or not to yi...
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...
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...
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...
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...
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