ku-fpg / data-reify

Reification of data structures using observable sharing
Other
28 stars 7 forks source link

What are the conditions for safe `unsafePerformIO`? #13

Open bert2 opened 1 year ago

bert2 commented 1 year ago

Observable sharing in general is unsafe, so we use the IO monad to bound this effect, but can be used safely even with unsafePerformIO if some simple conditions are met.

I can't find any explanations on these conditions. Even bought the paper on ACM in the hopes to find them there :(

noughtmare commented 1 year ago

I don't think the conditions are as simple as the authors claim. But I think the main requirement is that the end result should be independent from the particular sharing structure. For example, the list:

x = 1 : x

Is the same as this list which is unrolled one level:

y = 1 : 1 : y

But reifyGraph would produce two different graphs.

Still, we can write a function over the graphs that always produces the same answer regardless of this unrolling. For example a function that checks if all elements of the graph are equal to 1:

f :: Graph (DeRef [Int]) -> Bool
f (Graph g _) = all (\(_, x) -> case x of NilF -> True; ConsF x _ -> x == 1) g

With this function we can safely use unsafePerformIO:

g :: [Int] -> Bool
g = unsafePerformIO . fmap f . reifyGraph

Edit: Actually, g still seems to be unsafe because it can observe compiler optimizations for this expression:

z = let go () = 1 : go () in go ()

If compiler optimizations are disabled g z will loop infinitely but with optimizations it returns True.

So, I think using unsafePerformIO with reifyGraph is almost always unsafe.