On Thu, Nov 11, 2010 at 12:22 PM, Sjoerd Visscher
The equality that people typically expect to hold for Haskell expressions is that two such expressions are equal if they denote the same thing, as Max said. Expressions with function type denote mathematical functions, and so if we have something like:
serialize :: (Integer -> Integer) -> String
it must be a mathematical function. Further, its arguments will denote functions, to, and equality on mathematical functions can be given point-wise:
f = g iff forall x. f x = g x
Now, here are two expressions with type (Integer -> Integer) that denote equal functions:
\x -> x + x \x -> 2 * x
So, for all this to work out, serialize must produce the same String for both of those.
What I'm wondering is if it would actually break things if serialize would not produce the same String for these functions. The reasoning above is used regularly to shoot down some really useful functionality. So what would go wrong if we chose to take the practical path, and leave aside the theoretical issues?
Yeah, my sense -- but correct my if I'm reading the original post incorrectly -- is that the whole thing with function equality is a distraction and not really relevant here. It is true that (a) per Luke Palmer, if we could serialize equal functions to equal representations then we could we could decide whether two pure functions were equal, which (if not done in the IO monad) would(?) break purity; and (b) per Dan Doel, if we wanted to implement our serialization in a way so that equal functions get equal representations, we couldn't do it, because it's an impossible problem. But these sort of cancel each other out, because (a) it's an impossible problem, and (b) we don't want to do it. A function which does "x+x" would simply be serialized as doing x+x, and a function which does "x*2" would be serialized as doing x*2, and when deserialized the resulting functions would continue to do those things, and it would be completely agnostic and indifferent as to whether or not they are in fact equal. Obviously there are questions here with regards to the functions which the to-be-serialized function makes use of -- should they be serialized along with it? Required to be present when it is deserialized? Is it OK for the function to do something different when it is loaded compared to when it was stored if its environment is different, or not OK?
Also, the above two functions might not be exactly denotationally equal if the type is (Float -> Float), or the speed or memory use might be different. Could it not be that requiring them to be equal could just as well break things?
greetings, Sjoerd Visscher
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Work is punishment for failing to procrastinate effectively.