Saturday, June 23, 2007

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.


Thomas Schilling said...

Do you happen to remember what the % $ ! -(..)> and other notation stands for? It seems kind of hard to infer from the slides only.

Jim Apple said...

I wasn't actually at the talk, so I don't know either.

Michael Stone said...

I wasn't at the talk either, but they appear to me to be sigils separating the namespaces of type-variables (), region-variables (%), closure-variables ($), and effect-variables (!), respectively.

It's difficult to tell from just the slides if they carry additional meaning.

Anyway, thanks for posting this, Jim!

Jim Apple said...

I've emailed Ben to ask for whatever details he has time to provide us.