Great talk, super interesting! Seems like a lot of thinking went into solving this problem and a lot more needs to be done. As i understand, a parametric function would be like a mathematical function. Rusts current functions can have side effects which means they are procedures.
Great talk, hopefully this gains traction! Then Rust would really be almost the dream language, one that actually learns from 40 years of PL research but also has, y'know, users and code being written.
Great talk! Thank you very much! As others have stated in the comments, I think it would be useful at some point to address the series of blog posts that withoutboats has made. The things said in those blog posts really make a lot of sense, and deserve some more open discussion in my opinion, in a way that mere mortals like us can follow. Right now it seems like there are just 2 sides talking, with only one listening to the other.
Is there actually a reason (historically, or technical?), why uncarried types are not reflected in the type system? Why wouldn't an Unsafe make sense, that resulted from an unsafe function call, which has to be unwrapped in safe functions, but could be carried between unsafe functions?
You can think of effects as properties of the function itself, and not so much properties of the arguments or return type. unsafe fn, among other things grants you the permission to call other unsafe functions in the function body. That kind of “permission to do something” cannot be expressed by wrapping types.
I have some concerns about the Rust "weirdness budget" running out, where people look at this think "what the f" and walk away. I'd say a priority is to don't let this leak too much in application code.
I agree completely. I think there's a similar debate about whether "async next" versus "poll next" would be preferable for AsyncIterator. I think there exists some functionality which only makes sense in async or sync land, for example, that aren't amenable to effect abstraction like this when maximum performance is the most important factor.
The halting problem assumes a Turing machine. If a language is unable to loop indefinitely, it is no longer Turing-complete, and so the halting problem no longer applies. Or put differently: we can guarantee a program terminates (converges) by eliminating all conditions which could possibly cause it to not terminate (diverge).
It would be undefined behavior if its code paths were able to diverge. I think in practice (having not read any of the mentioned work/progress), it would have a syntax similar to `unsafe` where the programmer assumes responsibility of the correctness of the code with an identifier and an expression (think `non_diverging { ... }`.
Wonderful talk, great insights that were well explained, and the scene and editing are coming straight from a Wes Anderson film.
Also, *B L Å H A J*
thank you; that’s very kind of you to say
really great talk, i have run into these issues a lot with rust, and was completely ignorant to this "effect systems" way of thinking
We all know the star of the show here is Blahaj
this is such an unbelievably cool proposal, and if it gets added then cppbros will never shut up about how overcomplicated it is
Great talk, super interesting! Seems like a lot of thinking went into solving this problem and a lot more needs to be done. As i understand, a parametric function would be like a mathematical function. Rusts current functions can have side effects which means they are procedures.
Great talk, hopefully this gains traction! Then Rust would really be almost the dream language, one that actually learns from 40 years of PL research but also has, y'know, users and code being written.
Great talk! Thank you very much!
As others have stated in the comments, I think it would be useful at some point to address the series of blog posts that withoutboats has made. The things said in those blog posts really make a lot of sense, and deserve some more open discussion in my opinion, in a way that mere mortals like us can follow. Right now it seems like there are just 2 sides talking, with only one listening to the other.
Rust evolution is calling for a deeper understanding of effects.
ASMR
Is there actually a reason (historically, or technical?), why uncarried types are not reflected in the type system?
Why wouldn't an Unsafe make sense, that resulted from an unsafe function call, which has to be unwrapped in safe functions, but could be carried between unsafe functions?
You can think of effects as properties of the function itself, and not so much properties of the arguments or return type. unsafe fn, among other things grants you the permission to call other unsafe functions in the function body. That kind of “permission to do something” cannot be expressed by wrapping types.
I have some concerns about the Rust "weirdness budget" running out, where people look at this think "what the f" and walk away. I'd say a priority is to don't let this leak too much in application code.
U r great teacher
I love this.
Fascinating talk!
Super exciting talk - I hope this works out!
maybe[async] has far more implications than stated.
explained in without boats' blog -- let futures be futures
I agree completely. I think there's a similar debate about whether "async next" versus "poll next" would be preferable for AsyncIterator. I think there exists some functionality which only makes sense in async or sync land, for example, that aren't amenable to effect abstraction like this when maximum performance is the most important factor.
Is the divergence effect idea 'solve the halting problem' or am I missing something
I think it's 'reduce the valid programs to a subset for which halting can be proven'.
obviously you lose some expressive power for that.
The halting problem assumes a Turing machine. If a language is unable to loop indefinitely, it is no longer Turing-complete, and so the halting problem no longer applies.
Or put differently: we can guarantee a program terminates (converges) by eliminating all conditions which could possibly cause it to not terminate (diverge).
It would be undefined behavior if its code paths were able to diverge. I think in practice (having not read any of the mentioned work/progress), it would have a syntax similar to `unsafe` where the programmer assumes responsibility of the correctness of the code with an identifier and an expression (think `non_diverging { ... }`.