The bottom line: Equational reasoning in a typed language needs to
take account of types.
For those who would like me to go into a little more detail:
Warren has described a puzzling situation in which the two similarly
defined functions:
> f1 x y = const (show x == show y) w
> where
> w = x ++ y ++ ""
> f2 x y = const (show x == show y) w
> where
> w = (x ++ [5], y ++ "")
give different results, f1 [] [] = True, f2 [] [] = False. What is
really puzzling is that it doesn't look as though the results of each
function should depend on the definition of w, which is the only thing
that varies between the two definitions ... ?
The trick is that, although the value of w is not actually used in the
result of either function, the two different definitions do have a
significant effect on the types of the two functions:
f1 :: [Char] -> [Char] -> Bool
f2 :: [Int] -> [Char] -> Bool
Now it should be obvious that the two functions are not equivalent; they
don't even have the same type. The reason that they actually give
different results is because, as a special case, the empty string is
`show'n as "", while the empty list of integers (as any other empty list)
is `show'n as []. A similar effect could have been achieved by using
explicit type declarations:
> f1 :: [Char] -> [Char] -> Bool
> f1 x y = show x == show y
> f2 :: [Int] -> [Char] -> Bool
> f2 x y = show x == show y
The moral of the story seems to be that, if you are doing equational
reasoning in a typed language, then you really need to take account of
the types. This is particularly true when overloading is involved, but
it is still necessary even if we're restricted to pure polymorphism.
For example, I doubt that very many people would be happy with a proof
that used the law:
tail [1] = [] = tail "1".
In other words, when we write e1 = e2, we really want to be sure that
e1 and e2 have the same type. Likewise, when we write a law like:
map id = id,
we really ought to acknowledge that the two identity functions used here
are not the same; if the one on the left has type a -> a, then the one on
the right has type [a] -> [a].
Come to think of it, this argument makes me feel somewhat happier about
the fact that a Haskell type system will reject an expression like []==[].
After all, if we write [] = [] without saying what the types of each side
is supposed to be, then we have no way of knowing whether the equation even
makes sense. (Of course, Haskell's reasons for complaining about []==[]
are a little different, and I wasn't really that unhappy about it in the
first place ... never mind!)
All the best,
Mark
