John Launchbury writes:
Greg argument's about function denotations is valid up to a point. However,
when optimising functional programs we rely on *denotational* equivalence
to justify substitution, not just beta equivalence. So for example, we
can prove that
foldr (:) [] = id :: [a]->[a]
in the sense that given any input, they both produce the same output. This
form of equality is called *extensionality* and we make use of such facts
very frequently when deriving programs, or when proving them correct. Note
that neither side reduces to the other.
Fine; I *think* I understand this.
Thus, if we provided a function
showFun :: (Int->Int) -> String
say, that returned a string representing the function then any denotational
equivalence based on extensionality goes out the window.
In the absence of a rule or law that states:
f == g ==> showFun F == showFun g
this is not true; however, given that the above is simply Liebniz,
this seems a rather nasty choice! Is there any saving grace in
refusing to define an instance for class Eq for functions? The first
clause of the above cannot be written in Haskell; however, it can be
written in the meta notation if we hope to reason about correctness at
all.
How about another version of showFun:
showFun :: String -> (Int -> Int) -> String
where the first argument is the function name (as a string)? The idea
here is to make sure the distinction between the function definitions
gets into the function call. A logical patch, even a kludge, but one
that might not be too unpalatable.
Since, in response to Greg's question:
If we can establish that printable function representations are not
heretical :-) would other people find them useful?
I must give an unqualified "Yes!". We have analog and microwave
electronics applications that require some symbolic manipulation of
functions (boolean expressions, i.e. equations) written in Haskell
(well, in MHDL actually; take them as the same for this argument).
Doing this in Haskell itself requires some form of showFun function,
so I have been thinking about this a lot.
Dave Barton
[EMAIL PROTECTED]
