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 <apfelmus@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