Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Concurrency hierarchy #4

Open
natefaubion opened this issue Jul 22, 2017 · 32 comments
Open

Concurrency hierarchy #4

natefaubion opened this issue Jul 22, 2017 · 32 comments

Comments

@natefaubion
Copy link
Collaborator

natefaubion commented Jul 22, 2017

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
Copy link

jdegoes commented Aug 7, 2017

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
Copy link

jdegoes commented Aug 7, 2017

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
Copy link

jdegoes commented Aug 7, 2017

^^^ @natefaubion What other formulations might exist?

@natefaubion
Copy link
Collaborator Author

natefaubion commented Aug 7, 2017

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
Copy link

jdegoes commented Aug 7, 2017

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

@natefaubion
Copy link
Collaborator Author

natefaubion commented Aug 7, 2017

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

@jdegoes
Copy link

jdegoes commented Aug 7, 2017

Overall, I like it. 👍

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

@natefaubion
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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
Copy link
Collaborator Author

So then perhaps this should be a law:

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

@jdegoes
Copy link

jdegoes commented Aug 7, 2017

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
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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

@natefaubion
Copy link
Collaborator Author

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

@natefaubion
Copy link
Collaborator Author

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
Copy link

jdegoes commented Aug 7, 2017

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
Copy link

jdegoes commented Sep 6, 2017

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
Copy link
Collaborator Author

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

@natefaubion
Copy link
Collaborator Author

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

@jdegoes
Copy link

jdegoes commented Sep 6, 2017

@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
Copy link
Collaborator Author

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

@jdegoes
Copy link

jdegoes commented Sep 7, 2017

@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
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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

@jdegoes
Copy link

jdegoes commented Sep 7, 2017

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
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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

@natefaubion
Copy link
Collaborator Author

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
Copy link

jdegoes commented Sep 7, 2017

@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
Copy link
Collaborator Author

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
Copy link
Collaborator Author

-- 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
Copy link
Collaborator Author

natefaubion commented Sep 12, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

No branches or pull requests

2 participants