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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
