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

[apfelmus]

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