Coroutines and effects
without.boats
without.boats
Then you could implement something like Google capslock [0] just by looking at type signatures.
- Lambdas (mainstream)
- Static types (mainstream)
- Pattern matching (getting there)
- Sum types (getting there)
- TCO (getting there)
- Global type inference (future)
- Functors (future)
- Effect systems (future)
- Expression orientated (future)
With OCaml, I get all of this today.
The future is here, it’s just not evenly distributed…
I can also imagine that it must be hard to maintain, like sometimes the types must accidentally change
not in other people's code. My main concern is that gradual typing makes understanding other people's code more difficult.
Idiomatic Haskell warns against missing signatures[1], Rust makes them mandatory. Rather than global inference, local inference stopping at function boundaries is the future, if you ask me.
The worst case is actually worse than when types are mandatory, since you can get an error in the wrong place. For example, if a function has the wrong type inferred then you get an error when you use it even though the actual location of the error is at the declaration site. Type inference is good but there should be some places (ex. function declarations) where annotations are required.
They cannot add it in other people's libraries.
> did not stop Python rising to conqueror the world
I wasn't talking popularity, I was talking maintainability. Python is not a stellar example of maintainability (source: maintained the Python API for a timeless debugger for 5 years).
Python's ubiquity is unfortunate, thankfully there seems to be a movement away from typeless signatures, both with Python's gradual typing (an underwhelming implementation of gradual typing, unfortunately) and Typescript.
Does it matter that much how the internals of someone else's library are implemented? The tooling will tell you the types anyway and module interfaces will have type signatures.
> Python's ubiquity is unfortunate,
Well that we can agree on!
Case in point: Java does allow exactly this, while also allowing classes to implement interfaces very similarly to how Rust structs can implement traits. Rust code sometimes uses traits to achieve similar results, like the `slice::get(index: SliceIndex<[T]>)` function, but the example above can't be done.
In general, coroutines seem vastly easier to understand/type compared to effects unless your language can do a lot of effect inference.
Symmetric vs assymetric coroutines: symmetric coroutines are the original style, where the currently executing coroutine decides who to transfer control to. Assymetric coroutines have a caller and a callee and the callee always yields control back to the caller. (This is much more common today)
Stackful vs stackless coroutines: in a stackless setting the language distinguishes between synchronous and asynchronous functions. This is what Python and Rust generators do. In a stackless setting (such as Lua), every function can potentially yield or call a sub-function that yields.
Exception handling is somewhat similar to stackless coroutines, specially in languages such as Common Lisp where the exception handler can choose to resume execution from the point that raised the exception, instead of unwinding the stack.
This isn't quite correct, but it's close. The original style were co-routines, as distinguished from subroutines, this was when programming was still heavily goto-oriented, these were little more than patterns used to structure go-to.
Simula, if I recall correctly, was the first high-level language to have coroutines, and they were basically asymmetric. I say basically because there was a mechanism for a coroutine to replace itself with another coroutine, but it wasn't a general transfer mechanism. Not unlike a delimited continuation in fact.
Good summary of how it all works however! I believe this is a typo:
> In a stackless setting (such as Lua)
Since Lua is stackful, and you're contrasting it with stackless generators.
> For example, Koka has a “diverging” effect, which means that an expression may diverge (that is to say, it may not finish evaluating). An expression containing a diverging expression is also diverging. So you can distinguish in the type system between a function that is guaranteed to finish and a function that may not finish (this is imperfect, of course, because of the undecidability of the halting problem; some functions that do not diverge will be marked diverging).
As I think about it (and I’m not a programming language theorist, nor have I done much serious work in any language with any sort of effect system), there are two vague categories of effect: control-flow effects like exceptions, yields, async waits (Pending, sleep, or however you feel like modeling it) and non-control-flow effects (divergence, various forms of unsafety, nondeterminism, impurity, reads or writes of global state, syscalls in models that don’t treat IO in and of itself as an effect), etc.
I would like to be able to run and write code that is definitely free of certain kinds of effects. Xz should not be unsafe or do IO, for example. Leftpad is an entirely pure, non-diverging function. And I should be able to ask my language to enforce that, ideally with trivial code. Maybe even by default.
But mainstream languages seem to mostly limit their use of effect-like systems on the control flow part, like this:
> Overall, coroutines strike me as the most promising way to handle many kinds of effectful functions because they seem to be in the design sweet spot: They are statically typed, lexically scoped, and unlayered.
This is related to the vagueness of your two categories. While exceptions, yields, and awaits don't really make sense without a handler, all that matters to the type system is which operations an expression might perform in addition to producing a result of their primary type. Handlers only interact with the type system in the sense that they remove an effect from their handle-ee expression.
So even in a language that committed to coroutines as its approach handling effects at runtime, the type system could still track and rule out effects like divergence or system calls. (For what it's worth, nondeterminism, state, etc. can all also be defined in terms of handlers. And at the same time, though, unsafety is not an effect because it is not entirely captured by "can this expression perform operation X.")
Effects is a MUCH more general and powerful technique than coroutines. An effect system can help greatly with implementing a coroutine system (instead of dealing with the unfortunate type-level hack Rust uses), but trying to implement an effect system on top of a coroutine system will give you a very limited emulation in the best case and another incoherent mess in the worst.
It would've been really great if Rust had a proper effect system, but it's very hard to introduce it into an existing language similarly to how you can not easily introduce borrow checker to C/C++. The messy "keyword generics" proposals only serve as a good demonstration for this. So we probably have to wait for Rust 2 or a different successor language.
`leftpad(string, int) -> string` needs to allocate so not fully pure that way. You could pass in the resulting string but then it would have to mutate, which is not really pure either.
Edit: @naasking, all good points. Still, isn't the general strategy to ensure memory isn't exhausted, rather than handling such a situation "gracefully", whatever that means? :)
Best to avoid the condition, or design the client side to handle the possibility the resource could be unavailable.
It's very normal in a Unix to be allowed to limit total runtime for example.
A lot of modern programming logically involves telling a computer to what to compute and not particularly caring how it gets computed. Yet we mostly lack a language in which one can specify computations and then then run the result portably and safely.
Then the compiler could recursively understand whether any given function is pure.
But if you're going to do the calculation, there's no difference between an infinite loop and a loop that finishes, but will take longer than you're willing to wait. Either way, it looks like the program hung.
So in practical programming languages, I'm not sure that the "diverge" effect is useful? You still need to kill it if it hangs. If it will take a long time, returning some kind of progress indicator would be nice. Maybe writing it as an iterator would help with that?
As you suggest, explicitly adding a provably-reducing value like a maximum iteration limit lets you show progress, give up at a "reasonable" time, and avoid divergence. This is how unlifted programming languages permit general recursion - that, and allowing inductive types to merely prove they're productive within a finite time bound (eg, a stream of values only needs to show it produces the next value eventually, not that it produces all values eventually).
I think you can do this in Idris with "total" functions.
It's a shame this was not explored before going down the Async route. I believe Effect handlers would have been a better fit for a systems language. IMHO a Monadic approach really needs something expressive like a functional language in order to work well.
That’s what Kotlin’s `suspend fun` does.
The more fundamental difference between effects and coroutines is that a `yield` in a coroutine always goes to the one unique resumer, and carries a single type of value. On the other hand, an expression may have several effects, each of which may be handled in a different place, in the same way that distinct exception types may be caught in different places.
Should that last bit be: "advantage of effect handlers over coroutines"?
EDIT: Oh, maybe I should have read the rest of the article first. It might be going the other way than that one example suggested. :)
That's the right insight. Just give me implicit parameters (i.e. the statically typed versions of dynamic scoping). I'll build my own effect system, coroutines, exception and what not as needed.
This is currently the case in rust. IO and other effects are frequently implicit. You don’t have to use ? or await they are *sugar. I have frequently seen reinventions of exceptions, unwind nonsense, adhoc interpreted tagged effects, etc..
Explicit syntax for effectfull calls should not be a goal. We don’t actually have that today.
I frequently scan for all instances of `?` or `.await` in functions (though, unfortunately, for various reasons this won’t show you everywhere these effects are produced).
I would rather not have to rely on an IDE to get that functionality.
An function with an effect (in this sense) is a function which can ask a handler to `perform` some effect for it. This suspends the function and passes control to whichever handler is in scope for that call, allowing that handler to resume the function at its leisure.
I suspect that you're misunderstanding what is meant by effect, because despite buzz about them and backend support for them in OCaml 5, they aren't yet implemented with syntax and type-level support in any mainstream languages I'm aware of.
Why does it need to ask a "handler" to do something, why can't it just call a function that does the "action" for it?
Depending on what your language tracked as an effect, you could make your business-logic always terminate, or perform no allocations, if you had effects for Mutation/GeneralRecursion/Allocation.
But no, I certainly don't understand the function->handler control flow here. It has to be handler->function, otherwise you've got two handlers!
Effects require 1) well-defined control flow (think of IO; you need to know in what order output occurs) and 2) manipulation of control flow (think of error handling or concurrency).
We can model effects as a back-and-forth between effect handlers, which carry out effects, and the user program. The user program passes control to the effect handler to carry out some effect, and the effect handler passes control back to the user program (potentially a different part of the user program; think error handling) when the effect has been performed. Continuations give complete control over control flow, so in their full generality effects require continuations (or some equivalent like monads). Coroutines are a slightly stilted form of continuations, that you can model much, but not all, control flow with.
There are obvious implementation differences but I'm not sure it makes any difference here, in both cases you can return to the same execution state multiple times.
A continuation is immutable in that way, so it is either an error to invoke it multiple times, or else it will always resume at the same place. Implementing coroutines in terms of continuations would mean capturing a new continuation each time you yield.
This can in fact be emulated with a coroutine generator and some fancy footwork, but it's a subtly different primitive.
Functions and lists are technically isomorphic, you just replace the function with a list of (domain, codomain) pairs and function invocation then becomes list lookup. This is basically the set theory definition of a function. So yes, this comparison to the article is apt, the article is saying that you can encode effects via coroutines.
I like the way is presented here: https://mikeinnes.io/posts/transducers/
The main gist is that "effect" allows you to define your own "except" of "try/except/finally"
I wrote "Feels like comparing Lists with functions" for a more general audience, but in my mind I was thinking:
- Effects are Monads
- Continuations are one particular Monad [1]
- Coroutines are probably similar?
- I would use monadic effects to allow/disallow a function from making use of Coroutines.
- If my effect system *itself* uses Coroutines how do I use the effect system to forbid Coroutines?
This is basically what we do at Temporal, which is essentially deterministic coroutines with externalized effects. This gives another nice property: using coroutines to wrap effects lets the non-effect logic replay/resume durably.
I don't know if that counts, but I think `call_with_timeout(duration, function_that_diverges, timeout_return_value, args...)` handles the diverging effect of its function argument.
[1] https://koka-lang.github.io/koka/doc/book.html#sec-return
Unless you are manually matching on the the Maybe, and thus observing the timeout, then that isn't the case. You'd probably also want a nondetermism effect which cannot handle unless you specifically build your timeouts to be deterministic, which I think Lean 4 does, but you can't go from partial to total with it afaik.
Exception handling, for example, uses dynamic scoping since you don't know what will be handling your exception when you write code which throws it.
Another way of thinking about it is, with dynamic scoping the value of the dynamic variable must always be on the stack and the closest one is the value that will be used. This is a really good behaviour for global variables since a common source of bugs is some global variables (and I'm considering class members "global" for this) getting changed unexpectedly. If the variable is lexical then it can be very hard to figure out what changed the value (especially when threads are involved) but if the variable is dynamic it's easy: the culprit is in the stack trace.
EDIT: Ah, reading this comment[0],
> The more fundamental difference between effects and coroutines is that a `yield` in a coroutine always goes to the one unique resumer
maybe I thought too much of Python where async/await are implemented via generators and, unless I'm mistaken, there need not be a unique resumer/event loop.
> Btw this is the beginning of me trying to shift away from blogging about rust to blogging about PL design in general. I find that I have very little to say about Rust that I haven’t already said.
In 2014 that would be extremely presumptuous or targeted at a very niche audience, however in 2024 a lot of people know Rust and so it seems much more reasonable.