[Haskell-cafe] Re: Microsoft's Singularity Project and Haskell

[wren ng thornton]

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.

-- 
Live well,
~wren