Consider adding a _different_ effect that holds an implicit `Scope`

[michaelpj]

In https://github.com/TristanCacqueray/ki-effectful/issues/1 and https://github.com/TristanCacqueray/ki-effectful/issues/6 we went back and forth on whether or not StructuredConcurrency should hold a Scope.

I wonder whether we might want to just have a different effect (straw name: Scoped) that holds a Scope. That is:

• StructuredConcurrency tells us that the computation may create structured concurrency scopes
• Scoped tells us that a computation is actually running in a structured concurrency scope.

This isn't an unusual pattern, it's a bit like having one effect that says "you can access the database" and one effect that says "you are in a transaction".

Concretely, this might look like this:

module Ki.Effectful.Implicit where

data Scoped :: Effect

scoped :: StructuredConcurrency :> es => Eff (Scoped : es) a -> Eff es a

fork :: Scoped :> es => Eff es a -> Eff es (Thread a)

Why do this? Well, it seems to me that Scope is a handle for a local effect, namely spawning threads into the scope you created. We have a bit of a split in the effect-systems community about whether we like explicit handles (bluefin-style) or constraints (effectful-style). Since effectful tends to go for managing effect handles using constraints, perhaps it is more idiomatic to do that for Scopes.

What about the worry in https://github.com/TristanCacqueray/ki-effectful/issues/6 ? My take on that is that the suspicious thing is taking a Scope as an argument to a top-level. The only change with Scoped would be that having Scoped as a constraint on a top-level function would be a bit suspicious. Perhaps it makes it seem more natural to inherit Scoped constraints, and that's bad? But that seems like an education problem, much like it seems natural to pass around Scopes, but maybe that's bad.

Plus, because Scoped is a separate effect, you can still run everything in local scopes perfectly well. And we can provide both styles without them interfering with each other.

[TristanCacqueray]

Hello @michaelpj,

That sounds good to me. However, while this should fix #6, I'm concerned about the increased complexity. For example:

• The types doesn't guarantee that a new scope obtained after calling scoped will take precedence over an existing Scoped constraint. It seems like this boil down to the implementation of consEnv and I would worry this may not work as expected.

• How to fork into a higher scope, do we also need to bring back (from #2):

-- | Provide a callback function to run an action within the current `Scope`.
withCurrentScope ::
    Scoped :> es =>
    ((forall es' a. Scoped :> es' => Eff es' a -> Eff es' a) -> Eff es b) ->
    Eff es b
withCurrentScope f = do
    rep <- getStaticRep @Scoped
    f (localStaticRep (const rep))

• Should the Scoped constraint allow using atomically? It looks like we would need a dedicated STM effect to make this cleaner.

I wouldn't mind integrating this new design to see how it works in practice, though I have to say that I'm not using this library. I was hoping to pull it in Butler, but I'm still debating the complexity cost of an effect system.

So I'd love to get the opinion of @mmhat and @mitchellwrosen on this new design. Perhaps @arybczak could tell us if having a new STM effect would make sense too.

Thanks!

[arybczak]

Perhaps @arybczak could tell us if having a new STM effect would make sense too.

For the record, effectful puts atomically into the Concurrent effect. IIRC I did it since if you use STM, you work with threads so you'd need stuff from Concurrent anyway.

[michaelpj]

The types doesn't guarantee that a new scope obtained after calling scoped will take precedence over an existing Scoped constraint.

I think they do. What I'm proposing is really just a synonym for Reader Scope, and it should work just as well (or not) as that. I think it will all work out fine: if you have another Scoped effect in the tail of your effects but you can't see it, you won't use it! If you want to access two you need to use labelled effects (just like for Reader).

How to fork into a higher scope, do we also need to bring back

I'm not sure I'm understanding the use case, but if you want to have two Scoped effects and chose which one to fork into, then you can just use labelled effects (again, see Reader).

Should the Scoped constraint allow using atomically? It looks like we would need a dedicated STM effect to make this cleaner.

Awkward. Arguably you in fact only need STM in Scoped, not StructuredConcurrency, if all you're using it for is to await scopes!

But I do agree this would be nicer with a STM effect.

IIRC I did it since if you use STM, you work with threads so you'd need stuff from Concurrent anyway.

I think there are interesting cases here. One is if you have some code that will run in a multi-threaded scenario, but is itself single-threaded. Such code often reads and writes TVars, but doesn't need the full power of Concurrent. Similarly, in the scenario we are thinking of here, we have code which does only structured launching of threads, or maybe none at all (in the case of Scoped), but needs STM. So I think there is some value...

[arybczak]

The types doesn't guarantee that a new scope obtained after calling scoped will take precedence over an existing Scoped constraint.

I think they do.

Correct, given E :> es => Eff (E : es) a when you make use of E, the first one on the list is picked (to access the underlying one at this point you need raise). This is the only way :> can work for effect lookup, implementation of consEnv isn't a factor.

[mitchellwrosen]

I'm afraid I don't have too much to add to the discussion here beyond the scattered thoughts in #6 and in a few discussions, but regarding this:

Scoped tells us that a computation is actually running in a structured concurrency scope.

I will note that Scoped wouldn't exactly mean "is running in a structured concurrency scope" but rather "can spawn threads into an implicitly-passed structured concurrency scope".

"Running a structured concurrency scope" isn't captured in the type system in any of these variants as far as I understand: it's just an IO action.

And remember: a scopes form a tree; it's not just zero or one. So the type system ought not to prevent a thread from creating a scope just because it itself has been created in a scope, or something like that. (Hand-waving a bit here because I'm not that familiar with this effect system).

I can certainly imagine Reader Scope being put to good work, but I happen to have avoided that design in my own work in favor of an explicit Scope object.

Cheers!

[TristanCacqueray]

Thank you for taking the time to provide your feedback. I really appreciate it!

I think @michaelpj meant that Scoped guarantees forks don't leak. I'd be curious to see a use-case where you wouldn't want the StructuredConcurrency effect too.

Thank you for introducing labeled effects, that looks useful, though I'm not sure how I would use that in butler. My use-case is for a helper function (code) to create a kill-able 'Process', using the hitman trick from https://github.com/awkward-squad/ki/discussions/12#discussioncomment-3394438 . This helper takes an optional parent process to enable building a process hierarchy along side ki machinery. Therefor I need to pick the parent scope based on the parameters. I guess this helper could be implemented differently, but I worry such usage become too complicated when using type level effect to carry the scope.

Additionally, I’m cautious about the debugging experience. I had to take this helper apart to reproduce https://github.com/awkward-squad/ki/issues/19 , and having an explicit scope helped the investigation.

That being said, I’m open to being persuaded otherwise, but Scoped looks like a significant type-level work for a marginal gain at the term-level.

[michaelpj]

I think @michaelpj meant that Scoped guarantees forks don't leak.

I hadn't thought about that, but I guess it is somewhat true: if you have only Scoped and not StructuredConcurrency then you can fork into the scope but not create new ones. I'm not sure how useful that is.

Thank you for introducing labeled effects, that looks useful, though I'm not sure how I would use that in butler

Our use case is pretty much the one I describe here: https://github.com/awkward-squad/ki/discussions/35

To be honest, my main motivation is the abstract one I gave in the original post about how we track effect handles. Scopes look like effect handles and so I feel like I should be putting them in constraints! But it's not exactly a big deal.