bracket releases too early when combined with NonDet

[tomjaguarpaw]

When I use bracket (or rather bracket_, in the example below) inside a runNonDet block the resource is released too early. Is this expected?

(I feel this must be a common question, so apologies if it's answered elsewhere, but I didn't find this precise issue in the documentation, nor from searching the issues here.)

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}

import Control.Applicative ((<|>))
import Polysemy (embed, runM)
import Polysemy.NonDet (runNonDet)
import Polysemy.Resource (bracket_, runResource)

example :: IO [Int]
example =
  runM $
    runNonDet $
      runResource $
        bracket_
          (embed (putStrLn "Acquired"))
          (embed (putStrLn "Released"))
          ( do
              r <- pure 1 <|> pure 2
              embed (putStrLn "Used")
              pure r
          )
-- ghci> example
-- Acquired
-- Used
-- Released
-- Used
-- Released
-- [1,2]

[tek]

Interesting. I assume it's expected for pure interpreters to distribute over runNonDet, but it's pretty weird when it's Resource 😅

This resembles the interaction with Error as described in lexi's semantics-zoo article, so it seems somewhat reasonable that the release action is run as part of each branch before starting the next.

Given that you wrote "too early" rather than "twice", I assume that you expected the distributive semantics – how would you expect the release action to be executed? Should the entire bracket be distributed? I've never thought about this before, so no idea what would be right.

#246 is the closest discussion I can find, though its initial focus is different from this issue.
But if you swap runNonDet and runResource, the release action is only executed once, FWIW.

In case you actually didn't explore the algebraic properties and just want to do IO with bracket, using resourceToIOFinal also provides those more familiar semantics 😄

[tomjaguarpaw]

Thanks for your response.

Given that you wrote "too early" rather than "twice", I assume that you expected the distributive semantics – how would you expect the release action to be executed? Should the entire bracket be distributed? I've never thought about this before, so no idea what would be right.

I would say that the desirable behaviour is that the release happens exactly once, at the first time at which it is no longer possible to run a continuation that holds the resource.

But if you swap runNonDet and runResource, the release action is only executed once, FWIW.

Unfortunately that's no good either, at least for runNonDetMaybe. Consider the following. example1 is fine, I get the expected result [2]. But example2 is not fine. I get the result Nothing. It should be Just 2!

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}

import Control.Applicative (asum, empty, (<|>))
import Control.Monad (guard)
import Polysemy (embed, runM)
import Polysemy.NonDet (runNonDet, runNonDetMaybe)
import Polysemy.Resource (bracket_, runResource)

example1 :: IO [Int]
example1 =
  runM $
    runResource $ do
      runNonDet $ do
        r <-
          bracket_
            (embed (putStrLn "Acquired"))
            (embed (putStrLn "Released"))
            ( do
                r <- (pure 1 <|> pure 2)
                embed (putStrLn ("Used: " ++ show r))
                pure r
            )
        guard (r /= 1)
        pure r

-- ghci> example1
-- Acquired
-- Used: 1
-- Used: 2
-- Released
-- [2]

example2 :: IO (Maybe Int)
example2 =
  runM $
    runResource $ do
      runNonDetMaybe $ do
        r <-
          bracket_
            (embed (putStrLn "Acquired"))
            (embed (putStrLn "Released"))
            ( do
                r <- (pure 1 <|> pure 2)
                embed (putStrLn ("Used: " ++ show r))
                pure r
            )
        guard (r /= 1)
        pure r

-- ghci> example2
-- Acquired
-- Used: 1
-- Released
-- Nothing

resourceToIOFinal doesn't seem to help either:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}

import Control.Applicative (asum, empty, (<|>))
import Control.Monad (guard)
import Polysemy (embed, embedFinal, runFinal, runM)
import Polysemy.NonDet (runNonDet, runNonDetMaybe)
import Polysemy.Resource (bracket_, resourceToIOFinal, runResource)

example1 :: IO [Int]
example1 =
  runFinal $
    resourceToIOFinal $ do
      runNonDet $ do
        r <-
          bracket_
            (embedFinal (putStrLn "Acquired"))
            (embedFinal (putStrLn "Released"))
            ( do
                r <- (pure 1 <|> pure 2)
                embedFinal (putStrLn ("Used: " ++ show r))
                pure r
            )
        guard (r /= 1)
        pure r

