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

[Paul Hudak]

One can certainly use an operational semantics such as bisimulation, but you don't have to abandon denotational semantics.  The trick is to make output part of the "final answer".  For a conventional imperative language one could define, for example, a (lifted, recursive) domain: Answer = Terminate + (String x Answer) and then define a semantic function "meaning", say, such that: meaning loop = _|_ meaning loop' = <"x", <"x", ... >> In other words, loop denotes bottom, whereas loop' denotes the infinite sequence of "x"s.  There would typically also be a symbol to denote proper termination, perhaps <>. A good read on this stuff is Reynolds book "Theories of Programming Languages", where domain constructions such as the above are called "resumptions", and can be made to include input as well. In the case of Clean, programs take as input a "World" and generate a "World" as output.  One of the components of that World would presumably be "standard output", and that component's value would be _|_ in the case of loop, and <"x", <"x", ... >> in the case of loop'.  Another part of the World might be a file system, a printer, a missile firing, and so on.  Presumably loop and loop' would not affect those parts of the World. If returning one World is semantically problematical, one might also devise a semantics where the result is a sequence of Worlds.     -Paul Arnar Birgisson wrote: Hi there, I'm new here, so sorry if I'm stating the obvious. On Nov 1, 2007 2:46 PM, apfelmus <[EMAIL PROTECTED]> 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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe