I'm relatively new to Polysemy, and I'm trying to wrap my head around how to use NonDet correctly. Specifically, let's say I've got this computation

generate :: Member NonDet r => Sem r Int
generate = msum $ fmap pure [0..]

computation :: (Member NonDet r, Member (Final IO) r) => Sem r ()
computation = do
  n <- generate
  guard (n == 100)
  embedFinal $ print n

It's a horribly inefficient way to print the number 100, but it demonstrates the problem I'm having. Now, I want to run this effect only insofar as to get the first success. That is, I want to run this effect long enough to "find" the number 100 and print it, and then I want to stop.

My first attempt

attempt1 :: IO ()
attempt1 = void . runFinal . runNonDet @[] $ computation

This one fails to short-circuit. It prints 100 but then hangs forever, looking for the number 100 again. That makes sense; after all, I didn't actually tell it I only wanted one solution. So let's try that.

My second attempt

runNonDetOnce :: Sem (NonDet ': r) a -> Sem r (Maybe a)
runNonDetOnce = fmap listToMaybe . runNonDet

attempt2 :: IO ()
attempt2 = void . runFinal . runNonDetOnce $ computation

All we're doing here is discarding all but the head of the list. Understandably, this didn't change anything. Haskell already wasn't evaluating the list, so discarding an unused value changes nothing. Like attempt1, this solution hangs forever after printing 100.

My third attempt

attempt3 :: IO ()
attempt3 = void . runFinal . runNonDetMaybe $ computation

So I tried using runNonDetMaybe. This one, unfortunately, just exits without printing anything. Figuring out why that is took a bit, but I have a theory. The documentation says

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

So it's greedy and doesn't backtrack after success, basically. Thus, it runs my computation like this.

computation = do
  n <- generate        -- Ah yes, n = 0. Excellent!
  guard (n == 100)     -- Wait, 0 /= 100! Failure! We can't backtrack, so abort.
  embedFinal $ print n

Non-Solutions

In this small example, we could just alter the computation a bit, like so

computation :: (Member NonDet r, Member (Final IO) r) => Sem r ()
computation = msum $ fmap (\n -> guard (n == 100) >> embedFinal (print n)) [0..]

So rather than generate a number and then check it later, we simply move generate inside of computation. With this computation, attempt3 succeeds, since we can get to the "correct" answer without backtracking. This works in this small example, but it's infeasible for a larger codebase. Unless someone has a good systematic way of avoiding backtracking, I don't see a good way to generalize this solution to computations that span over multiple files in a large program.

The other non-solution is to cheat using IO.

computation :: (Member NonDet r, Member (Final IO) r) => Sem r ()
computation = do
  n <- generate
  guard (n == 100)
  embedFinal $ print n
  embedFinal $ exitSuccess

Now attempt1 and attempt2 succeed, since we simply forcibly exit the program after success. But, aside from feeling incredibly sloppy, this doesn't generalize either. I want to stop running the current computation after finding 100, not the whole program.

So, to summarize, I want the computation given in the first code snippet above to be run using Polysemy in some way that causes it to backtrack (in NonDet) until it finds one successful value (in the example above, n = 100) and then stop running side effects and end the computation. I tried delving into the source code of runNonDetMaybe and co in this hopes of being able to reproduce something similar to it that has the effect I want, but my Polysemy skills are not nearly to the level of understanding all of the Weaving and decomp shenanigans happening there. I hope someone here who has more expertise with this library than I do can point me in the right direction to running NonDet with the desired effects.

Now attempt1 and attempt2 succeed, since we simply forcibly exit the program after success. But, aside from feeling incredibly sloppy, this doesn't generalize either. I want to stop running the current computation after finding 100, not the whole program.

Rather than exitSuccess, a closely related idea is to throw an exception that you can catch in the interpreter.