Concurrency hierarchy about purescript-fork HOT 32 OPEN

So then perhaps this should be a law:

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

from purescript-fork.

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.

from purescript-fork.

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)

from purescript-fork.

^^^ @natefaubion What other formulations might exist?

from purescript-fork.

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

from purescript-fork.

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

from purescript-fork.

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

from purescript-fork.

Overall, I like it. 👍

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

from purescript-fork.

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.

from purescript-fork.

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).

from purescript-fork.

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.

from purescript-fork.

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.

from purescript-fork.

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

from purescript-fork.

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

from purescript-fork.

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.

from purescript-fork.

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.

from purescript-fork.

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

from purescript-fork.

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

from purescript-fork.

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

from purescript-fork.

@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.

from purescript-fork.

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

from purescript-fork.

@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?

from purescript-fork.

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)

from purescript-fork.

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

from purescript-fork.

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.

from purescript-fork.

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

from purescript-fork.

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

from purescript-fork.

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.

from purescript-fork.

@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.

from purescript-fork.

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.

from purescript-fork.

-- 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.

from purescript-fork.

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))

from purescript-fork.