-- ghci> example1
-- Acquired
-- Used: 1
-- Used: 2
-- Released
-- [2]

example2 :: IO (Maybe Int)
example2 =
  runFinal $
    resourceToIOFinal $ do
      runNonDetMaybe $ do
        r <-
          bracket_
            (embedFinal (putStrLn "Acquired"))
            (embedFinal (putStrLn "Released"))
            ( do
                r <- (pure 1 <|> pure 2)
                embedFinal (putStrLn ("Used: " ++ show r))
                pure r
            )
        guard (r /= 1)
        pure r

-- ghci> example2
-- Acquired
-- Used: 1
-- Released
-- Nothing

[Burtannia]

Just passing by while doing a bunch of research into the NonDet situation...

I don't think the result with runNonDetMaybe is wrong, albeit it's not obvious at first glance. The behaviour of Maybe-style non-determinism is not to execute further branches at all as soon as one succeeds.

Unlike runNonDet, uses of <|> will not execute the second branch at all if the first option succeeds.

In your case, your first branch did succeed but you later rejected the result via guard leaving the only possible result to be Nothing.

[tomjaguarpaw]

I suppose so. I can get rid of the bracket and observe the behaviour whereby the branch of <|> is committed too early (example3). But my point is not that this behaviour is inexplicable, but more that it's not very useful. The point of non-determinism is that I can bail out of it and backtrack!

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}

import Control.Applicative (asum, empty, (<|>))
import Control.Monad (guard)
import Polysemy (embed, runM)
import Polysemy.NonDet (runNonDet, runNonDetMaybe)
import Polysemy.Resource (bracket_, runResource)

example3 :: IO (Maybe Int)
example3 =
  runM $
    runResource $ do
      runNonDetMaybe $ do
        r <- pure 1 <|> pure 2
        guard (r /= 1)
        pure r

-- ghci> example2
-- Acquired
-- Used: 1
-- Released
-- Nothing

[tek]

FWIW, I recalled in September that I had a discussion about this on Zulip at some point, where we tried interpreting into ListT, which appears to be behaving a bit better for simple cases. I uploaded that exercise: https://github.com/tek/nondet-bug/blob/main/app/Main.hs

[Burtannia]

@tomjaguarpaw The point is r <- pure 1 <|> pure 2 runs the computation and binds the result to r. In order to pass r to guard the decision must already have been made. If you want to guard inside each branch and have that considered by (<|>), you must put it inside each branch. Monads are sequential and that's what mandates this behaviour, it is not specific to Polysemy, it's fundamental to Alternative.

I think your original example with bracket is definitely problematic though and should be resolved. There seems to be a general issue with effect systems when handling how effects distribute (or don't distribute) over NonDet.

[tomjaguarpaw]

If you want to guard inside each branch and have that considered by (<|>), you must put it inside each branch. Monads are sequential and that's what mandates this behaviour

How do you reconcile this claim with the behaviour that the list alternative/monad has?

import Control.Monad (guard)
import Control.Applicative ((<|>))
import Data.Maybe (listToMaybe)

example3List :: Maybe Int
example3List =
  listToMaybe $ do
    r <- pure 1 <|> pure 2
    guard (r /= 1)
    pure r

-- ghci> example3List
-- Just 2

[Burtannia]

@tomjaguarpaw The list monad returns all branches. Therefore r is bound to both 1 and 2 in respective subsequent branches. Therefore the guard is applied to all branches because they all still exist after the bind. With the maybe variant, your second branch is already dead after the first step of the computation.

[tomjaguarpaw]

With the maybe variant, your second branch is already dead after the first step of the computation.

I agree, I'm just saying it's not very useful (it's basically just the Maybe monad), nor is it really what we mean or want by a "non-determinism monad".

[Burtannia]

@tomjaguarpaw I see what you mean. I don't really have the answer to this tbh, NonDet in this case seems to get its behaviour from the underlying Alternative instance. I can only suggest that it's a case of choosing an appropriate Alternative instance, if one exists, rather than an issue with NonDet.