| You're not using "equational reasoning" here - equational reasoning
| has nothing to say on the subject of caching results for later use so
| you can't use it to argue about whether or not caching is happening.
If you're going to quibble, then I have to contradict you and repeat
that I *was* using equational reasoning. But I was using it to explain
why the expression concerned could be expected to expand to something
much larger, not to reason about caching. After all, in a lazy language,
all evaluation is supposed to be cached: don't evaluate unless you have
to, but cache the results when you do.
But I'm not really interested in quibbling with your quibbles. I'm
responding to your message now because it actually helps to make the
point I was trying to make earlier much clearer. The kind of thing
that you are proposing is, in certain places, to break the property I
mentioned above that "all evaluation is supposed to be cached". Your
motivation is pragmatic, and makes a lot of sense in the case of
compiled code. For example, you don't want to cache evaluation of
"main" if "main" does not involve recursive calls to itself, because
you can be sure that the cached value will not (indeed, cannot) be
used. In an interpreter, however, you can't make those same guarantees
because you can't tell what the user will type next.
You could change the semantics of the interpreter's read-eval-print
loop so that every expression is evaluated as if it were a program
starting from scratch. It would clearly be useful to have a system
that worked that way. My concern however is that the current semantics,
which is entirely consistent with lazy evaluation, also has useful
applications and shouldn't be lost. We need both, perhaps with a
command line argument to select between them.
| If you were using equational reasoning, you'd probably have used "=="
| or "=" instead of "===>" in the above reduction sequence.
I used "===>" to indicate either reduction or rewriting, and all
properties obtained in this way are also equalities, by definition.
So I could have written "=", but I thought the extra information
carried by the "===>" notation might be useful. Pardon me for
being more precise that necessary!
All the best,
Mark
