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

[Arnar Birgisson]

Hi there,

I'm new here, so sorry if I'm stating the obvious.

On Nov 1, 2007 2:46 PM, apfelmus <apfelmus at quantentunnel.de> wrote:
> 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?

For side-effecting program one has to consider bisimilarity. It's
common that semantically equivalent (under operational or denotational
semantics) behave differently with regard to side-effects (i/o) - i.e.
they are not bisimilar.

http://en.wikipedia.org/wiki/Bisimulation

Arnar