[Haskell-cafe] Serialization of (a -> b) and IO a

[Dan Doel]

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 
functions:

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

-- Dan