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?
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?
Greg
