Last active
March 19, 2025 20:21
-
-
Save zesterer/a596d05d02201e3f4f2af148f8b67791 to your computer and use it in GitHub Desktop.
Ideas for a language with first-class effects
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// - Effects are groups of action that are provided to callees | |
// - Actions define a 'throw' value (passed up the stack on yield) and a 'fetch' value (passed back down the stack on resume) | |
// - Actions are syntax sugar for effectful functions | |
// i.e: | |
// effect e { action foo(A) -> B } | |
// appears as a function like (TODO: scoping?) | |
// foo: A -> e ~ B | |
// TODO: Are typeclasses and effects similar enough to be merged? | |
// Example: Mutation | |
effect read[A] { action read() -> A } | |
effect write[A] { action write(x: A) -> () } | |
// Mutation is an effect alias that combines both reading and writing | |
effect mut[A] = read[A] + write[A] | |
// Add the elements of the list to an accumulator value | |
// TODO: It would be nice to be able to label effects so that, for example, two `Nat`s could be incremented independently | |
// This sounds quite similar to function arguments: can we differentiate between explicit and implicit effects? | |
fn add_sum(xs: List Nat) -> mut[Nat] ~ () { | |
match xs { | |
[] => (), | |
[x .. xs] => { set(get()! + x)!; add_sum(xs)! } | |
} | |
} | |
// TODO: Should returning be an effect, or a built-in? If the former, it might look like this | |
// Pros of making it an effect: consistency, easy to express non-termination | |
// Cons: Would need to be a lang item since `effect { 42 }` needs to work, also might make HM inference harder | |
effect return[A] { | |
// Implies that the effect cannot return | |
action return(A) -> ! | |
} | |
effect gen[A] { | |
// Implies that the effect returns | |
action yield(A) -> () | |
} | |
// Map generator elements using a function | |
fn map[A, B, T, e, f](g: e + gen[A] ~ T, f: A -> f ~ B) -> e + f + gen[B] ~ T { | |
when g { performs yield(x) => yield(f(x))! } | |
} | |
// Filter generator elements according to a predicate | |
fn filter[A, T, e](g: e + gen[A] ~ T, f: A -> f ~ Bool) -> e + f + gen[A] ~ T { | |
when g { | |
performs yield(x) if f(x) => yield(x)! | |
performs yield(x) => resume () | |
} | |
} | |
effect async { | |
// TODO: Design this properly later | |
action block[R: Request](R) -> R.Output | |
} | |
effect fail[E] { | |
// Failures are non-resumable | |
action fail(E) -> ! | |
} | |
// Effect can declare other items | |
effect stdio { | |
action write(File, bytes: List[u8]) -> fail[IoError] ~ () | |
action print(s: [Char]) -> () | |
} | |
// Effect sets can compose effects (TODO: private effects akin to non-exhaustive enums?) | |
effect io = net + fs + stdio + ... | |
data InvalidRange; | |
// Yields numbers from a to b (exclusive), returning the total number yielded. | |
fn range(a: Nat, b: Nat) -> fail[InvalidRange] + gen[Nat] ~ Nat { | |
when cmp(a, b) { | |
is Equal => 0 | |
is Less => | |
yield(a)! | |
1 + range(a + 1, b)! | |
is More => fail(InvalidRange)! | |
} | |
} | |
fn count_numbers() -> stdio ~ () { | |
// Effect handling can be done in-line with pattern matching | |
// Any unhandled effects are propagated to the nearest effect basin | |
when range(0, 10) | |
-> map(fn x => x * x) | |
-> filter(fn x => x < 10) | |
{ | |
// by default, control flow terminates | |
// TODO: Is this a sensible default? Maybe only if the fetch value's type has no inhabitants? | |
// Proposal: emit compilation error if type of resume value is inhabited, require an explicit `escape` (like `resume` above) | |
performs fail(InvalidRange) => print("Invalid range!")! | |
// `resume` causes control flow to return to the effect (i.e: it's like a local `return`) | |
// Handler arms also pattern-match. Refutable patterns do *not* unwrap their effect from the type (maybe this implies effect checking should be combined with exhaustivity checking?). | |
performs yield(0) => resume print("Counted zero")! | |
performs yield(x) => resume print("Counted {x}")! | |
// Non-handler arms must be exhaustive | |
// If no `is` clauses are present, the output of the predicate becomes the result of the `when` expression. | |
// TODO: Does this work properly with uninhabited types? Does it require subtyping? | |
is 0 => print("Counted no numbers!")! | |
is n => print("Counted {n} numbers!")! | |
} | |
} | |
fn ftp_server() -> net + fs { | |
... | |
} | |
when web_server() { | |
yields x => print(x) | |
else => ! | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment