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

[apfelmus]

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