(This post is literate Haskell, available here.)
I’ve always thought that strictness annotations can only turn terminating programs into non-terminating ones. Turns out that this isn’t always the case. As always,
unsafePerformIO changes things.
import Data.IORef import System.IO.Unsafe
Consider the following function for turning an
IORef into a pure value:
unsafeFreezeRef :: IORef a -> a unsafeFreezeRef = unsafePerformIO . readIORef
(I explain why I’m interested in this function below.)
This function is of course unsafe, but we may naively expect it to work in the following setting where it’s used inside a function that returns in
modRef :: (a -> a) -> IORef a -> IO () modRef f r = writeIORef r $ f $ unsafeFreezeRef r
However, this doesn’t work, because the
unsafeFreezeRef happens to be performed after
writeIORef, leading to a loop.
So, strangely, the solution is to use a strictness annotation to force the read to happen before the write:
modRef' :: (a -> a) -> IORef a -> IO () modRef' f r = writeIORef r $! f $ unsafeFreezeRef r
This is the first time I’ve seen a strictness annotation turn a non-terminating program into a terminating one.
Here is a small test program that terminates for
modRef' but not for
test = do r <- newIORef "hello" modRef' tail r putStrLn =<< readIORef r
I’m not sure this tells us anything useful. We should probably stay away from such ugly programming anyway… But at least I found this example quite interesting and counterintuitive.
Why on earth would anyone write
In case you wonder where this strange example comes from, I’m working on a generic library for EDSLs that generate C code. Among other things, this EDSL has references that work like Haskell’s
The purpose of
unsafeFreezeRef in the library is to avoid temporary variables in the generated code when we know they are not needed. The idea is that the user of
unsafeFreezeRef must guarantee that result is not accessed after any subsequent writes to the reference. Reasoning about when a value is used is quite easy in the EDSL due to its strict semantics. For example, we don’t need any strictness annotation in the definition of
modRef due to the fact that
setRef (the equivalent of
writeIORef) is already strict.
The reason I noticed the problem of laziness and
unsafeFreezeRef was that the EDSL evaluator turned out to be too lazy when writing to references. So I had a program which produced perfectly fine C code, but which ran into a loop when evaluating it in Haskell. The solution was to make the evaluator more strict; see this commit and this.