[Haskell-cafe] Serialization of (a -> b) and IO a
dan.doel at gmail.com
Thu Nov 11 05:34:59 EST 2010
On Thursday 11 November 2010 4:25:46 am Thomas Davie wrote:
> I don't think I agree, I didn't see a rule f == g => serialise f ==
> serialise g anywhere.
That equal things can be substituted for one another is one of the fundamental
ideas of equality (the other is that anything is equal to itself). In fact, in
second order logic, equality can be *defined* as (roughly):
(x = y) means (forall P. P x -> P y)
That is, x is equal to y if all predicates satisfied by x are also satisfied
by y. Using this, one can derive other typical laws for equality. Transitivity
is pretty easy, but surprisingly, even symmetry can be gotten:
If P z is z = x, using substitution we get x = x -> y = x,
and x = x is trivially true.
And of course, we also get congruence:
Given a function f, let P z be f x = f z,
substitution yields f x = f x -> f x = f y,
where f x = f x is again trivial.
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
\x -> x + x
\x -> 2 * x
So, for all this to work out, serialize must produce the same String for both
of those. But in general, it isn't possible to decide if two functions are
point-wise equal, let alone select a canonical representative for each
equivalence class of expressions that denote a particular function. So there's
no feasible way to implement serialize without breaking Haskell's semantics.
How making serialize :: (Integer -> Integer) -> IO String solves this? Well,
that's another story.
More information about the Haskell-Cafe