Using unsafePerformIO safely?

[VictorCMiraldo]

@atravers

Let’s consider a simple use case for that version of safePerformIO:

deleteFile :: Text -> ()
deleteFile path = safePerformIO (System.Directory.removeFile path) safeToDelete

So what should happen here?

task = (... (deleteFile "./temp.txt") ... (deleteFile "temp.txt") ...)

For ProofOfSafety values enities to be able to check for a problem like this, they would need some way to be “connected” e.g.

deleteFile :: Text -> ProofOfSafety (...) -> ()
deleteFile path safeToDelete =
  safePerformIO (System.Directory.removeFile path) safeToDelete

task safeToRun =
  let !(safe1, safe2) = safeParts safeToRun in
  (... (deleteFile "./temp.txt" safe1) ... (deleteFile "temp.txt" safe1) ...)

…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.

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) == ((), ())

whereas

(unsafePerformIO (deleteFile "foo.txt"), unsafePerformIO (deleteFile "foo.txt"))

will crash.

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.