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