Concurrency hierarchy

[natefaubion]

class (Monad m, Functor t) <= MonadFork t m | m -> t where
  fork :: forall a. m a -> m (t a)
  join :: forall a. t a -> m a

class (MonadFork t m, MonadThrow e m) <= MonadKill e t m | m -> e t where
  kill :: forall a. e -> t a -> m Unit

class (MonadKill e t m, MonadError e m) <= MonadBracket e t m | m -> e t where
  bracket :: forall a b. m a -> (a -> m Unit) -> (a -> m b) -> m b

MonadFork has a fairly obvious law of fork >=> join = id, but I'm not sure what I'd state about the others.

[jdegoes]

MonadKill could have something like the following law:

(attempt do
  f <- fork ma
  kill e f
  join t) == Left e

That is, attempting to join a killed forked thread yields the error it was killed with. Some restrictions on ma might be needed.

Another law for MonadKill might state that for all a:

(attempt do
  f <- fork (pure a)
  kill e f
  join t) == Right a

MonadBracket would take a similar approach and say that the release action is always invoked, even when the body throws an exception (law 1), and even when the thread is killed (law 2). i.e. release is always invoked, whether the body completes normally, is killed from within, or is killed from without.

[jdegoes]

Idea 1: Suspension

type Suspension e = { suspend :: Aff e Unit, resume :: Aff e Unit }

newSuspension :: Aff e (Suspension e)

do
  suspension <- newSuspension
  f <- fork $ suspension.suspend *> ma
  kill e f
  suspension.resume
  r <- attempt $ join t
  r == Left e

Idea 2: Strict & Lazy

fork/join (strict) and suspend/resume (lazy)

Idea 3: Lazy Fork

class (Monad m, Functor t) <= MonadFork t m | m -> t where
  forkSuspended :: forall a. m a -> m (t a)
  join :: forall a. t a -> m a

  suspend :: forall a. t a -> m Unit
  resume :: forall a. t a -> m Unit

  fork :: forall a. m a -> m (t a)
  fork = forkSuspended >>= (\f -> resume f *> pure f)

[jdegoes]

^^^ @natefaubion What other formulations might exist?

[natefaubion]

I think we could just add suspend to MonadFork, because there are useful laws in terms of each other. resume and join are the same thing.

class (Monad m, Functor t) <= MonadFork t m | m -> t where
  suspend :: forall a. m a -> m (t a)
  fork :: forall a. m a -> m (t a)
  join :: forall a. t a -> m a

join <=< suspend = id
fork = fork <<< join <=< suspend

---

class (MonadFork t m, MonadThrow e m) <= MonadKill e t m | m -> e t where
  kill :: forall a. e -> t a -> m Unit

(do t <- suspend (throwError e1)
    kill e2 t
    join t)
  = throwError e2

(do t <- fork (pure a)
    kill e2 t
    join t)
  = pure a

---

data BracketResult e
  = Killed e
  | Failed e
  | Completed

class (MonadKill e t m, MonadError e m) <= MonadBracket e t m | m -> e t where
  bracket :: forall a b. m a -> (BracketResult e -> a -> m Unit) -> (a -> m b) -> m b

-- Wave hands

[jdegoes]

Yes, you're right, sorry. I didn't intend to include resume in that version.

[natefaubion]

In any case, I don't think we need attempt/try to state the laws for MonadKill.

[jdegoes]

Overall, I like it. 👍

What useful things, if any, could a user do with suspend?

[natefaubion]

suspend is useful when you want to preemptively "fork" a computation, but there may not be any consumers to observe it, in which case nothing gets run.

[natefaubion]

So for example, you could build a table of forked effects, but then only observe the results as needed. This means things are only computed on demand and then memoized (at least for Aff).

[natefaubion]

So then perhaps this should be a law:

(do t <- fork a
    _ <- join t
    join t)
  = fork a >>= join

[jdegoes]

The problem with that example is you can bypass the whole suspend / join merely by sequencing the result into the parent. Instead of storing the "suspended" effects, you just store the actions, and instead of joining them, you just run them. The effect is the same.

[natefaubion]

That's not true. With the above law (multiple joins don't run the effect more than once), it's very different. If you stored Aff actions, every time you dereferenced it, an effect would run. With suspend and join, effects are only run once as needed.

[natefaubion]

A real world example, trivial lazy loading with ListT (Aff eff) (Thread eff Result) and suspend.

[natefaubion]

Actually, that example is poor. So you might be right 😆

[natefaubion]

The lazy loading example is useful if you want to share results among multiple consumers. The sequencing an effect thing only applies with a single consumer.

