Indeed. Notice that there is a similar difference between call-by-need
and call-by-value beta:
(\x -> u) t = u[t/x] call-by-need
(\x -> u) t = u[t/x] if t /= _|_ call-by-value
But here we seem to think the difference is important. So why is
it important for beta, but unimportant for eta? Or are we deluding
ourselves in thinking it is important?
Well, I think we all agree that it's IMPORTANT. It's just that
up until now we have always said that we NEVER wanted to clutter
up the reasoning with the extra constraint. But now some of us are
saying that there are occasions when we're willing to (I say
"occasions" because the default is still non-strict, reflecting
our original desires). Stefan's recent example is a good one that
I hadn't thought of before.
And again I point out that despite our original intents, we still
need to reason about _|_'s -- in pattern-matching, for example --
and "strictness bugs" have become infamous (:-)!
-Paul
