I have not made such a claim.

]]>Thanks for an interesting post! I find this is a very interesting question, for the following reason. If you consider the linear lambda calculus, then there’s no question about implementing it efficiently, because the linear use criterion means that you can always safely do destructive updates. It’s only at exponential types !A that destructive updates become unsafe. In other words, update becomes unsafe once we permit sharing or reuse of values.

That’s well-known, almost a commonplace, but now consider the flip side: efficient algorithms go out of their way to avoid re-doing work, and one of the most important mechanisms for doing this — is sharing! For example, compiler optimizations often work with truly hairy graph representations to turn naively cubic algorithms into n-log-n ones. And of course you pointed out union-find, which is the queen of algorithms that exploit sharing.

So in a vague, handwavy way it seems like you get a choice of two ways to use sharing, but you can’t (easily?) use both at once. It would be incredibly cool to learn of some nice logical explanations of this tradeoff. Perhaps the work on light affine logic has something to say here?

]]>