Re: [Haskell-cafe] unsafePerformIO: are we safe?

Chaddaï Fouché wrote:

2007/9/26, Adrian Hey :

...

Chaddaï Fouché wrote:

...

There can't be alternatives, unsafeIO throw by the window most guarantee that Haskell can give you and you have to provide them yourself (with a proof of this part of your program), but it's inherent to the nature of the beast, it's what it do ! What about ..

http://www.haskell.org/haskellwiki/Top_level_mutable_state

This as unsafe a use of unsafePerformIO as you'll ever find, but necessary for real IO libs.

I'm not arguing that there aren't specific current usage of unsafePerformIO that could be better formalized (there are), I'm saying that you can't design an alternative to unsafePerformIO which cover all its applications but stay safer. What we can do with unsafePerformIO is inherently unsafe, even though you can obtain safe results with it (and in some of those use-case, a restricted version of unsafePerformIO could be used and would be safer).

In your original post you appear to be making the usual argument about proof obligations and the possibility that unsafePerformIO can be used safely, despite the name (and should only be used this way). I was simply pointing out that there is at least one common use of unsafePerformIO for which this isn't possible (and there is currently no safe alternative). Regards -- Adrian Hey