diff options
Diffstat (limited to 'plt')
| -rw-r--r-- | plt/effects.md | 180 |
1 files changed, 116 insertions, 64 deletions
diff --git a/plt/effects.md b/plt/effects.md index ef97667..f1f73f1 100644 --- a/plt/effects.md +++ b/plt/effects.md @@ -3,48 +3,51 @@ layout: plt title: computation/effects --- -# effects and handlers: a comprehensive introduction +# algebraic effects and effect handlers What are effects? -Effects are a lot of things. Like other terms in computer science, it is overloaded, and refers typically to two similar but notably different concepts: -1. a *side* effect, i.e. some sort of impurity in the computation of an otherwise [pure function] -2. an *algebraic effect*. We'll get back to this later. +Effects are a lot of things. Like other terms in computer science, it is overloaded, and refers typically to two similar but notably distinct concepts: +1. a *side* effect, i.e. some sort of impurity in the computation of an otherwise [pure function](/wiki/plt/glossary#pure) +2. an *algebraic effect*. These are occasionally referred to as *abilities* or *capabilities*. -<!-- The term "effects system" gets thrown around with "effects" a lot. --> -What is an effects system? +The term "effects system" gets thrown around with "effects" a lot. But what is an effects system? -Effects systems, too, are a couple of things. +Effects systems, too, are a couple of things: 1. a system for *tracking side-effects* of routines -2. for algebraic effects and alongside **handlers**, a *broad generalization of non-local control flow*. +2. for algebraic effects and alongside *handlers*, a **broad generalization of non-local control flow**. By "effects system", most programmers generally mean the first. Academics near-universally mean the second. [This can be the cause of some confusion.](https://github.com/nim-lang/RFCs/issues/491) -... +## toc - [Background](#background) -- [An Intuition](#an-intuition-exceptions-as-an-effect) (exceptions as an effect) -- [Resuming Continuations](#resuming-continuations-iteration-as-an-effect) (iteration as an effect) -- [Resumption with a Value](#resuming-with-a-value-io-as-an-effect) (i/o as an effect) -- [...]() (mutable global state as an effect) -- [Subsuming Effects Tracking](#subsuming-effects-tracking-safety-as-an-effect) (safety as an effect) -- [Multiple Resumptions](#multiple-resumptions-nondeterminism-as-an-effect) (nondeterminism as an effect) -- [Communication Protocols](#communication-protocols-ping-pong-as-effects) (ping/pong as effects) -- [Colourless Functions](#colourless-functions-async-as-an-effect) (async as an effect) -- [Unified Control Flow Semantics](#unified-control-flow-semantics-async-await-as-an-effect) (async/await as an effect) -- [Why Not Undelimited Control?](#why-not-undelimited-control-effects-as-a-sweet-spot) (effects as a sweet spot) -- [Some Design Considerations](#some-design-considerations-for-future-effectful-systems) (for future effectful systems) +- [An Intuition](#an-intuition) (exceptions as an effect) +- [Resuming Continuations](#resuming-continuations) (iteration as an effect) +- [Resumption with a Value](#resuming-with-a-value) (i/o as an effect) +- [Side Effects are Effects, Too](#side-effects) (mutable global state as an effect) +- [Subsuming Effects Tracking](#subsuming-effects-tracking) (safety as an effect) +- [Multiple Resumptions](#multiple-resumptions) (nondeterminism as an effect) +- [Communication Protocols](#communication-protocols) (ping/pong as effects) +- [Colourless Functions](#colourless-functions) (async as an effect) +- [Unified Control Flow Semantics](#unified-control-flow-semantics) (async/await as an effect) +- [What is Algebraic About Algebraic Effects?](#algebraic-effects) +- [Why Not Undelimited Control?](#undelimited-control) (effects as a sweet spot) +- [Some Design Considerations](#some-design-considerations) (for future effectful systems) ## background -Effects-and-handlers systems are *experimental*, even within computer science academia. There are scant few languages implementing them, and they all do so with their own unique quirks: -Koka (and Frank) have complexities around parametric effect polymorphism, while OCaml (and Eff) handlers are untyped as to satisfy backwards compatibility... +Effects-and-handlers systems are *experimental*, even within academia. There are scant few languages implementing them, and they all do so with their own unique quirks: Koka (and Frank) have complexities around parametric effect polymorphism, while OCaml (and Eff) handlers are untyped as to satisfy backwards compatibility. There is a lot of unexplored ground around soundness and usability! Out of existing languages, though, I think [**Effekt**](https://effekt-lang.org) does the best job. The examples throughout this entry are given in Effekt. They compile, and run, and I encourage the reader to download and play around with Effekt themselves. (I have also given corresponding examples in a syntax of my own division. These examples neither compile nor run, but are meant to illustrate what a future system could look like.) If sitting down and working through a paper appeals to you, I recommend watching/reading, in the following order: -- [✨ Deliminated Continuations, Demystified](https://www.youtube.com/watch?v=TE48LsgVlIU) (fundamental ideas of continuations; which effects handlers build atop) -- [✨ Effects as Capabilities: Effect Handlers and Lightweight Polymorphism](https://dl.acm.org/doi/pdf/10.1145/3428194) ([talk](https://www.youtube.com/watch?v=ITRyzJadgMw) (the Effekt programming language; drastically simplifies polymorphism in such systems) -- [✨ Handling Bidirectional Control Flow] ([talk](https://www.youtube.com/watch?v=RLTEuZNtRCc)) (generalization of exceptions to capture mutating iterators; good exceptions+async example) -- [✨ Continuing WebAssembly with Effect Handlers](https://arxiv.org/pdf/2308.08347) ([talk](https://www.youtube.com/watch?v=2iiVhzzvnGA)) (a compilation target for effectful languages) +- [✨ Deliminated Continuations, Demystified](https://www.youtube.com/watch?v=TE48LsgVlIU) + - fundamental ideas of continuations; which effects handlers build atop +- [✨ Effects as Capabilities](https://dl.acm.org/doi/pdf/10.1145/3428194) ([talk](https://www.youtube.com/watch?v=ITRyzJadgMw) + - the Effekt programming language; drastically simplifies polymorphism in such systems +- [✨ Handling Bidirectional Control Flow](https://dl.acm.org/doi/pdf/10.1145/3428207) ([talk](https://www.youtube.com/watch?v=RLTEuZNtRCc)) + - generalization of exceptions to capture mutating iterators; good exceptions+async example; implemented in Effekt +- [✨ Continuing WebAssembly with Effect Handlers](https://arxiv.org/pdf/2308.08347) ([talk](https://www.youtube.com/watch?v=2iiVhzzvnGA)) + - an efficient compilation target for effectful languages These are all very recent papers (all in the last ~5 years). This is kind of surprising! The idea of effects and handlers has been around since at least the 90s. But it seems that computer science academia is only now getting a handle on how to coherently present and implement such systems: thanks in large part to the hard work of the authors of these papers (and thanks in larger part, of course, to the authors of the papers they in turn built upon). @@ -54,18 +57,41 @@ This is all covered in much more depth in Alexis King's excellent talk on contin - **continuations**: "the rest of the program". Evaluation can be broken up into reducing *redexes* (reducible expressions) and substituting them back into their corresponding *continuations*. - For example, consider `(1 + 2) * 3`. - - We can consider `(1 + 2)` a redex with continuation `∙ * 3`. Evaluation proceeds by reducing `(1 + 2)` to `3` and substituting it into the hole of the continuation `∙ * 3`, giving us `3 * 3`. - - We can consider `3 * 3` a redex with continuation `∙`. Evaluation proceeds by reducing `3 * 3` to `9` and substituting it into the hole of the empty continuation `∙`, giving us the value `9`. -- **deliminated continuations**: continuations that are split up and *manipulated*. + - We can consider `(1 + 2)` a redex with continuation `● * 3`. Evaluation proceeds by reducing `(1 + 2)` to `3` and substituting it into the hole of the continuation `● * 3`, giving us `3 * 3`. + - We can consider `3 * 3` a redex with continuation `●`. Evaluation proceeds by reducing `3 * 3` to `9` and substituting it into the hole of the empty continuation `●`, giving us the value `9`. +- **delimited continuations**: continuations that are split up (delimited) and *manipulated*. - For example, consider `exit(1) * 3`. - - We can consider `exit(1)` a redex with continuation `∙ * 3`. Evaluation proceeds by hitting `exit(1)`: which *discards* the continuation `∙ * 3`, and thus exits. - - This treatment of continuations as a thing + - We can consider `exit(1)` a redex with continuation `● * 3`. Evaluation proceeds by hitting `exit(1)`: which *discards* the continuation `● * 3`, and thus exits. - For a better example, consider [`1 + catch(2 * throw(5), (n) => 3 * n)`](https://www.youtube.com/watch?v=TE48LsgVlIU&t=840s). -- **one-shot continuations**: continuations that may be continued only once. The prototypical idea of a continuation is a one-shot continuation. -- **multi-shot continuations**: continuations that may be continued multiple times. See [Multiple Resumptions](#multiple-resumptions-nondeterminism-as-an-effect) for an example. +- **one-shot continuations**: continuations that may be continued *only once*. + - The prototypical idea of a continuation is a one-shot continuation. +- **multi-shot continuations**: continuations that may be continued *multiple times*. + - See [Multiple Resumptions](#multiple-resumptions-nondeterminism-as-an-effect) for an example. - **effectful**: having to do with effects, vaguely. -## an intuition: exceptions as an effect +<h2 id="an-intuition"> an intuition: exceptions as an effect</h2> + +```scala +// FIXME: does not compile!! why?? +interface Exception[E] { + def Exception[T](msg: E): T +} + +def raise[E, T](err: E): T / Exception[E] = + do Exception(err) + +def catch[E, T]{action: () => T / Exception[E]}{handler: E => T}: T = + try action() + with Exception[E] { (err) => handler(err) } + + +def default[E, T](value: T){action: () => T / Exception[E]} = + catch { action() } { err => value } +``` + + +<details> +<summary> puck </summary> ```puck pub mod exceptions = @@ -111,7 +137,9 @@ assert 5.div(0).to_err() == Error("div-by-zero") assert 0.div(5).to_err().to_exn() == 0 ``` -## resuming continuations: iteration as an effect +</details> + +<h2 id="resuming-continuations"> resuming continuations: iteration as an effect </h2> This suspend-and-resume model is a *very good* model of iteration... @@ -194,7 +222,7 @@ pub func iter[T](self: List[T]) = </details> -## resuming with a value: io as an effect +<h2 id="resuming-with-a-value"> resuming with a value: io as an effect </h2> Side effects are effects, too! @@ -223,7 +251,7 @@ pub mod io return do(Input) # (2) suspends here @[handler] - func handle_output[T](action: () -> T {Output}) = + func handle_output[T](action: () -> T {Output}) = try action() with Output(msg) => std.primitive.write(msg) @@ -257,7 +285,7 @@ hello().handle_input().handle_output() </details> -## mutable global state as an effect +<h2 id="side-effects"> side effects are effects, too: mutable global state as an effect </h2> ```puck type State[T] = effect @@ -265,11 +293,11 @@ type State[T] = effect Put(S) ``` -## subsuming effects tracking: safety as an effect +<h2 id="subsuming-effects-tracking"> subsuming effects tracking: safety as an effect </h2> The Rust programming language famously distinguishes between *safe* and *unsafe* functions. Safe functions may be called freely, while unsafe functions "poison" their called context unless explicitly wrapped in an `unsafe{}` block. This abstraction has been praised for providing for a separation of concerns, making it easier to build safe abstractions and track down bugs that result from unsafety when things go wrong. -We can implement such a system with effects-and-handlers. +We can implement such a system as a library with effects-and-handlers. ```scala interface Unsafe { @@ -369,54 +397,78 @@ pub mod io = ... ``` -Well, that was straightforward. Neat. +<h2 id="multiple-resumptions"> multiple resumptions: nondeterminism as an effect </h2> -## multiple resumptions: nondeterminism as an effect +<h2 id="modification-of-iterators"> modification of iterators: yield as an effect </h2> -## modification of iterators: yield as an effect +<h2 id="communication-protocols"> communication protocols: ping/pong as effects </h2> -## communication protocols: ping/pong as effects - -## colourless functions: async i/o as an effect +<h2 id="colourless-functions"> colourless functions: async i/o as an effect </h2> We've now arrived at the *real* interesting stuff. Effects-and-handlers systems promise -## unified control flow semantics: async/await as an effect +<h2 id="unified-control-flow"> unified control flow semantics: async/await as an effect </h2> + +<h2 id="algebraic-effects"> what is algebraic about algebraic effects? </h2> -## why not undelimited control? effects as a sweet spot +<h2 id="undelimited-control"> why not undelimited control? effects as a sweet spot </h2> delimited control is *compositional*. -## some design considerations for future effectful systems +<h2 id="design-considerations"> some design considerations for future effectful systems </h2> There are a couple of things I have realized while learning about these effects-and-handlers systems. -1. Effekt and their system of "lightweight polymorphism" is entirely correct. Effects **should be treated as capabilities**. This is simply the correct approach. +1. Effects **should be treated as capabilities**. This is simply the correct approach. Effekt and their system of "lightweight polymorphism" is entirely correct. + +2. Syntax is **incredibly important**. Having a language with succinct and flexible syntax, like Effekt (or like my fake language ;->), is an absolute necessity for a language built atop an effects system. Effects-and-handlers should be able to disguise themselves as constructs programmers are *already familiar with*. Because they are! The point of having an effects system is that it subsumes other *existing* systems of non-local control flow: you want the semantics (and syntax) of those systems to stay the same, not bow and twist to the whims of a low-level system most are unfamiliar with. Syntax somewhat leads into the next point: + +3. I think there is a very very good argument for **never exposing effects to end users**. To be more precise, disallowing the use of `try`/`with`/`do`/`resume` on exceptions *outside of the module in which they are defined*. They are a powerful primitive: but in my opinion, should remain a low-level one, as it is all too easy to break function abstraction (consider the resumption examples above) and thus any sort of user encapsulation. + -2. Syntax is **incredibly important**. Having a language with succinct and flexible syntax, like Effekt (or like my fake language ;->), is an absolute necessity for a language with an effects system. Effects-and-handlers should look like constructs programmers are already familiar with. Having a language with flexible syntax is also helpful for the next point: -3. I think there is a very very good argument for **never exposing effects to end users**: to be more precise, disallowing the use of `try`/`with`/`do`/`resume` on exceptions *outside of the module* in which they are defined. They are a low-level primitive, and an excellent one, but it is all too easy to *break function abstraction* and user encapsulation. -# effects +## resources posts -- [Oleg Kiselyov's writings](https://www.okmij.org/ftp/) -- [Exotic Programming Ideas: Effect Systems](https://www.stephendiehl.com/posts/exotic03.html) +- [✨ Effect bibliography](https://github.com/yallop/effects-bibliography) +- [✨ Oleg Kiselyov's writings](https://www.okmij.org/ftp/Computation/having-effect.html) +- [Exotic programming ideas: Effect Systems](https://www.stephendiehl.com/posts/exotic03.html) - [Faking algebraic effects and handlers with traits](https://blog.shtsoft.eu/2022/12/22/effect-trait-dp.html) - [From deliminated continuations to algebraic effects](https://blog.poisson.chat/posts/2023-01-02-del-cont-examples.html) -- [OCaml effects tutorial](https://github.com/ocaml-multicore/ocaml-effects-tutorial) -- [Simple functional effects with tag unions](https://www.youtube.com/watch?v=7SidSvJcPd0) -- [Effect bibliography](https://github.com/yallop/effects-bibliography) +- [Algebraic effects for the rest of us](https://overreacted.io/algebraic-effects-for-the-rest-of-us/) papers -- [What is algebraic about algebraic effects and handlers?](https://arxiv.org/abs/1807.05923) -- [Asynchronous effects](https://dl.acm.org/doi/10.1145/3434305) +- [✨ Effects as Capabilities (2020)](https://dl.acm.org/doi/pdf/10.1145/3428194) +- [✨ Handling Bidirectional Control Flow](https://www.cs.cornell.edu/andru/papers/ufo/bidirectional-effects.pdf) +- [✨ Continuing WebAssembly with Effect Handlers (2023)](https://arxiv.org/pdf/2308.08347) +- [📋 Effects, Capabilities, and Boxes (2022)](https://dl.acm.org/doi/pdf/10.1145/3527320) +- [📋 Asynchronous effects (2020)](https://dl.acm.org/doi/10.1145/3434305) +- [📋 What is algebraic about algebraic effects and handlers?](https://arxiv.org/abs/1807.05923) +- [📕 An Introduction to Algebraic Effects and Handlers (2015)]() +- [📕 (Koka) Algebraic Effects for Functional Programming (2016)](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/algeff-tr-2016-v2.pdf) +- [📕 (Koka) Structured Asynchrony with Algebraic Effects (2017)](https://www.microsoft.com/en-us/research/wp-content/uploads/2017/05/asynceffects-msr-tr-2017-21.pdf) + +talks +- [✨ Deliminated Continuations, Demystified](https://www.youtube.com/watch?v=TE48LsgVlIU) +- [📋 Effects as Capabilities](https://www.youtube.com/watch?v=ITRyzJadgMw) +- [📋 Handling Bidirectional Control Flow](https://www.youtube.com/watch?v=RLTEuZNtRCc) +- [📋 Continuing WebAssembly with Effect Handlers](https://www.youtube.com/watch?v=2iiVhzzvnGA) +- [📋 Effects for Less](https://www.youtube.com/watch?v=0jI-AlWEwYI) +- [📋 Simple functional effects with tag unions](https://www.youtube.com/watch?v=7SidSvJcPd0) + +tutorials +- [📕 (Unison) Introduction to Abilities](https://www.unison-lang.org/docs/fundamentals/abilities/) +- [📖 (OCaml) Concurrent Programming with Effect Handlers](https://github.com/ocaml-multicore/ocaml-effects-tutorial/) +- [📖 (OCaml) Language extensions: Effect Handlers](https://kcsrk.info/webman/manual/effects.html) languages +- [✨ WasmFX](https://wasmfx.dev/) +- [✨ Effekt](https://effekt-lang.org/) - [Koka](https://koka-lang.github.io/koka/doc/book.html) -- [Effekt](https://effekt-lang.org/) -- [Eff](https://www.eff-lang.org/) +- [OCaml](https://ocaml.org/) + - [Eff](https://www.eff-lang.org/) - [Unison](https://www.unison-lang.org/) -- [Effect handlers for WebAssembly](https://wasmfx.dev/) -- [Coeffects: Context-aware programming languages](https://tomasp.net/coeffects/) +- [F*](https://www.fstar-lang.org/) ([paper](https://fstar-lang.org/papers/mumon/)) +- [Coeffects](https://tomasp.net/coeffects/) |