[jdegoes]

Yes, that's right, for more than one consumer, suspend achieves sharing. If there's no rush, let's think it over a day & make sure this is the best law-abiding formulation we can come up with.

[jdegoes]

Unjoined suspension is a no-op

  suspend a1 *> suspend a2 = suspend a2

Killed suspension is an exception 

  suspend a >>= \f -> killFiber e f *> joinFiber f = throwError e

Suspend/join is identity

  suspend >=> joinFiber = id

Fork/join is identity

  fork >=> joinFiber = id

Suspend/kill is unit

  suspend a >>= killFiber e = pure unit

Join is idempotent

  joinFiber f *> joinFiber f = joinFiber f

[natefaubion]

@jdegoes do we want to punt on bracket for now?

[natefaubion]

We can forgo algebraic laws for the time being, and just state operational laws.

[jdegoes]

@natefaubion I think so. The best I came up with was specifying its behavior in the absence of interruptibility:

nonInterruptible $ bracket aff1 f g =
  nonInterruptible $ do
    a <- aff1
    e <- try (g a)
    f a (either Failed Completed e)
    either throwError pure

This is a guarantee that, assuming nothing is interrupted, the release action is always called so long as the acquire action succeeds.

I think stating more than that — that the release action is called if the body is interrupted — cannot be stated algebraically with this formulation, at least, not without a model of Aff. So operational laws are better than nothing and we can always improve this over time.

[natefaubion]

@jdegoes In that case, MonadBracket should just contain bracket for the time being?

[jdegoes]

@natefaubion Can you think of useful laws involving never?

There's some trivial stuff:

bracket (pure a) (\_ _ -> aff) pure == (nonInterruptible aff) *> pure a

bracket never f g == never

bracket (pure a) (\_ _ -> never) pure == never

Not sure how useful it is?

[natefaubion]

I don't think those never laws are very interesting. They would require nonInterruptible anyway, since the acquisition effect can't be killed once it is initiated. So I think if we are going to add another member, nonInterruptible is a more interesting candidate.

bracket a1 (const a2) pure = nonInterruptible (a1 >>= \a -> a2 a $> a)

[natefaubion]

I also think that nonInterruptible works as a member because it has a default implementation in terms of bracket.

[jdegoes]

That makes sense.

Are you sure the above law holds? What if body is interrupted? I know it's just pure but that doesn't mean it can't be interrupted.

[natefaubion]

I think it should be OK, but it would require more laws. If you kill something that is non-interruptible, the action is run, and the exception is deferred until it completes. So in that case, you'd end up with an exception at the end for that Fiber either way. I guess you could use never then to say:

do
  t <- fork (bracket a1 (const a2) never)
  kill e t
  join t
=
  nonInterruptible (a1 >>= a2) *> throwError e

[natefaubion]

Since fork is non-deterministic, unlike suspend, a1 must be initiated.

[natefaubion]

Thinking about this, I'm not sure we can say that fork >=> join or suspend >=> join are equivalent to id in the presence of cancellation. That would require killing a join to kill the subject fiber, which I don't think is desirable behavior.

[jdegoes]

@natefaubion I think we can say fork >=> join, because this says nothing about cancelation. If you literally have fork >=> join in your code, you can always replace that with id. If you do other stuff with the fiber, which means you don't have fork >=> join, but rather something like do { fiber <- fork aff; kill error fiber; join fiber, then all bets are off.

[natefaubion]

OK, that's fair. I was thinking of something similar to that where:

fork (fork aff >>= join) >>= kill e

Is not necessarily the same as:

fork aff >>= kill e

But this ascribes some sort of equivalence to the fork, but the point of fork is that it's non-deterministic.

[natefaubion]

-- Release
bracket a (const k) (const (pure unit))
  = uninterruptible (a >>= k)

-- Release exception
bracket a (const k) (const (throwError e))
  = uninterruptible (a >>= k *> throwError e)

-- Release kill
do
  f <- fork (bracket a (const k) (const never))
  kill e f
  void $ try $ join f
  = uninterruptible (a >>= k)

I used void <<< try at the end because it's not necessarily the same as throwError since the effect may have already completed.

[natefaubion]

With BracketConditions:

-- Release
bracket a k \_ -> pure r
  = uninterruptible (a >>= k (Completed r))

-- Release exception
bracket a k \_ -> throwError e
  = uninterruptible (a >>= k (Failed e) *> throwError e)

-- Release kill
fork (bracket a k \_ -> never) >>= \f -> kill e f *> void (try (join f))
  = uninterruptible (a >>= k (Killed e))