Using unsafePerformIO safely?

[VictorCMiraldo]

I’m glad this is picking up! Particularly, thanks to everyone for the great suggestions and discussion and for @rae for posting this here

@atravers, that’s amazing, thanks for all the references! I’ll study them!

I’ll try answering some points inline below…

@jaror

Catching exceptions inside the unsafePerformIO actually seems kind of strange to me, is the following function pure?

f x = unsafePerformIO (evaluate (x `seq` True) `catch` (\e -> (e :: SomeException) `seq` pure False))

That’s a good question.

That’s a good question indeed! That seems to enable one to catch calls to error (or other exceptions) purely. I’m inclined in calling f pure indeed, but its weird that f undefined == False. I guess that’s precisely the type of question I believe we have to answer as part of shedding light to unsafePerformIO.

@tomjaguarpaw

These equivalences (or similar) allow you to prove the results that you want. In particular:

Is mapM (f <=< g) xs, in fact, equal to mapM g xs >>= mapM f?

Yes! In SMT it would be.

I don’t think I can prove that. What is “equal” supposed to mean if we’re running an IO computation under the hood?

@tomjaguarpaw

I’m not sure what you mean. map is not “inherently parallel”. It is sequential, as can be verified by looking at its implementation.

Ok, fair. But it could have been implemented in parallel. I’d hope that future compilers would detect that fmap f can always be executed in parallel for any functor; there’s no dependency between the calls of f.

@tomjaguarpaw

Sure, and solving in the SMT monad also has a very clear specification solve env exp = pure True iff exp is SAT.

But it would never the equal to pure True (not even bringing it up the problem of defining “equal”). We brought IO into the domain of reasoning, we’re now doomed to have to reason about the side-effects that are performed or bring in a different equivalence relation.

@jaror

You’ll still need to prove that (probably informally). And if you have such an (informal) proof why not just use unsafePerformIO?

Precisely! That’s the question that brought all of this up for me. Hence, I’m looking into understanding what such a proof would look like, even if just informally. There’s tremendous value in pure APIs.

@tomjaguarpaw

The SMT solver can easily fail to be pure, for example, by not being installed, or through some OS-specific fault that typical Haskell “pure” functions are isolated from by the RTS.

Memory can also run out making allocation in bytestring fail too…

@tomjaguarpaw

I’m just trying to offer an alternative and understand the notion that monadic APIs are somehow “complex”. They don’t seem that way to me. And I guess I’m implicitly trying to counter the notion (perhaps) underlying this, that “pure” code is somehow “better” than monadic code.

I’d encourage trying to write proofs for monadic code versus trying to write proofs for pure code. I believe this complexity becomes much more present when we try to reason about the correctness of our programs. Nevertheless, even for programming exclusively, I’d bring up again how much nicer the bytestring API is, when compared to a hypothetical monadic alternative.