This whole thing has to be understood in terms of capture calculus, a type system that can track which capabilities can get captured in a value. The idea is that we don't want to track effects, but instead track the capability to have an effect. A first version of this was presented
at this year's Scala symposium [EDITED to switch to a link that's openly accessible]
https://infoscience.epfl.ch/record/290885?ln=en
That paper is ostensibly about checked exceptions, but it contains a "capture calculus" that is much more general than that. We have fleshed out the meta theory of that type system since the paper appeared.
Because we track capabilities instead of effects we don't need two versions of def. Methods don't capture anything, only objects do. Functions are objects, so they can capture capabilities. With this PR, => will mean a function that can retain arbitrary effect capabilities in its closure and -> will mean a function that cannot. So -> by itself denotes pure functions. You can also express functions that only retain a specific capability, e.g. {c} A -> B for the function from A to B that retains capability c and is otherwise pure.