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