summaryrefslogtreecommitdiff
path: root/plt/effects.md
blob: f1f73f12de4cac9030122e3380ab5f2ba6c908e3 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
---
layout: plt
title: computation/effects
---

# 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 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. But 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)

## toc

- [Background](#background)
- [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 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](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).

### 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`.
- **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.
  - 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.

<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 =
  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
```

</details>

<h2 id="resuming-continuations"> resuming continuations: iteration as an effect </h2>

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>

<h2 id="resuming-with-a-value"> resuming with a value: io as an effect </h2>

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>

<h2 id="side-effects"> side effects are effects, too: mutable global state as an effect </h2>

```puck
type State[T] = effect
  Get(): S
  Put(S)
```

<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 as a library 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) =
    ...
```

<h2 id="multiple-resumptions"> multiple resumptions: nondeterminism as an effect </h2>

<h2 id="modification-of-iterators"> modification of iterators: yield as an effect </h2>

<h2 id="communication-protocols"> communication protocols: ping/pong as effects </h2>

<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

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

<h2 id="undelimited-control"> why not undelimited control? effects as a sweet spot </h2>

delimited control is *compositional*.

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



## resources

posts
- [✨ 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)
- [Algebraic effects for the rest of us](https://overreacted.io/algebraic-effects-for-the-rest-of-us/)

papers
- [✨ 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)
- [OCaml](https://ocaml.org/)
  - [Eff](https://www.eff-lang.org/)
- [Unison](https://www.unison-lang.org/)
- [F*](https://www.fstar-lang.org/) ([paper](https://fstar-lang.org/papers/mumon/))
- [Coeffects](https://tomasp.net/coeffects/)