Semantics of IORefs in GHC

Ben Lippmeier benl at
Mon Mar 14 13:38:47 UTC 2016

> On 14 Mar 2016, at 8:06 pm, Simon Peyton Jones <simonpj at> wrote:
> But my rough answer would be: IORefs are really only meant for single-threaded work.  Use STM for concurrent communication.

You can also use atomicModifyIORef for simple things. 

> Why can’t GHC tighten the semantics of IORefs so that the bind operation simply means sequential composition?

Part of the problem is that IO encomposes all sorts of computational effects, including ones that don’t have a well defined notion of time. File and network effects are also a problem, not just IORefs. The IO instance of bind composes two IO computations, but the computations themselves could do anything.

A first step is to split the IO type into more fine grained effects, perhaps ones that can be properly sequentialized and those which can’t (or should not be). Many people have done work on more expressive effect systems, though no system so far has been good enough to want to refactor the GHC base libraries using it.

On a more philosophical level, Haskell types are statements in a simple predicate logic which does not natively know anything about time. Functions don’t know about time either, so it’s a bit odd to ask a functional operator to do something sequential (at least relative to the real world). In the “awkward squad” paper note that the functional encoding of the bind operator *passes* the world from one place to another -- it is not part of the world, and does not act upon the world itself.

In recent work on effect systems there are a lot of embeddings of modal logics into the ambient Haskell/predicate logic, and the embeddings then suffer an encoding overhead. AFAIK the future lies in type systems that natively express temporal concepts, rather than needing tricky encodings of them, but we’re not there yet.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list