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.
I’m not sure how it works under the hood though - so I can’t justify why this whole affair works. But my intuition around unsafePerformIO at least has always worked!
But this interface should be robust to multi-threading (at least).
How so? You could certainly solve something in one thread and then pass its result to another I imagine. You could probably even use unsafeDupablePerformIO there if you didn’t call the SMT solver twice on the same inputs (as I understand it).
…which is more-or-less the “safe-use requirements” for unsafePerformIOunsafeLocalState - see chapter 30 of the Haskell 2010 Report.
I’m just wondering: is there a library for this particular SMT framework? If so, perhaps primitive imports (one of GHC’s FFI extensions) could access the library directly, using a non-IO type.
However in either case, foreign code is being used, and to quote one M. Chakravarty:
After all, you can import any C function with a pure type, which also allows you to wreak arbitrary havoc. We enable the user to disguise arbitrary machine code as a Haskell function of essentially arbitrary type. In comparison, unsafePerformIO [or unsafeLocalState] seems angelic.
If anyone can make that arrangement robust to multi-threading, etc: well done!
Acquiring an MVar is a global effect in the program. Doing this in the context of IO is much easier to understand than in the execution of pure code. What does it matter if the runtime system chooses to stop executing some pure code? If it makes such a choice after acquiring the MVar it prevents any other thread from acquiring the MVar.
Taking an MVar is only impure if the MVar is exposed to the rest of the program. That is not the case here. In this case the only thing that can happen is that a function takes longer to run (assuming that the MVar does eventually get released), but that is not considered a side effect because pure programs cannot observe time.
For this to be safe, the IO computation should be free of side effects and independent of its environment.
I, too, think this specification is exact. It also gives compiler optimisations the greatest leeway to compile pure code efficiently and is the reason why Haskell can execute efficiently in the first place.
The beauty is that the specification of unsafePerformIO in f (unsafePerformIO e) only relates to e; it doesn’t assume anything about the function/environment/context f which is called with an argument that uses unsafePerformIO. If the specification would allow some premise about all such f, then certain compiler optimisations (like strictness analysis) would have to prove that f is never called with an argument that uses unsafePerformIO to unbox f's argument, say. This would amount to saying that the optimiser must assume that Haskell is lazy, (non-total,) and impure, which is horrible to work with.
IMO, that is why the docs of unsafePerformIO are written as they are. Many use cases, like those in bytestring, fall into this fragment: After the “IO transaction” e finishes, the intermittent side-effects are no longer observable.
Regarding supposedly safe uses of unsafePerformIO that fall outside the specification:
Given enough confidence of the programmer, deferring and interleaving side-effects with unsafeInterleaveIO to achieve something like value-supply: A library for generating values without having to thread state. (which @atravers linked and which is also used in GHC) is possible if you make sure that all environments indeed can’t observe the side-effects. That is often done by making very judicious use of supposedly strictly internal APIs like GHC.Types.Unique which break the abstraction. Properly locking away these APIs to “environments” that we control and where we can make sure the optimiser doesn’t interfere (by making use of NOINLINE etc.) means that the specification of unsafePerformIO applies again. I would say this is quite similar to encapsulation in the OO sense, where an export like nonDetCmpUnique would be considered bad practice to uphold the abstraction.
In terms of GHC, failure to do so means non-deterministic builds (in terms of binary hashes) and the resulting loss of incremental rebuilds. Despite years of ongoing efforts, I still feel like bugs still hide because of use of unsafe abstractions like that, because I sometimes observe more rebuilding than I feel is necessary.
Why is it so difficult to fix these bugs? Because we actually use the Int# identity of GHC’s Unique for implementing efficient maps in terms of IntMap. And now suddenly the whole, pure API (well, at least half) of IntMap has become non-deterministic with no IO to warn us! See this Note in the compiler: compiler/GHC/Types/Unique.hs · 706deee0524ca6af26c8b8d5cff17a6e401a2c18 · Glasgow Haskell Compiler / GHC · GitLab Our solution so far is to justify each use of a non-deterministic function (which all have a nonDet* prefix) with a comment like It's OK to use nonDetUFMToList here because ... which acts as our “proof” in the sense of the OP.
Without Ord Unique (which is non-deterministic), we could only use O(n^2) assocation lists for Unique/Name lookup, which is terrible. Non-determinism as a direct result of our unsafe use of unsafePerformIO is just horrible, but we get to use O(n) IntMaps. So I’d call our solution horribly efficient
…first unsafe, then nonDet - appearing soon: unknown.
Having praised monads to the hilt, let me level one criticism. Monads tend to be an all-or-nothing proposition. If you discover that you need interaction deep within your program, you must rewrite that segment to use a monad.
Once you’re in the IO monad, you’re stuck there forever, and are reduced to Algol-style imperative programming. You cannot easily convert between functional and monadic style without a radical restructuring of code.
One alternative would be to replace the prefixes with types - then entities like these:
unsafeLocalState :: IO a -> a
nonDetUFMToList :: UniqFM key elt -> [(Unique, elt)]
would require an extra argument:
localState :: Unsafe# -> IO a -> a
ufmToList :: NonDet# -> UniqFM key elt -> [(Unique, elt)]
where Unsafe# and NonDet# are abstract, like GHC’s RealWorld. Since it’s IO model is already nondeterministic and can be unsafe e.g. using the FFI to call “poorly-implemented” foreign entities:
…so no extra harm done to (what’s left of) the semantics attributed to Haskell.
Yes, the need for extra parameters would probably be annoying, but if it saves having to “monadify” vast segments of existing code (or even a change of paradigm)…
