Friday, July 20, 2007

More Proof of Referential Transparency

Previously, I talked about proving referential transparency. The authors of A Persistent Union-Find Data Structure (other version) use Coq to prove imperative functions referentially transparent, and they point out the work of Harold Baker, who designed fast persistent arrays (and here), which they also prove to be referentially transparent. These arrays are even available in Haskell, though wrapped in the IO monad.

The authors of the union-find paper say that their structure is not "purely applicative". I don't actually know what that means, but I suppose it means it's not strictly functional, since it requires in-place modification.

In any case, there are now at least four cases for being able to prove referential transparency so we can use it without wrapping everything in the IO monad:

Any other ideas?

No comments: