[Haskell-cafe] Re: Proving stuff about IORefs

[Ben Franksen]

Derek Elkins wrote:
> On Sun, Oct 17, 2010 at 6:49 AM, Miguel Mitrofanov
> <miguelimo38 at yandex.ru> wrote:
>>
>> On 17 Oct 2010, at 05:21, Ben Franksen wrote:
>>
>>> I want to prove that
>>>
>>> f r == do
>>> s1 <- readIORef r
>>> r' <- newIORef s1
>>> x <- f r'
>>> s3 <- readIORef r'
>>> writeIORef r s3
>>> return x
>>
>> That is not true. Consider the following function:
>>
>> g r1 r2 = writeIORef r1 0 >> writeIORef r2 1 >> readIORef r1
>>
>> This function behaves differently depending on whether r1 and r2 are the
>> same IORef or not. Therefore, the property you want to prove doesn't hold
>> for the partially-applied function
>>
>> f = g r1
> 
> I originally was thinking along these lines, and this is an important
> case, but there is an even more trivial example.
> 
> Let f be return.

Oh, my god. Of course.

Thanks for pointing me to the obvious ;-)

This means I either have to give up on the second law

  callback . embed  =  id

or find another implementation. Maybe IORef is too powerful. Hmm.

The second law was inspired by the instance for ReaderT:

  instance Embed m (ReaderT r m) where
    type Content m (ReaderT r m) = r
    embed = ReaderT
    callback = runReaderT

which is much more general (it does not depend on the inner monad being IO),
and where indeed the second law holds.

Cheers
Ben