emilaxelsson · October 26, 2015 09:57
diff --git a/StrictTermination.lhs b/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).
	<!--
	\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).