[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why
can't Haskell be faster?)
apfelmus at quantentunnel.de
Fri Nov 2 06:35:26 EDT 2007
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
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 ;)
More information about the Haskell-Cafe