Compiler Proof of Referential Transparency

Programs in languages with mutation can make optimizations that Haskell programs can't, at least not without compiler magic, unsafePerformIO, or wrapping return types in the IO monad. Simple examples that spring to mind are memoization and splay trees. Here, operations that should have no semantic effects (calling a fib function or doing a find on a splay map) do have actual effects. It would be nice if Haskell programmers could write these optimizations and prove them safe with the type system, then use these functions as if they were referentially transparent.

My idea for this a few months ago was to use quotient types, since quotient types equate two actually different things that are functionally the same under some view. A Fibonacci function with a memoization table up to 100 looks the same to a caller as one with no memoized values at all, so they are equal under some quotient.

Other things came up, and I put off this idea for a while, and I have now seen a really cool way for Haskell programmers to deal with local effects. Ben Lippmeier's talk at the SAPLING June 2007 meeting (talk summary) explains region and effect inference for Haskell-like languages without sacrificing referential transparency or having to use the IO monad. This insight wouldn't solve the splay tree issue, because reading a splay tree does modify data that is not local to the reading function, though that modification should be opaque to clients.

I can't wait to see the full paper(s) and the implementation. Until I can, I'll have to settle for the slides from an earlier talk with more motivation.