A colleague of mine Victor Miraldo asked me today whether I know how to use unsafePerformIO safely. And I realized I have no idea. Do you? Or do you know of an existing blog post / other resource that addresses this?
Context: Victor is writing a program that needs to call out to an SMT solver. An SMT solver acts like a pure function: it gets information in and then deterministically produces a result based (only) on its input. But because the SMT solver is invoked via a separate process, the interface to it must be routed through IO. So Victor wants to write a pure interface to the SMT solver using unsafePerformIO. But this interface should be robust to multi-threading (at least). And, other than lots of guess-and-check, it’s hard to know how to proceed confidently.
If it’s helpful, Victor shared this idea (which he credited to Conal Elliott): Imagine (in a dependently typed language) safePerformIO :: (action :: IO a) -> ProofOfSafety action -> a, where ProofOfSafety action is a proof that executing action is indeed safe. What would ProofOfSafety look like? Or maybe this interface is wrong somehow – but hopefully you get the idea. If this new point is not helpful to you, please ignore; I’m more interested in resources about normal (non-proof-carrying) uses of unsafePerformIO.
My advice is: don’t. Define a monad SMT which has a function solve :: Params -> SMT Result and a “morally pure” handler SMT a -> IO a. Trying to pretend that solve is really pure of type Params -> Result is going to lead to a lot of headaches down the line. If there’s a usecase where SMT monad gets in the way somehow then I’d love to know what it is!
For this to be safe, the IO computation should be free of side effects and independent of its environment.
If the SMT solver really acts like a pure function then it is free of side effects and independent of its environment, so it is safe to use unsafePerformIO.
Formally proving that a function like this is pure sounds very difficult. I think that would involve proving things about the operating system and the SMT solver.
@tomjaguarpaw, having the SMT monad gets in the way of reasoning and writing a clear denotation to code that calls the solve function. With a monad in there I’m now forced to pick an execution order. Testing becomes much more difficult too, because now my properties would have to be monadic.
Even if we end up going that way on our implementation, there is still the question of having a canonical, concrete answer to the question of when is unsafePerformIO safe.
@jaror while I agree that in spoken language the docs are descriptive, its far from letting me know what does that statement really mean. For instance, here’s the solve function I was able to conjure from my experiments (consider Env and Query to be opaque types)
{-# NOINLINE solve #-}
solve :: Env -> Query -> Bool
solve gamma = unsafePerformIO $ do
solver <- cvc4_ALL_SUPPORTED True
declareVariables gamma
mv <- evaluate solver >>= newMVar
return $ \ q -> unsafePerformIO $ do
withMVar mv $ \safeSolver -> do
runSolverWith safeSolver $ do
solverPush
assert q
res <- checkSat
solverPop
return $ case res of
SimpleSMT.Unsat -> False
_ -> True
I find it quite elegant that partial application embodies sharing the SMT environment. Yet, how do I know I didn’t miss any case? Is the evaluate solver really necessary? I found this e-mail in the mailing list archives that goes in the direction I’m looking for: Prevent optimization from tempering with unsafePerformIO
In a sequential setting, I guess we can say that unsafePerformIO k is safe iff let x = unsafePerformIO k in (x, x) is equal to (unsafePerformIO k, unsafePerformIO k), where we’d have some leeway on what “equal” means. do you know of a set of such “equalities” that could help provide a more formal footing to “performs no side-effects” and “independent of its environment”?
I don’t think so. I would be surprised if evaluating it would have side-effects, but that all depends on what the cvc4_ALL_SUPPORTED function does.
That is certainly a necessary condition, but I am not convinced it is sufficient to prove that k is free of side-effects.
I think the question you really want to ask is what does referential transparency and purity really mean formally? I would say referential transparency formally means something like: for every expression x and context E (expression with a hole), if x evaluates to a value v and E[x] evaluates to v' then E[v] evaluates to v'.
unsafePerformIO is safe iff referential transparency is preserved. So in particular: for every context E, if unsafePerformIO x evaluates to a value v (and it should always evaluate to the same value v!) and E[unsafePerformIO x] evaluates to v' then E[v] evaluates to v' (i.e. other pure functions in the context should not be able to observe any side effects).
Of course a big problem is that we don’t have a formal semantics of Haskell, so you can’t really make anything formal. And as I already mentioned we also will need a formal model of the OS and the external SMT solver program.
And as you mention, you probably need to be more specific about your notion of equality, although I suspect limiting the proof to expressions that return booleans and using the standard boolean equality might suffice see the writeFile example below. Also, some care needs to be taken to account for laziness and bottoms.
Absolutely! Bringing a monad into a design incurs a heavy cost that IMO can sometimes go unnoticed. Say you have f :: (Monad m) => a -> m b. Calling mapM f xs for some xs implies an explicit execution order which might forbid parallel implementations whereas map is inherently parallel. It also becomes more difficult to reason about your code. Is mapM (f <=< g) xs, in fact, equal to mapM g xs >>= mapM f? Hopefully! But if m ~ IO, for example, I don’t know what “equal” should mean.
Another aspect is the API design. Up to which point is it a good idea to burden all users and all uses of a library to deal with implementation specific (i.e.: non-essential) complexity just because the implementors couldn’t solve an implementation puzzle?
A great example is the bytestring library. It provides an API designed to be pure and elegant and hides a lot of the implementation concerns away where they belong: inside the implementation. How would ByteString look like if all functions returned IO ByteString instead?
In the particular example of the SMT solver, we need IO just because there is no SMT solver written purely in Haskell, hence we need to talk to another process. Otherwise, it is an operation that has a very clear specification: solve env exp = True iff exp is SAT.
Miss some possible usage of my code that is, in fact, unsafe.
In this case, cvc4_ALL_SUPPORTED calls simple-smt's newSolver, but that is just a small example, my question is more general.
That’s alright; I certainly appreciate the difficulty of that problem. But maybe we can collect a set of rules that start establishing the good practices even if its impossible to come up with a complete treatment. I feel a little dissatisfied with the usual “its bad, don’t do it”, especially because the alternative of permeating the code with IO can be bad too.
I guess my question, in general, is whether we have a set of resources that shed light on how does one judge whether a certain unsafePerformIO call is “safe” or not. For example:
never forget {-# NOINLINE ... #-}
I really like the point on referential transparency you brought up. In that context, the rule-of-thumb I mentioned was just one single context: E[v] = let x = v in (x, x). Are there some other contexts that work particularly well to illustrate other situations? How about concurrency: E[f] = (v1 `par` v2, v1) where v1 = f 1; v2 = f 2?
Do you care if side-effects are performed at all? I.e., how about E[v] = let x = v in True? If you do care for side-effects, how to get around that and ensure the E[unsafePerformIO k] actually triggers the side-effects? Maybe you don’t get around and just embrace IO in that case.
As long as the IO action is actually really pure (e.g. running another Haskell program that only uses interact in its main function), then no special measures are necessary. Things like NOINLINE, -fno-cse, and -fno-full-laziness are only required if you still want the side-effects of each unsafePerformIO call to be performed exactly once.
I’m imagining a context like
E[x] = do evaluate x; readFile "test"
This shows that writeFile "test" "something" is not pure, because do evaluate (unsafePerformIO (writeFile "test" "something")); readFile "test" is clearly different than do evaluate (); readFile "test". However, this does require some kind of equality on the IO type.
How else would we prove that writeFile "test" "something" is not pure?
Exceptions can only be caught from inside IO. In the pure subset of Haskell throwing an exception is like entering an infinite loop. Exceptions thrown from within the unsafely performed IO are no different. 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))
FUNDIO: A Lambda-Calculus With letrec,
case, Constructors, and an IO-Interface:
Approaching a Theory of unsafePerformIO (Manfred Schmidt-SchauĂź) https://core.ac.uk/download/pdf/14504553.pdf
A Partial Rehabilitation of Side-Effecting I/O: Non-Determinism in Non-Strict Functional Languages (also by Schmidt-SchauĂź) Download Limit Exceeded
Look for the Uniq name-supply type in GHC’s sources - it uses an alternate approach which isn’t so sequential.
Oleg Kiselyov has written about reviving another early approach to dealing with effects.
Your reply makes me think that I probably didn’t explain my original proposal clearly enough, so I shall try to elaborate further.
It’s very important to note that I am not suggesting running the SMT solver directly in the IO monad. I am suggesting defining a monad SMT (in fact in practice probably a transformer SMTT) in which SMT actions can be run. In particular there will be a function solve :: Params -> SMT Result. This SMT monad will be (morally) pure. That is, the following equivalences hold in SMT:
do
x <- mx
y <- my
...
==
do
y <- my
x <- mx
...
do
_ <- m
...
==
do
...
do
x1 <- m
x2 <- m
...
==
do
x1 <- m
let x2 = x1
...
(If they don’t hold exactly then they hold modulo some set of observations that you care about. That’s the “morally” part.)
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.
Then the question arises “how do I get the a out of an SMT a?”. Well, the answer is you use runSMT :: SMT a -> IO a.
Calling mapM f xs for some xs implies an explicit execution order which might forbid parallel implementations whereas map is inherently parallel.
I’m not sure what you mean. map is not “inherently parallel”. It is sequential, as can be verified by looking at its implementation. Perhaps you are thinking of parMap? But if you want similar “parallel” functionality in SMT then you can define parallelSMT :: SMT a -> SMT b -> SMT (a, b), without needing to pretend that calling out to an external process is “pure”.
Another aspect is the API design. Up to which point is it a good idea to burden all users and all uses of a library to deal with implementation specific (i.e.: non-essential) complexity just because the implementors couldn’t solve an implementation puzzle?
This seems to be begging the question: what exactly about SMT is “complexity”? It would just be a normal monad, something that Haskellers are perfectly happy to deal with.
A great example is the bytestring library. It provides an API designed to be pure and elegant and hides a lot of the implementation concerns away where they belong: inside the implementation. How would ByteString look like if all functions returned IO ByteString instead?
I’m not sure what you mean. bytestring isn’t secretly using IO inside and unsafePerformIO is not used in it, except to allocate ByteStrings (which arguably should be a pure part of the run time system). It doesn’t call out to external processes!
In the particular example of the SMT solver, we need IO just because there is no SMT solver written purely in Haskell, hence we need to talk to another process. Otherwise, it is an operation that has a very clear specification: solve env exp = True iff exp is SAT.
Sure, and solving in the SMT monad also has a very clear specification solve env exp = pure True iff exp is SAT.
I’m still not seeing how a monadic interface is much of an inconvenience, and certainly not at all an inconvenience to the compared to the rest of the codebase which is presumably using many monads already. So if you could elaborate further with more details of such inconvenience then I would appreciate it.
It does use IO for other things, e.g. here, here, and here. In the end, any manipulation (mostly allocation and indexing) of the underlying data needs to go through the Storable/(Foreign)Ptr api which is all in IO.
You’ll still need to prove that (probably informally). And if you have such an (informal) proof why not just use unsafePerformIO?
Ah, I beg your pardon then, because I was foolish enough to only grep for unsafePerformIO.
I’ll have to adjust my point of view on that slightly.
I agree that the pure ByteString API is much better than doing everything in a BS monad!
I’m somewhat skeptical that much of the ByteString operations really need some form of “unsafely performing” IO. Rather I expect that some very small subset of operations should be exposed by the RTS or a base library and the bytestring library could be purely implemented in terms of those. Just for historical reasons this is done with IO littered all over the place and no one dares clean it up.
The case of bytestring is very different from the case of an SMT solver, largely because there are likely to be fewer calls in one’s codebase to the SMT solver than to the ByteString API, and because there are fewer functions in the SMT solver API.
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.
I strongly suspect that if you use unsafePerformIO for things that you have only informally proved morally pure, i.e. only pure up to some set of observations that you care about, then you will end up with a big headache somewhere down the line.
But ultimately I’m not trying to stop anyone doing so! Everyone is free to choose their own API as far as I am concerned. 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’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…
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.
I don’t think I can prove that. What is “equal” supposed to mean if we’re running an IO computation under the hood?
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.
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.
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.
Memory can also run out making allocation in bytestring fail too…
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.
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.
I think you can, from the commutativity and idempotency properties I gave above. How you prove those is another matter, but no more difficult than, and in fact very similar to, proving “purity”.
What is “equal” supposed to mean if we’re running an IO computation under the hood?
It means that you can replace one with another in your program and get equal results. You might respond: “But my program is in IO so I don’t even know what it means to get equal results!” True, but the same applies to proving that your program is pure. After all, you’ll have a similar problem when trying to prove that solve env exp = True iff exp is SAT.
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.
Perhaps, but you can also execute traverse f in parallel for any commutative monad (which SMT is) because in such a case there is no dependency between the calls of f either.
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.
I’m pretty sure that proving it’s observationally equal to pure True is roughly equally as difficult as proving that solve env exp = True for a pure version of solve, as I mentioned above.
Memory can also run out making allocation in bytestring fail too…
Yes, true. But there are few ways the RTS can fail, and they are largely non-recoverable. On the
other hand there are many ways calling out into the OS can fail, and they are largely recoverable.
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.
Well, I admit that I haven’t tried it, but my strong belief is that writing proofs for idempotent, commutative monads is not much harder than for pure code.
As I said, I agree that the bytestring API is nicer pure, but there are mitigating circumstances. For example, we typically want to combine ByteStrings with other ByteStrings in a multitude of ways. I maybe be too unimaginitive, but I do not envisage SAT results being combined in quite so many ways.
Furthermore, if there were an API similar to ByteString but operating on the (immutable once written) contents of files on the filesystem then I would definitely want the API to be monadic, even though it would be as morally pure as your proposed SAT API.
Here’s a concrete example of why I don’t like pretending that anything that interacts with the OS is “pure”:
At work we have a Nix-based build system. It “should be” pure, since Nix is reproducible. However, it sometimes calls out to external hardware which is transiently broken, caching “hardware did not respond” into our build results, and with no way of purging it. There’s no direct analogue of that in Haskell, but it really makes me cautious of “pure” APIs that call out to the OS, and I wouldn’t use one myself, in practice. (I think it’s a worthy academic exercise though.)
There’s some prior work on catching exceptions in pure code. It is highlighted in “A Semantics for Imprecise Exceptions” that catching from pure code leads to nondeterministic results, e.g. pureCatch (error "this" + error "that") could return the “this” error or the “that” error, because the evaluation order of Haskell is not fixed. However since my function only returns True or False based on whether there is an exception at all, I think it might still be pure. This also only works if every exception is caught by that SomeException signature.
I don’t think f undefined == False is a problem, e.g. f _ = False is pure and also satisfies that equation.
…well, something like that, but probably at the level of types, not expressions since ProofOfSafety is a dependent type. In either case, the implementation can use the connection between the two deleteFile calls to respond accordingly.
If you haven’t already read it, this is loosely based on the functional pearl On generating unique names: https://www.cambridge.org/core/services/aop-cambridge-core/content/view/763DE73EB4761FDF681A613BE0E98443/S0956796800000988a.pdf/functional_pearl_on_generating_unique_names.pdf (the first “alternate approach”).
I see you took on challenge much further than what I had in my mind. You seem to be thinking of making ProofOfSafety aware of external resources. That would be awesome, but its much harder than the original idea/question of starting with ProofOfSafety covering only the aspects intrinsic to the code manipulations runtime system. At the end of the day, if you try to delete the same file twice, being in IO or not doesn’t help you at all; you get an exception and crash and that’s it.
Here’s an aspect intrinsic to the compiler and the RTS: let x = unsafePerformIO k in (x, x) must be “equal” to (unsafePerformIO k, unsafePerformIO k); I’ll call that the CSE-equality for k. A proof of CSE-equality should naturally be a component of ProofOfSafety. In fact, it already informs us that deleteFile "foo.txt" is not safe:
let x = unsafePerformIO (deleteFile "foo.txt") in (x, x) == ((), ())
That’s a great example because it brings up the question of exceptions! How about defining an operation deleteFileIdemp f = deleteFile f `catch` (\(e :: IOError) -> ())? Is that safe? If would certainly satisfy the CSE-equality. My question is whether we can find a set of such properties that are sufficient to prove that running unsafePerformIO k is just as safe as running the entire code in IO for some k. In other words, relying unsafePerformIO to benefit from purity doesn’t come at any additional safety cost: if the code crashes, it would also have crashed had we placed IO everywhere anyway.
Alright, I now think your best option is to look at those two papers by Schmidt-Schauß, seeing if there’s more recent research (e.g. via a citation search). My interest in this topic is the result of searching for other approaches to I/O in languages like Haskell:
Before monadic IO, there was a lot of vibrant and imaginative work on functional I/O. It hadn’t arrived yet, but was still in touch with the spirit of functional programming.
In all that time, I’ve never thought of trying to establish a basic set of rules or principles for the safe use of unsafe... pseudo-definitions, particularly after encountering remarks like:
During the 1960s, several researchers began work on proving things about programs. Efforts were made to prove that:
A program was correct.
Two programs with different code computed the same answers when given the same inputs.
One program was faster than another.
A given program would always terminate.
While these are abstract goals, they are all, really, the same as the practical goal of “getting the program debugged”.
Several difficult problems emerged from this work. One was the problem of specification: before one can prove that a program is correct, one must specify the meaning of “correct”, formally and unambiguously. Formal systems for specifying the meaning of a program were developed, and they looked suspiciously like programming languages.
…but maybe you can see what the rest of us has missed, either in Schmidt-Schauß’s papers or other content, and make the breakthrough which reconciles the presence of effects with the otherwise-mathematical clarity presented by languages like Haskell - all the best with your research.
