[Haskell-cafe] Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)

Stefan Holdermans wrote:

Exposing uniqueness types is, in that sense, just an alternative to monadic encapsulation of side effects.

While *World -> (a, *World) seems to work in practice, I wonder what its (denotational) semantics are. I mean, the two programs loop, loop' :: *World -> ((),*World) loop w = loop w loop' w = let (_,w') = print "x" w in loop' w' both have denotation _|_ but are clearly different in terms of side effects. (The example is from SPJs awkward-squad tutorial.) Any pointers? Regards, apfelmus