You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The Vale programming language would highly benefit from the addition of effect types and handles. In this issue i propose a draft design, as well as suggesting use cases and a compilation method.
Draft Design
Effects can be defined with the effect keyword
effect Throws<T> {
throw(T);
}
This declaration specifies the effect type (Throw<T>) as well as the set of operations that can be performed (throw(T)).
Any function that performs an effect operation must be marked with the corresponding effect type. Effect types can be annotated as following:
func idiv(a int, b int) int & Throws<str>
Syntactically, performing an effect operation looks the same as a function call, but its purpose is to move the control flow to an effect handler, which will 'handle' the operation just performed.
Handlers can be defined with the with keyword, and they are valid for the scope they are declared in.
Here is an example of an effect handler in action:
func idiv(a int, b int) int & Throws<str> {
if b == 0 {
throw("You can't divide by zero!"); //Perform the 'throw' operation, moving the flow to the handler of this operation.
}
return a / b;
}
func idiv1(a int, b int) int & Throws<str> {
return idiv(a, b) + 1;
}
func foo(bar int) {
with throw(val) {
//This block of code is executed only if 'throw' is performed.
print(val);
//After the handler, the flow exits the current scope.
}
res = idiv1(1, bar); //Do operation that can perform 'throw'
// Do stuff with res...
}
The function 'idiv1' is annotated as Throws while foo isn't. This is because, if not handled, effects propagate through the call stack. So, if you call a function that may perform an effect operation, you must either handle it or annotate the effect in the parent signature.
This effect is linear, since the control flow of that operation is one-directional.
In non-linear effects, handlers can move back the flow to where the operation was performed, optionally yielding a value.
Non-linear effects are declared in a similar way to linear ones, except a type is specified after the operation:
effect Yields<T> {
yield(T) void;
}
This effect accepts a parametr of type T, and resumes with no values.
This is how non-linear effects work:
func squares(to int) void & Yields<int> {
foreach i in range(0, to) {
yield(i); //Perform the operation 'yield', that yields no value
//Flow may resume here
}
}
func main() {
with yield(value) {
//do something with value
resume; //resume the flow from where the operation was performed, with no value
}
squares(10);
}
Another concept related to effect types is effect polymorphism. This allows a function to be polymorphic over the effects it raises. It works as following:
Effects can be used to implement a variety of patterns and features.
The Throws effect, shown above, can be a good alternative to the Result<T, E> variant. It doesn't require syntactic sugar to propagate, and it looks familiar to people coming from C++/Java.
The Yields effect, shown above, can be used to implement generators, even if they can't be used in a foreach loop.
Effect handlers can also be used to design the low-level custom allocator system. Here is how it would look like:
effect Alloc {
func alloc<T>(T) ^T;
func dealloc<T>(^T);
}
func allocates() void & Alloc {
foo ^str = alloc("bar");
//Do stuff with foo
dealloc(foo);
}
func main() {
with alloc(expr){
//Low-level code to allocate the object
resume allocated;
}
with dealloc(value) {
//Low-level code to deallocate the object
}
allocates(); //Now 'allocates' uses the custom allocator implemented above.
}
Implementation
Effects can be considered zero-cost abstractions.
They can be implemented through evidence passing, as described here, or with staging, as described here.
Linear effects, used mostly for error handling, can be lowered to a propagated return value, making them as fast (if not even faster) than Result. Since Vale compiles to LLVM, non-linear effects can be implemented with llvm.coro.suspend and llvm.coro.resume, or alternatively with implicit closure passing.
The text was updated successfully, but these errors were encountered:
The Vale programming language would highly benefit from the addition of effect types and handles. In this issue i propose a draft design, as well as suggesting use cases and a compilation method.
Draft Design
Effects can be defined with the
effect
keywordThis declaration specifies the effect type (
Throw<T>
) as well as the set of operations that can be performed (throw(T)
).Any function that performs an effect operation must be marked with the corresponding effect type. Effect types can be annotated as following:
Syntactically, performing an effect operation looks the same as a function call, but its purpose is to move the control flow to an effect handler, which will 'handle' the operation just performed.
Handlers can be defined with the
with
keyword, and they are valid for the scope they are declared in.Here is an example of an effect handler in action:
The function 'idiv1' is annotated as
Throws
whilefoo
isn't. This is because, if not handled, effects propagate through the call stack. So, if you call a function that may perform an effect operation, you must either handle it or annotate the effect in the parent signature.This effect is
linear
, since the control flow of that operation is one-directional.In non-linear effects, handlers can move back the flow to where the operation was performed, optionally yielding a value.
Non-linear effects are declared in a similar way to linear ones, except a type is specified after the operation:
This effect accepts a parametr of type T, and resumes with no values.
This is how non-linear effects work:
Another concept related to effect types is
effect polymorphism
. This allows a function to be polymorphic over the effects it raises. It works as following:Use Cases
Effects can be used to implement a variety of patterns and features.
The
Throws
effect, shown above, can be a good alternative to theResult<T, E>
variant. It doesn't require syntactic sugar to propagate, and it looks familiar to people coming from C++/Java.The
Yields
effect, shown above, can be used to implement generators, even if they can't be used in aforeach
loop.Effects can also be used to implement async/await, as shown in this paper. Effect polymorphism resolves the problem of function coloring very easily, in a more natural way than what rust is doing.
Effect handlers can also be used to design the low-level custom allocator system. Here is how it would look like:
Implementation
Effects can be considered zero-cost abstractions.
They can be implemented through evidence passing, as described here, or with staging, as described here.
Linear effects, used mostly for error handling, can be lowered to a propagated return value, making them as fast (if not even faster) than
Result
. Since Vale compiles to LLVM, non-linear effects can be implemented withllvm.coro.suspend
andllvm.coro.resume
, or alternatively with implicit closure passing.The text was updated successfully, but these errors were encountered: