>John, why does your argument not hold for INPUT function representations
>as well as OUTPUT function representations?
>
>Consider the "identity" interpreter:
>
> interpret program == program
> interpret : string -> string
>
>Presumably this preserves meaning. So why is it that the "lambda x.x" in the
>call:
>
> interpret "lambda x.x"
>
>is acceptable but the result:
>
> "lambda x.x"
>
>is not?
Indeed it is. If you start with function *representations*, and manipulate
them within the language as representations, then indeed you can safely
return a representation of the result. But it will still be a String (or
whatever). The one-sidedness comes from the fact that there are functions
eval :: String -> (Int -Int)
say, which behave as interpreters of representations, but there are no
(particularly interesting) function which go in the other direction
(i.e. from (Int->Int) -> String). Functions which produce representations
from real functions are worse than non-monotonic, they aren't even functions!!
All this is true in the lambda-calculus as well. If we write [E] for a
lambda expression which represents the lambda expression E (i.e. which
allows another lambda expression to examine E's internal structure)
then there exists a lambda expression M such that
M [E] = E
but there does NOT exist a lambda expression N such that
N E = [E]
Torben Mogensen's paper in JFP a while ago covers this very nicely.
>Are you saying that we can throw away implementations and just keep
>type checkers? The output from a program that returns a function is at best
>the type of that function so why bother evaluating the program at all if
>you've deduced that final type already?
A function can only be told by what it does, not by how it does it. Otherwise
extensional equality is lost.
John.
