carbon-language / carbon-lang

Carbon Language's main repository: documents, design, implementation, and related tools. (NOTE: Carbon Language is experimental; see README)
http://docs.carbon-lang.dev/
Other
32.24k stars 1.48k forks source link

Algebraic Effect Handlers as a General Control flow mechanism #2840

Open TimWhiting opened 1 year ago

TimWhiting commented 1 year ago

Summary of issue:

This is a language feature request. What are the opinions of the leads about having a general control flow mechanism that is extensible by users? Delimited continuations is one approach - which were implemented for a time in #368. A more recent general control flow mechanism which provides a more structured and type safe approach to delimited continuations is Algebraic Effects. Are the leads familiar with work on Algebraic Effects, and what are the opinions about using algebraic effects to implement general control flow mechanisms?

Algebraic Effect Handlers are a general control flow mechanism, which unifies many different control flow operators, and makes control flow more user extensible. They allow users to define async / await, coroutines / schedulers, exceptions, generators, etc in a typed and composable way that can be efficiently compiled. While they were born out of functional language research, there are libraries showing their use in languages such as Scala, C++, and even C library.

Details:

Pros:

Cons:

Any other information that you want to share?

Further Information: A good overview in one research language can be found here. There are different approaches to type systems, but I think possibly the C++ library linked at the top of the issue could be one place to draw inspiration for including this feature in a language that isn't 'purely functional'.

Implementation: They can be built on top of delimited continuations which were added to the Carbon interpreter here (https://github.com/carbon-language/carbon-lang/pull/368.), but there are more efficient ways of implementing them as well: google scholar link to papers - Specifically I'd recommend looking at Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C.

geoffromer commented 1 year ago

Can you be more specific about what question you want the leads to resolve, or what decision you want them to make?

TimWhiting commented 1 year ago

I updated the first paragraph to be an explicit question.

clavin commented 1 year ago

(Aside: Happy to see another Utahn popping their head up in this project! And I was looking into Koka just months ago too! Greetings from SLC 🙂)

I'm not a lead here, but in the project milestones document the features involving effects are explicitly deferred until later in Carbon's development:

Features explicitly deferred until at least 0.2

  • ...
  • Coroutines, async, generators, etc.
  • Comprehensive story for handling effects, and how functions can be generic across effects

(Emphasis mine.)

Granted, there is no explicit mention of user-defined effects or a full effects system. Still, these milestones were drafted by the leads, so I take it that they're aware of the problem space. This excerpt also indicates that effects are, at most, low priority at the moment (deferred to the 0.2 milestone), thus it may be a while before this problem space gets adequate attention in Carbon.

To bring up an example of effects in other languages for discussion, OCaml 5.0 recently released with runtime support for effects. At present, there is no syntax associated with effects in OCaml. It may be sufficient for Carbon to follow this route, providing the machinery but not necessarily any syntax, even if just for a phase of the design of effects. This approach is similar to the C++ library referenced in the OP.

I'd also like to point out that many of the references in the OP involve Daan Leijen (github profile), a researcher currently at Microsoft Research.

For anyone unfamiliar, Daan Leijen has contributed numerous research papers on the topic of algebraic effects (among others) and has a strong background in Programming Language Design, Type Systems, and Effect Typing. Prominently, Daan has contributed the research language Koka, which features effect types and handlers (among other impressive language features). I wouldn't be surprised if the leads already know of Daan and/or their work! 😁


To add my own commentary:

Playing with Koka, I found the effects system to be very intuitive and simple to use. I would love to see user-defined effects make their way into Carbon's design, but I will admit I have no idea what that design or proposal would look like in practice.

I feel like algebraic effects are still in their "research language" phase, which makes it tough for me to currently see how they'd fit into a language like Carbon that, similar to C++, wants to be very practical. Working with effects is a little bit of a paradigm shift, and it's not one that I've personally wrapped my head fully around yet. It doesn't help that effects don't have mainstream patterns and well-known usages yet. I can only hope this gets better with time, especially as Carbon develops past 0.1 and is able to address this problem space with more resources and knowledge. 🤞

(Fun fact: Daan Leijen is one of the authors of the popular Haskell parser combinator library, Parsec.)