Choice of functorial state for runNonDet

[KingoftheHomeless]

Turns out choosing a functorial state for runNonDet is rife with trouble.

We previously used [] as the functorial state for runNonDet. However, this made the semantics of <|> differ depending on if it's used inside or outside a higher-order action of an effect interpreted after runNonDet.

data HO m a where
  HO :: m a -> HO m a

makeSem ''HO

runHO :: Sem (HO ': r) a -> Sem r a
runHO = interpretH $ \(HO m) -> runT m >>= raise . runHO

-- prints "abrahadabra" with both the new and old choice of functorial state
abrahadabra :: IO [()]
abrahadabra =
    runM
  . runHO
  . runNonDet @[]
  $ do
    _ <- embed (putStr "ab") <|> embed (putStr "hadab")
    embed (putStr "ra")

-- prints "abhadabrara" with the old choice of functorial state.
-- prints "abrahadabra" with the new choice of functorial state.
abhadabrara :: IO [()]
abhadabrara =
    runM
  . runHO
  . runNonDet @[]
  $ do
    _ <- hO $ embed (putStr "ab") <|> embed (putStr "hadab")
    embed (putStr "ra")

This also means that listen and censor will hear all tells of all branches collectively within the argument to a listen/censor; for example, if you do listen $ tell "ab" <|> tell "ra", then you will hear "abra" in both resulting branches, rather than first "ab", and then "ra".

My solution in #210 was to change the choice of functorial state to one similar to one ListT uses for its MonadBaseControl instance in the list-t package. That fixes this, but it has a unfortunate side-effect; only the first branch is visible to any higher-order action, and all other branches are hidden in the functorial state.

For example:

-- Prints out "onetwo" under the old choice of functorial state.
-- Prints out "one" under the new choice of functorial state.
asyncTest :: IO [()]
asyncTest =
    runFinal
  . asyncToIOFinal
  . runNonDet @[]
  $ do
    a <- async (embedFinal (putStr "one") <|> embedFinal (putStr "two"))
    _ <- await a
    return ()

Similarly, censor only affects the first branch, listen only hears what the first branch has to tell, and most egregiously, catch can only catch exceptions of the first branch.

So the two different choices of functorial state of runNonDet have their own share of troubles, and neither choice is ideal. I doubt there's a perfect solution to this problem.

I recommend reverting to using [] as the functorial state for runNonDet. It's bad, but it's not as bad as the problems you get with NonDetState.

[isovector]

I hate programming :(

[ocharles]

Is this the same as the discussion in https://github.com/polysemy-research/polysemy/issues/80#issuecomment-504789558? Specifically:

For example, in NonDet, it will return the first successful thing in an asum --- pretty reasonable semantics!

Which I replied:

I have no idea if this is reasonable semantics! But I am unfortunately less hopeful, and think this could well result in some super spooky-action-at-a-distance debugging.

[KingoftheHomeless]

Only tangentially so; that discussion is about how the inspector can only fetch up to one value from the functorial state of runNonDet, and not multiple values. This discussion is about how to represent that functorial state of runNonDet, as the currently known representations either causes NonDet to mess up other higher-order effects, or causes NonDet to get messed up by other higher-order effects.

[ocharles]

Right, but is it not due to other things using the inspector?

[ocharles]

I often approach things like this by contrasting to fused-effects, which is fundamentally the same idea, but a little more "open". Have they solved it there, or do they have the same problem? If so, it may point to some problems in the weaving formulation, which would be very interesting to understand.

[KingoftheHomeless]

The problems mentioned in the OP is not related to the use of the inspector.

I think fused-effects has the same problem. They use [] as the functorial state in the Carrier instance for NonDetC when weaving other effects through.

[ocharles]

Then @robrix and @zenzike might want to have a look at this too!

[robrix]

(We’re currently using a binary tree on master, but I imagine it has the same issue.)

[isovector]

Thanks for tracking this down, @KingoftheHomeless. It's becoming more and evident to me that we should make a significantly more comprehensive test suite to stop being blindsided by huge problems like these.

[spacekitteh]

Well, I'm making a series of SAT solvers with Polysemy, you're more than welcome to use them as regression tests lol

[lexi-lambda]

Good news, folks—ListT’s totally broken, too, so at least you aren’t alone:

ghci> runExcept . ListT.toList $
        (pure 1 <|> throwError ()) `catchError` \() -> pure 2
Left ()

[lexi-lambda]

Even better, LogicT is broken, too:

ghci> let printAsk = liftIO . print =<< ask in
      flip runReaderT 12 $ observeAllT $ local (* 5) ((printAsk $> 1) <|> (printAsk $> 2))
60
12
[1,2]

[isovector]

everything is broken!!!

[lexi-lambda]

everything is broken!!!

Indeed… except for, as of approximately ten minutes ago, my branch of eff:

ghci> let printAsk = liftIO . print =<< ask @Integer in
        runReader @Integer 12 $ runNonDetAll @_ @[] $ local @Integer (* 5) $
          (printAsk $> 1) <|> (printAsk $> 2)
60
60
[1,2]

But wait, there’s more:

specify "lazy fold with scoped operations" $ do
  let takeNonDet :: forall m a. Monad m => Integer -> EffT NonDetT m a -> m [a]
      takeNonDet n xs0 =
        let next :: Integer -> m (Integer -> m [a]) -> m [a]
            next m xs
              | m < n     = xs >>= ($ m)
              | otherwise = pure []
            go x xs = pure $ \m -> (x :) <$> next (m + 1) xs
        in next 0 $ foldrNonDet go (pure $ \_ -> pure []) xs0

      results = runIdentity $ runWriter @[String] $ runReader True $ takeNonDet 6 $ do
        x <- ask <|> local not ((tell ["three"] *> ask) <|> (tell ["four"] *> ask))
        tell ["one"]
        y <- local not (ask <|> (tell ["two"] *> ask)) <|> ask
        pure (x, y)

  results `shouldBe`
    ( [ "one"
      , "two"
      , "three"
      , "one"
      , "two" ]
    , [ (True, False)
      , (True, False)
      , (True, True)
      , (False, False)
      , (False, False)
      , (False, True)
      ] )

[isovector]

@lexi-lambda very cool! what's the trick?

[lexi-lambda]

Four things:

1. My formulation of NonDetT is the ListT one, where NonDet m a is m (Maybe (a, NonDetT m a)).

2. On my branch, I have ditched MonadTransControl in favor of a less powerful typeclass hierarchy. Currently, the hierarchy consists of the following classes:

   class
     ( MonadTrans t
     , forall m. Functor m => Functor (t m)
     , forall m. Monad m => Monad (t m)
     , forall m r. Functor (HandlerState t m r)
     ) => Handler t where
     data HandlerState t (m :: Type -> Type) r a
     hmap
       :: (Functor m, Functor n)
       => (m (HandlerState t m a a) -> n (HandlerState t m a b))
       -> t m a -> t n b
   
   class Handler t => Scoped t where
     -- | Lifts a scoped operation with support for suspension and resumption.
     scoped
       :: (Functor m, Functor n)
       => ((c -> m (HandlerState t m a a)) -> n (HandlerState t m a b))
       -- ^ Action to run the first time control enters the scoped region.
       -> (m (HandlerState t m a a) -> n (HandlerState t m a b))
       -- ^ Action to run on subsequent reentry into the scoped region.
       -> (c -> t m a) -> t n b
   
   class Handler t => Choice t where
     choice
       :: Functor m
       => t m a -> (m (HandlerState t m a a) -> t m a)
       -- ^ Make a choice by extending the continuation.
       -> ((t m a -> m (HandlerState t m a a)) -> m (HandlerState t m a a))
       -- ^ Make a choice via state threading.
       -> t m a

   These classes cannot lift as many operations, but they are enough to lift all the operations I already have: Reader, State, Writer, Error, NonDet, and Resource. Also, every effect handler I currently have can provide instances of all three classes.

3. Importantly, the above classes provide just enough information for NonDetT to properly thread any lifted operations through the continuation.

   When lifting scoped operations, stateful handlers like StateT and ExceptT need to have their state threaded through the computation and unpacked on the other end. For NonDetT, the situation is more complicated: there isn’t really any state to thread through the computation per se (though the Maybe (a, NonDetT m a) result has many of the same problems), but rather scoped operations must distribute over NonDetT. For example, given an expression like

   local f (e1 <|> e2) >>= k

   evaluation must proceed by distributing the call to local over the branches of execution:

   (local f e1 <|> local f e2) >>= k

   This is also true for more complex scoped operations like catch or mask. A MonadTransControl-like liftWith operation does not capture the continuation in a way that NonDetT can get access to it, leading to dropped operations.

   All the operations in the above classes expose the continuation to NonDetT so that it can be threaded through the other branches. By far the trickiest case is Choice, which supports operations like (<|>) and catch that have a notion of “speculative” execution followed by backtracking. For stateful handlers, this requires an ability to fork the state, so each continuation sees a copy of the state. For NonDetT, however, this doesn’t make sense: you still want (<|>) and catch to distribute over each branch in the usual way. Therefore, Choice requires lifted operations support both use cases explicitly.

4. There’s one more wrinkle in all this, which can be pretty subtle. The aforementioned issue of distributing effects over branches accommodates many operations well enough, but it is insufficient to handle all kinds of interactions, especially ones in IO. The lingering issue has to do with computation resumption.

   To understand the issue, first consider a simple effect like mask_, which masks asynchronous interrupts in a region of code. As long as we take care to distribute this over the suspended branches of a computation, we ought to be alright. For example, if we have mask_ (e1 <|> e2), and we distribute it to produce mask_ e1 <|> mask_ e2, then the masking will be re-introduced when computation backtracks. Good!

   But now consider the more general mask operation, which also provides a restore function to its argument, which unmasks interrupts. This is awfully tricky, as mask has the following type:

   mask :: ((forall a. m a -> m a) -> m b) -> m b

   How do we distribute an operation like mask over a computation? It isn’t entirely obvious. Consider the following expression:

   mask (\f -> e1 f <|> e2 f)

   It seems like the right thing to do is distribute mask to get mask e1 <|> mask e2, and indeed, it would be great if we could do that. But we cannot, as e1 f <|> e2 f is under the lambda, so by the time we have discovered that computation has forked, we have already evaluated the function, and f is bound to the same function in both branches. We can’t somehow “unapply” the function so that f can be rebound inside e2 to a new restore function. This is the unfortunate power of Monad.

   Therefore, operations like these must provide explicit support for resumption. When we suspend a computation inside mask, we must be provided a second operation that is applied upon resumption of the computation, which re-installs the mask and ensures the provided f binding is (imperatively) updated as necessary to work in the new region.

   Fortunately, in the case of mask specifically, we do not need to actually update f in any way, as a quirk of its implementation means it can actually function fine outside of the region created by mask. We do, however, need to re-install the interrupt mask. Therefore, we actually want to distribute mask_ over all suspended branches of the computation, and this is the power the second argument to scoped provides.

You can find all this on the no-monad-control branch of the eff repository. It still needs documentation updates, and a few API details still need to be worked out, but I’m optimistic that the above approach will work out, in spite of the subtlety. This is because, although the details are complex, many of them can be hidden away from general users of the library:

• No users should have to manually implement instances of the above classes unless they are defining entirely new handlers from scratch. If they use HandlerT to define an effect handler in terms of existing handlers, they have to write zero new instances—the instances are effectively automatically inherited from the underlying handlers.

• Lifting algebraic effects is still as easy as before, and it doesn’t involve any of the above complexity. For example, the following instance defines lifting for the State effect:

  instance (Handler t, State s m) => State s (LiftT t m) where
  get = lift get
  put = lift . put
  modify = lift . modify

• Furthermore, although the API of the above classes is not impossible to misuse, it’s much more difficult to unintentionally do so than for MonadTransControl. With documentation in place, it should hopefully guide users towards the right solutions, since it’s much more in-one’s-face about the complexities involved.

I’m also considering providing simpler versions of many of these operations that are easier to use but prohibit nondeterminism, which are likely necessary for certain IO effects anyway. For example, it is not really feasible to implement a withFile effect that allows arbitrary suspension and resumption of the computation—you can’t exactly save and restore all the details about the state of the file handle when backtracking. Therefore, those interactions should be statically disallowed, which is doable by defining another class in the hierarchy without an instance for NonDetT.

Overall, I’m quite positive. Performance is as good as ever—GHC specializes everything with gusto—and the resulting library is both more expressive and safer than existing solutions in the mtl ecosystem, without sacrificing performance. Boilerplate is low, though a tiny bit more has crept in as part of these changes. It’s very minimal, though, and so mechanical that it is trivial to TH away, once I get to that point. Error reporting needs work, though; that’s the next big frontier, and I’m not sure how to make it better just yet. Maybe someone else has some better ideas.

[KingoftheHomeless]

About the v2 milestone -- fixing this means switching from the weave abstraction -- this bug is inherent to it -- and that's too much for v2. However, we should decide upon a temporary fix for v2, most likely sticking a warning onto runNonDet in the documentation -- perhaps even add a WARNING pragma, or deprecate it entirely.