Could you expand on effects which preserve extensionality some more? I'm fairly sure I understand it, but I've never quite follows what Harper's "benign effects" meant in detail and I'd like to see how it all connects.
So extensionally equal simply means that there is a model with and without the effect such that extensionally, according to some model of observation, we cannot discern the existence of the effect?
I wasn't thinking about models, but perhaps you could? I just mean that you get the same results for equal inputs; laziness is fine in this respect (but not in the presence of some other effects).
