[Haskell-cafe] unsafePerformIO: are we safe?
ahey at iee.org
Thu Sep 27 06:42:39 EDT 2007
Chaddaï Fouché wrote:
> 2007/9/26, Adrian Hey <ahey at iee.org>:
>> 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 ..
>> 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).
More information about the Haskell-Cafe