Using unsafePerformIO safely?

The question “when do we know that unsafePerformIO is safe” can be specialized to “why do we believe that runST is safe?” (which is one possible use of unsafePerformIO).

I asked that before, and shortly after an answer was given by Amin Timany et al in their POPL 2018 paper “A Logical Relation for Monadic Encapsulation of State”.

So that establishes one possible way of answering that question. I am not sure how easy it is to extend to other uses of unsafePerformIO (e.g. the tricks I am playing here), or to safety in the presence of concurrency.

2 Likes