fixST lost bottoms

[Levent Erkok]

Hi David,

Wonderful example. I'm afraid no-eager-blackholing also breaks the "no
spooky action at a distance" rule. Since `x` is not used recursively, we
should be able to pull it out of the `mfix` call, transforming the original
to:

foo :: ST s Int
foo = do
  ref <- newSTRef True
  x <- readSTRef ref
  mfix $ \res -> do
    if x
      then do
        writeSTRef ref False
        return $! res + 5 -- force the final result
      else return 10

I believe this variant will produce <<loop>> with or without
eager-blackholing, as it should. By this argument alone, I'd say the
no-eager-blackholing breaks mfix axioms for strict-state.

This example is also interesting from a pure termination point of view:
Moving things "out-of" mfix usually improves termination. In this case, the
opposite is happening.

Strictly speaking, this is in violation of the mfix-axioms. But I doubt
it's worth losing sleep over. I suggest we add this as an example in the
value-recursion section on how eager-blackholing can change things.

Cheers,

-Levent.

On Sun, Jul 8, 2018 at 9:40 AM, David Feuer <david.feuer at gmail.com> wrote:

> I filed a ticket[*] for this, but I think maybe the libraries list should
> weigh in on whether it is something that should be fixed. In general, fixST
> f is supposed to bottom out if f forces its argument. However, the lazy way
> GHC blackholes thunks under evaluation sometimes leads to the computation
> being run again. In certain contrived situations, this can allow the
> computation to succeed!
>
> The example I give in the ticket:
>
> import Control.Monad.ST.Strict
> import Control.Monad.Fix
> import Data.STRef
>
> foo :: ST s Int
> foo = do
>   ref <- newSTRef True
>   mfix $ \res -> do
>     x <- readSTRef ref
>     if x
>       then do
>         writeSTRef ref False
>         return $! res + 5 -- force the final result
>       else return 10
>
> main = print $ runST foo
>
> Here, the computation writes to an STRef before forcing the final result.
> Forcing the final result causes the computation to run again, this time
> taking the other branch. The program prints 15. When compiled with -O
> -feager-blackholing, however, the expected <<loop>> exception occurs.
>
> As far as I know, this weirdness never changes the value produced by a
> non-bottoming computation, and never changes a non-bottoming computation
> into a bottoming one. The fix (defining fixST the way fixIO is currently
> defined) would have a slight performance impact. Is it worth it?
>
> [*] https://ghc.haskell.org/trac/ghc/ticket/15349
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180708/938772c3/attachment.html>