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.
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. A big loss, to put
it mildly! The problem is that the string is then available for use by the
rest of the program.
On the other hand, if we provided a system call (a request or whatever)
of the form
data Request = ...
| ShowFun (Int->Int)
then any problems become much more contained, as it is only the *external
world* that would witness non-extensionality.
John.
