[Haskell-cafe] Serialization of (a -> b) and IO a
Sjoerd Visscher
sjoerd at w3future.com
Thu Nov 11 06:22:06 EST 2010
> 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?
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
More information about the Haskell-Cafe
mailing list