Paul writes,
I think it's important to realize that laws aren't being entirely
lost -- they're just being weakened a (wee) bit, in the form of
carrying an extra constraint. For example, eta conversion:
\x -> f x = f
must simply be modified slightly:
\x -> f x = f if f /= _|_
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?
Cheers, -- P
