[Haskell-cafe] Re: Microsoft's Singularity Project and Haskell
wren ng thornton
wren at freegeek.org
Sat Jul 31 16:48:25 EDT 2010
David Leimbach wrote:
> Haskell's great and all but it does have a few warts when it comes to how
> much real trust one should put into the type system.
> Some compromises still exist like unsafePerformIO that you can't detect
> simply by looking at the types of functions.
> In order to live up to the hype and the marketing around Haskell, really
> things like unsafePerformIO should not be allowed at all.
As I mentioned in the thread about escaping monads, you actually have a
proof obligation in order to use unsafePerformIO. The only problem is
that those obligations are not captured in the source language itself,
so you must trust the code you link against, separately from any trust
induced by type checking.
There are very real reasons for wanting a function that can take an IO A
into A, which is why unsafePerformIO was added in the FFI addendum. The
only way to correct this situation is to (a) add a proof theory to the
Haskell language, a la dependent types; or, (b) to break apart the IO
sin bin so that we can track the more innocuous parts independently from
launching missiles. Of course, the second approach also requires proof
that information from the, e.g., RTS monad does not leak into the return
value of runRTS. To do this in general without loosing the power we want
from RTS, we'll need to add a proof theory to the language in order to
demonstrate that two functions are extensionally equal. So really, the
first option is the only one; in which case you might as well switch to
Agda or the like.
More information about the Haskell-Cafe