Strictness can fix non-termination!

StrictTermination.lhs

  <!--
\begin{code}
module Loop where
\end{code}
  -->

(This post is literate Haskell, [available here](https://gist.github.com/emilaxelsson/26658849e39918883ffe).)

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.

\begin{code}
import Data.IORef
import System.IO.Unsafe
\end{code}

Consider the following function for turning an `IORef` into a pure value:

\begin{code}
unsafeFreezeRef :: IORef a -> a
unsafeFreezeRef = unsafePerformIO . readIORef
\end{code}

(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 `IO`:

\begin{code}
modRef :: (a -> a) -> IORef a -> IO ()
modRef f r = writeIORef r $ f $ unsafeFreezeRef r
\end{code}

However, this doesn't work, because the `readIORef` inside `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:

\begin{code}
modRef' :: (a -> a) -> IORef a -> IO ()
modRef' f r = writeIORef r $! f $ unsafeFreezeRef r
\end{code}

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 `modRef`:

\begin{code}
test = do
    r <- newIORef "hello"
    modRef' tail r
    putStrLn =<< readIORef r
\end{code}

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 `unsafeFreezeRef`?
--------------------------------------------------

In case you wonder where this strange example comes from, I'm working on a [generic library for EDSLs that generate C code](https://github.com/emilaxelsson/imperative-edsl). Among other things, this EDSL has references that work like Haskell's `IORef`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](https://github.com/emilaxelsson/imperative-edsl/commit/766be1b09fc744f7259f5eaeb5890a872a1e03a2) and [this](https://github.com/emilaxelsson/imperative-edsl/commit/51fd5ba91095d5a7d05a7f0113e353aa173ead81).