[Haskell-cafe] What unsafeInterleaveIO is unsafe

[Dan Doel]

On Monday 16 March 2009 2:11:10 pm Ryan Ingram wrote:
> However, I disagree with your description of what "unsafe" should be
> used for.  "unsafe" calls out the need for the programmer to prove
> that what they are doing is safe semantically, instead of the compiler
> providing those proofs for you.  Whether that is due to type safety
> (unsafeCoerce) or breaking the assumptions of the compiler
> (unsafePerformIO, unsafeInterleaveIO, unsafeIOToST), depends on the
> situation.

Of course, unsafeIOToST can also break the type system, because you can write:

  unsafePerformIO m = runST (unsafeIOToST m)

> For example, unsafePerformIO can make your program not type-safe, but
> it's convoluted to do so; in fact, at monomorphic types it can't break
> type safety.  That's not what makes it unsafe at all.  It's unsafe
> because it breaks the rule that pure values don't have side effects,
> so that the effects inside the unsafePerformIO might get executed more
> than once, or not at all, depending on how the compiler decides to
> evaluate the pure value returned.  And what happens could depend on
> the optimization settings of the compiler, the timing of the machine
> you are running on, or the phase of the moon.

In practice, 'unsafe' can mean any number of things depending on the context. 
unsafeRead/Write on mutable arrays can (attempt to) read/write arbitrary 
memory locations. An index into a data structure that just calls error instead 
of returning a Maybe result might be called unsafe. In a similar vein, some 
people think head and tail should be called unsafeHead and unsafeTail. :)

Technically, one can probably lay down a semantics of IO such that 
unsafeInterleaveIO maintains the purity of the language by the usual 
definitions. However, such a semantics is necessarily too vague to explain why 
you might want to use it in the first place, because the only real reason 
you'd want to do so is to have side effects triggered in response to 
evaluation of otherwise pure terms. At the very least, using 
unsafeInterleaveIO adds significant complications to reasoning about the 
behavior of otherwise ordinary IO, which might well justify its name.

-- Dan