Paul Hudak wrote:
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.
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.
Ah, so the denotational semantics would be a bit like good old
stream-based IO.
However, we have to change the semantics of -> , there's no way to put
the side effects in *World only. I mean, the problem of both loop and
loop' is that they never return any world at all, the side effects occur
during function evaluation. Then, we'd need a "purity lemma" that states
that any function not involving the type *World as in- and output is
indeed pure, which may be a bit tricky to prove in the presence of
higher-order functions and polymorphism. I mean, the function arrows are
"tagged" for side effects in a strange way, namely by looking like
*World -> ... -> (*World, ...).
In contrast, we can see IO a as an abstract (co-)data type subject to
some straightforward operational semantics, no need to mess with the
pure -> . So, in a sense, the Haskell way is cleaner than the Clean way ;)
Regards,
apfelmus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
