diff options
| -rw-r--r-- | plt/effects.md | 395 |
1 files changed, 395 insertions, 0 deletions
diff --git a/plt/effects.md b/plt/effects.md index 03b7c8e..ef97667 100644 --- a/plt/effects.md +++ b/plt/effects.md @@ -3,6 +3,401 @@ layout: plt title: computation/effects --- +# effects and handlers: a comprehensive introduction + +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. + +<!-- The term "effects system" gets thrown around with "effects" a lot. --> +What is an effects system? + +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*. + +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) + +... + +- [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) + +## 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... + +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) + +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). + +### some terminology + +This is all covered in much more depth in Alexis King's excellent talk on continuations above. But if videos aren't for you, here is the basic jargon used when talking about effects systems: + +- **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*. + - 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 + - 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. +- **effectful**: having to do with effects, vaguely. + +## an intuition: exceptions as an effect + +```puck +pub mod exceptions = + use std.results + + pub type Exception[E] = effect + Exception[T](E): T + + # inferred: {Exception[E]} + pub func throw[E, T](err: E): T = + do Exception(err) + + # inferred: any other effects of action + pub func catch[T, E](action: () -> T {Exception[E]}, handler: E -> T): T = + try action() + with Exception(err) => + handler(err) + + pub func to_err[T, E](action: () -> T {Exception[E]}): Result[T, E] = + try Okay(action()) + with Exception(err) => Error(err) + + # inferred: {Exception[E]} + pub func to_exn[T, E](self: Result[T, E]): T = + match self + of Okay(value) => value + of Error(err) => throw err + +# example function defined outside of the module +# does not have access to try/with/resume. still useful, cannot break abstractions +pub func default[T, E](action: () -> T {Exception[E]}, value: T): T = + catch action() + err => value + +# inferred: {Exception["div-by-zero"]} +func div(x: Int, y: Int): Int = + if y == 0 => + throw "div-by-zero" + else + x / y +assert 5.div(0).default(0) == 0 +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 + +This suspend-and-resume model is a *very good* model of iteration... + +This is all terribly complicated. Can we implement something simpler with effects and handlers? + +```scala +// fixme: this does not compile... +interface Iter[T] { + def Iter(item: T): Unit +} + +def yield[T](item: T): Unit / {Iter[T]} = + do Iter(item) + +def iterate[T](self: List[T]): Unit / {Iter[T]} = + self match { + case Cons(head, tail) => + yield(head); + iterate(tail) + case Nil() => () + } + +def for_each[T]{action: () => Unit / {Iter[T]}}{f: T => Unit} = + try action() + with Iter { (value) => + f(value); + resume(()) + } + +def main() = { + println("hello!") + for_each{[1, 2, 3].iterate()} { + x => println(x) + } +} +``` + +<details> +<summary> puck </summary> + +```puck +pub mod iter = + type Yield[T] = effect + Yield(T) + + pub func yield[T](value: T) = + do Yield(value) + + pub type Iter[T] = class + iter(Self): {Yield[T]} + + pub func next[T](self: mut Iter[T]): Option[T] = + # iter is defined + try self.iter() + with Yield(item) => + self = self + return Some(T) + return None + # todo: implement next(). how tf do you do this??? + +#; +pub macro[T] `for` (value) `in` (expr: Iter[T]) `=>` (body) = + quote + try expr.iter() + with Yield(item) => + let `value`: `T` = item + `body` + resume() + +pub macro[T] `for` (value) `in` (expr: Iter[T]) `=>` (body) = + quote + while `expr`.next() of Some(`value`) => + `body` + +pub func iter[T](self: List[T]) = + if self of Cons(head, tail) => + yield head + tail.iter() +``` + +</details> + +## resuming with a value: io as an effect + +Side effects are effects, too! + +<details> +<summary> puck </summary> + +```puck +pub mod io + type Input = effect + Input: String + type Output = effect + Output(String) + + @[magic] + pub const stdin: File + pub const stdout: File + pub const stderr: File + + pub func write(file: File, messages: varargs[String]) = + if file == stdin => + for msg in messages => + do Output(msg) # (1), (3) suspend here + + pub func read(file: File): String = + if file == stdin => + return do(Input) # (2) suspends here + + @[handler] + func handle_output[T](action: () -> T {Output}) = + try action() + with Output(msg) => + std.primitive.write(msg) + resume() # (1), (3) calls resume here + + @[handler] + func handle_input[T](action: () -> T {Input}) = + try action() + with Input() => + let name = std.primitive.read() + resume(name) # (2) calls resume here + + +func print(msg: String) = + stdout.write(msg, "\n") + +func input(msg: String): String = + print(msg) + stdin.read(until = "\n") + +# inferred: {Input, Output} +func hello = + let name = input("Enter your name: ") # (1), (2) resume here + print("Hello, {}".fmt(name)) # (3) resumes here + +hello().handle_input().handle_output() +# Enter your name: +# > JJ +# Hello, JJ +``` + +</details> + +## mutable global state as an effect + +```puck +type State[T] = effect + Get(): S + Put(S) +``` + +## subsuming effects tracking: safety as an effect + +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. + +```scala +interface Unsafe { + def Unsafe(): Unit +} + +// Equivalent of Rust's `unsafe{}` blocks. +def safe[T](reason: String){action: () => T / {Unsafe}}: T / {} = { + try action() + with Unsafe {() => resume(())} +} + +def unsafe_operation() = { + println("doing an unsafe operation...") + do Unsafe() + println("completed unsafe operation.") +} + +def safe_operation() = { + println("calling an unsafe operation safely...") + // Equivalent of Rust's `unsafe{}` blocks. + safe("SAFETY: This operation is safe because I said so.") { + unsafe_operation() + println("another safe operation.") + } +} + +def top_level_safety_handler[T]{action: () => T / {Unsafe}} = { + try action() + with Unsafe {() => + println("unhandled unsafe function") + resume(()) + } +} + +def main() = { + top_level_safety_handler { + safe_operation() + } +} +``` + +<details> +<summary> puck </summary> + +```puck +type Unsafe = effect + Unsafe + +# Equivalent of Rust's `unsafe{}` blocks. +func safe[T](reason: const String, action: () -> T {Unsafe}): T = + try action() + with Unsafe => resume + +func unsafe_operation = # inferred effects: {Unsafe} + print "doing an unsafe operation..." + do Unsafe + print "completed unsafe operation." + +func safe_operation = + print "calling an unsafe operation safely..." + # Equivalent of Rust's `unsafe{}` blocks. + safe "SAFETY: This operation is safe because I said so." + unsafe_operation() + print "another safe operation." + +try + safe_operation() +with Unsafe continuation => + print "unhandled unsafe function" + continuation.resume() +``` + +</details> + +However, this is not quite enough. While we have implemented a *tracking* system for safety: we haven't actually implemented anything *unsafe* to go along with it. + +[Rust distinguishes several operations as unsafe](https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html#unsafe-superpowers), namely: +- Dereferencing a raw pointer +- Calling an `unsafe` function +- Accessing/mutating a global mutable variable +- Implementing an `unsafe` trait (`Send`, `Sync`) +- Accessing fields of an (untagged) `union` + +We have neither marker traits nor untagged unions in our system, so we won't deal with the last two. We also have already implemented unsafety propagating through function calls above (provided `do Unsafe` is called appropriately). And the first is typically implemented with compiler magic. So that leaves us with global mutable state. + +Hey, we already implemented something similar! What has to happen to get our effectful mutable state global and working with our new notion of unsafety? + +```puck +pub mod io = + + type Global[T] = effect + Get(Symbol): T + Put(Symbol, T) + + macro `global` (expr: Expr) `=` (value: Value) = + ... +``` + +Well, that was straightforward. Neat. + +## multiple resumptions: nondeterminism as an effect + +## modification of iterators: yield as an effect + +## communication protocols: ping/pong as effects + +## colourless functions: async i/o as an effect + +We've now arrived at the *real* interesting stuff. + +Effects-and-handlers systems promise + +## unified control flow semantics: async/await as an effect + +## why not undelimited control? effects as a sweet spot + +delimited control is *compositional*. + +## some design considerations for future effectful systems + +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. + +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 posts |