Bounded asynchronous effects that don't discard effectful state; e.g. race effect

[KingoftheHomeless]

I thought of the possibility of having effects that do asynchronous computations in a bounded setting, such that the resulting effectful state from a particular asynchronous computation may be used at the end, and don't need to be discarded using the inspector.

The most obvious such effect would be a Race effect:

import qualified Control.Concurrent.Async as A

data Race m a where
  Race  :: m a -> m b -> Race m (Either a b)
  Delay :: Int -> Race m ()

makeSem ''Race

raceToIOFinal
  :: Member (Final IO) r
  => Sem (Race ': r) a
  -> Sem r a
raceToIOFinal = interpretFinal $ \case
  Race left right -> do
    left' <- runS left
    right' <- runS right
    pure (either (fmap Left) (fmap Right) <$> A.race left' right')
  Delay i -> liftS (threadDelay i)

In a race, only the effectful state of the losing computation would be discarded, rather than the effectful state of both computations. Plus, there's no Maybe pollution.

I feel like it should be possible to have more effects that work in a similar way, such that effectful state don't always need to be discarded, but I can't think of anything else at the moment.

[isovector]

I'm not super sure what the takeaway here is. Can we not implement this today?

[KingoftheHomeless]

Async needs to discard the effectful state of any asynchronous computations you launch using it (local state when using asyncToIO; local and global when using asyncToIOFinal). However, certain special uses of asynchronous computations can be interpreted such that they don't always need to discard effectful state; one such use is race. race implemented in terms of Async needs to discard the effectful state of both branches; however, if you interpret it in terms of Final IO directly, you can keep the effectful state of the winning branch.

Bottom line, we may want to add effects like Race that are basically specialized uses of Async but don't require using the inspector when interpreting them

[isovector]

I understand what's happening here. Legitimately you're a month ahead of me :) I'm starting to think you should just start merging good ideas, and I can stop being an unnecessary bottleneck.

That being said, I'm coming around to the idea that effects should come with associated laws. I'm not sure what one would look like here, especially wrt delay.

[KingoftheHomeless]

So this effect was intended to be a slightly generalized variant of the Alternative instance of Control.Concurrent.Async.Concurrently, which has empty = forever $ threadDelay maxBound. So indeed, the only compelling laws I can think of is the associativity of race and that forever $ delay maxBound is a neutral element to race. In fact, I'm considering that delay should be represented in a separate effect from race, and if so you lose the neutral-element law.

My motives for a Race effect is that it'd be a nice part of the ecosystem. There are the traditional points of representing race as an effect rather than lifting it using Final IO:

1. You may use it instead of Final IO in application code
2. Mocking purposes.

But the big thing in my eyes is that it'd compose nicely with other effects that do IO-based blocking. An example would be an effect for delay, or effects that do blocking communication between threads such as through MVars. That way you could do stuff like delaySeconds 0.5 `race` blockingOperation in application code.