5 ms·
This touches on something I’d like to see in more mainstream languages, but it doesn’t quite get there. > For example, Koka has a “diverging” effect, which mea
by amluto 3y ago
This touches on something I’d like to see in more mainstream languages, but it doesn’t quite get there.
> 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.
- noelwelsh 3y agoThis is one of the motivations of algebraic effects: you can have fine grained control over which effects are allowed.
- Rusky 3y agoThere are two aspects to effects as a language feature- first there is the runtime behavior, and then there is the type system. Ruling out categories of effects is the job of the type system, and you don't have to commit to (or avoid) any particular runtime approach to use it that way. 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.")
- newpavlov 3y agoYeah, the whole blog post reads like "if you worked too much with a hammer, everything starts looking like a nail". In other words, it puts the cart before the horse. 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.
- klabb3 3y ago> Leftpad is an entirely pure, non-diverging function. `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.
- atlintots 3y agoIt would be pure in languages without manual memory management
- naasking 3y agoUnless it can't allocate, and then the whole program terminates. There are unfortunately limitations everywhere.
- Kinrany 3y agoIf the whole program terminates, the purity of the function is still intact, the computer just can't compute it :D
- metadat 3y agoIs it really worth worrying about? This strikes me as pedantic. Once a program can no longer allocate memory, it's very likely toast anyway. 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? :)
- naasking 3y agoIt depends what your program is for. Some programs need guarantees because of bounded resources, so you may want resource allocation to be a visible effect (like embedded systems), or because you're running potentially untrusted code (like JS or WASM in a browser), or because you want sane failure handling (like running modules in a web server).
- arzig 3y ago
- kuchenbecker 3y agoHack programming language (Facebook's php++). They are called coeffects and can range from "this is pure with no side effect" to "this can modify local members" to "this has I/O".
- vendiddy 3y agoI would love something like this where to write a function with side effects I'd have to annotate it as such. Then the compiler could recursively understand whether any given function is pure.
- cryptoxchange 3y agoThe solidity language for smart contracts works like this.
- mrkeen 3y agoI write code like this every day in Haskell.
- dustingetz 3y agodon’t forget unbounded loops diverge - while(true){} and fn f() {f()} - also impure are blocking “pure” computations like fib(50)
- skybrian 3y agoIn proof languages where you want a proof that a function will succeed without running it, knowing that it doesn't diverge is important. 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?
- codebje 3y agoIt may depend on what you mean by 'practical', perhaps, but in a Haskell-like language divergence (as opposed to induction) more or less takes the form "let x = x in x" with varying degrees of ceremony. If you can provide to the compiler that you don't have any such thing in your fragment of code it can omit black-hole updates and checks during garbage collection for a small (possibly negligible or nil, if divergence still exists in the language anyway) performance boost. 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).
- brabel 3y agoD has a lot of these kinds of "effects", though they're called "attributes" [1] like "nothrow", "pure", "safe", "mustuse", "nogc"... there's also the "noreturn" type for functions that will never return [2] (infinite loop or throws). [1] https://dlang.org/spec/attribute.html#return https://dlang.org/spec/attribute.html#return [2] https://dlang.org/spec/type.html#noreturn https://dlang.org/spec/type.html#noreturn
- jbjohns 3y ago> 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. I think you can do this in Idris with "total" functions.