[Haskell-cafe] Re: Asynchronous exception wormholes kill modularity

[Simon Marlow]

On 21/04/2010 19:38, Bas van Dijk wrote:
> On Tue, Apr 20, 2010 at 12:56 PM, Simon Marlow<marlowsd at gmail.com>  wrote:
>> On 09/04/2010 12:14, Bertram Felgenhauer wrote:
>>> It could be baked into a variant of the forkIO primitive, say
>>>
>>>      forkIOwithUnblock :: ((IO a ->    IO a) ->    IO b) ->    IO ThreadId
>>
>> I agree with the argument here.  However, forkIOWithUnblock reintroduces the
>> "wormhole", which is bad.
>>
>> The existing System.Timeout.timeout does it the other way around: the forked
>> thread sleeps and then sends an exception to the main thread. This version
>> work if exceptions are masked, regardless of whether we have
>> forkIOWithUnblock.
>>
>> Arguably the fact that System.Timeout.timeout uses an exception is a visible
>> part of its implementation: the caller must be prepared for this, so it is
>> not unreasonable for the caller to also ensure that exceptions are unmasked.
>>   But it does mean that a library cannot use System.Timeout.timeout invisibly
>> as part of its implementation.  If we had forkIOWithUnblock that would solve
>> this case too, as the library code can use a private thread in which
>> exceptions are unmasked.  This is quite a nice solution too, since a private
>> ThreadId is not visible to anyone else and hence cannot be the target of any
>> unexpected exceptions.
>>
>> So I think I'm convinced that forkIOWithUnblock is necessary.  It's a shame
>> that it can be misused, but I don't see a way to avoid that.
>>
>> Cheers,
>>         Simon
>>
>
> I can see how forkIOWithUnblock (or forkIOWithUnnmask) can introduce a wormhole:
>
> unmaskHack1 :: IO a ->  IO a
> unmaskHack1 m = do
>    mv<- newEmptyMVar
>    tid<- forkIOWithUnmask $ \unmask ->  putMVar mv unmask
>    unmask<- takeMVar mv
>    unmask m
>
> We can try to solve it using a trick similar to the ST monad:

Funnily enough, before posting the above message I followed exactly the 
line of reasoning you detail below to discover that there isn't a way to 
fix this using parametricity.  It's useful to have it documented, though 
- thanks.

Cheers,
	Simon



> {-# LANGUAGE Rank2Types #-}
>
> import qualified Control.Exception as Internal (unblock)
> import Control.Concurrent (forkIO, ThreadId)
> import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar)
>
> newtype Unmask s = Unmask (forall a. IO a ->  IO a)
>
> forkIOWithUnmask :: (forall s. Unmask s ->  IO ()) ->  IO ThreadId
> forkIOWithUnmask f = forkIO $ f $ Unmask Internal.unblock
>
> apply :: Unmask s ->  IO a ->  IO a
> apply (Unmask f) m = f m
>
> thisShouldWork = forkIOWithUnmask $ \unmask ->  apply unmask (return ())
>
> The following shouldn't work and doesn't because we get the following
> type error:
>
> "Inferred type is less polymorphic than expected. Quantified type
> variable `s' is mentioned in the environment."
>
> unmaskHack2 :: IO a ->  IO a
> unmaskHack2 m = do
>    mv<- newEmptyMVar
>    tid<- forkIOWithUnmask $ \unmask ->  putMVar mv unmask
>    unmask<- takeMVar mv
>    apply unmask m
>
> However we can still hack the system by not returning the 'Unmask s'
> but returning the IO computation 'apply unmask m' as in:
>
> unmaskHack3 :: IO a ->  IO a
> unmaskHack3 m = do
>    mv<- newEmptyMVar
>    tid<- forkIOWithUnmask $ \unmask ->  putMVar mv (apply unmask m)
>    unmaskedM<- takeMVar mv
>    unmaskedM -- (or use join)
>
> AFAIK the only way to solve the latter is to also parametrize IO with s:
>
> data IO s a = ...
>
> newtype Unmask s = Unmask (forall s2 a. IO s2 a ->  IO s2 a)
>
> forkIOWithUnmask :: (forall s. Unmask s ->  IO s ()) ->  IO s2 ThreadId
> forkIOWithUnmask f = forkIO $ f $ Unmask Internal.unblock
>
> apply :: Unmask s ->  IO s2 a ->  IO s a
> apply (Unmask f) m = f m
>
> With this unmaskHack3 will give the desired type error.
>
> Of course parameterizing IO with s is a radical change that will break
> _a lot of_ code. However besides solving the latter problem the extra
> s in IO also create new opportunities. Because all the advantages of
> ST can now also be applied to IO. For example we can have:
>
> scope :: (forall s. IO s a) ->  IO s2 a
>
> data LocalIORef s a
>
> newLocalIORef :: a ->  IO s (LocalIORef s a)
> readLocalIORef :: LocalIORef s a ->  IO s a
> writeLocalIORef :: LocalIORef s a ->  a ->  IO s a
>
> regards,
>
> Bas