
On Mar 11, 2011, at 7:37 PM, Luke Palmer wrote:
On Fri, Mar 11, 2011 at 8:18 PM, Joshua Ball
wrote: Suppose I want the following functions:
newRef :: a -> RefMonad (Ref a) readRef :: Ref a -> RefMonad a writeRef :: Ref a -> a -> RefMonad ()
I would be delighted to see a pure, unsafe*-free implementation of your interface. I have never seen one, and I don't really expect it to exist. Likewise I would love to see a proof that it doesn't.
This message from Koen Claessen, dating back to 2001, discusses precisely this issue: http://www.mail-archive.com/haskell@haskell.org/msg09207.html Quoting Koen: "I conjecture this functionality cannot be implemented in Haskell 98, nor in any of the known safe extensions of Haskell." I think the folk consensus in the community is that Koen was right. While a proof along the lines of "doing so would violate parametricity" seems plausible, I can't recall anybody attempting a rigorous proof so far. -Levent.