(The older thread has being closed so I've written a new one).

A new language implemented in Scala for the JavaVM is named Flix:

It has three interesting features, one of the three is that its type system tracks the effects of functions (I think for now it only tracks function purity, but there's interest to track other effects too later). Pure functions aren't a subtype of impure functions (invariant), so to a function that accepts an impure function as argument you can't give a pure function. The "Pure" annotation for functions is the default and you can omit it. An usage example of such polymorphic effects:

/// Assume we have some pure and impure functions: def inc1(x: Int): Int & Pure = x + 1 def inc2(x: Int): Int & Impure = Console.printLine("Hello"); x + 1

/// We can write functions that expect pure or impure functions: def twice1(f: Int -> Int & Pure, x: Int): Int & Pure = f(f(x)) def twice2(f: Int -> Int & Impure, x: Int): Int & Impure = f(f(x))

/// But we can also write *effect polymorphic* functions:
def twice3(f: Int -> Int & e, x: Int): Int & e = f(f(x))

/// We can use `twice3`

with both pure and impure functions:
def main(): Int & Impure = twice3(inc1, 0) + twice3(inc2, 0)

The explanation of how such polymorphic effects work:

The & symbol is used to attach an effect to the signature of a function. Such syntax is not beautiful, in my opinion, but it works. An example usage of such polymorphic effects to implement a map:

def map(f: a -> b & e, xs: List [a]): List [b] & e = ...

A more complex example of polymorphic effects to implement an >> operator that performs function composition, it specifies that >> is impure if at least one of the two functions is impure (in this system Pure equals to a true boolean value, and Impure is a false value):

def >>(f: a -> b & e1, g: b -> c & e2): a -> c & (e1 and e2) = x -> g(f(x))

But in Flix you can do even bette, this specifies that at most one of the two input functions is impure:

def mapCompose(f: a -> b & e1, g: b -> c & (not e1 or e2), l: List [a]): List [c] & (e1 and e2) = ...

All this stuff is orthogonal to the current Rust type system, so I think it can be added. In practice it can't be added because it's a breaking change because on default functions must be pure. Rust used to have the "pure" annotation, but it was removed because it was implemented naively. A polymorphic effects design similar to Flix is more useful and reasonable. Still, I am not sure why/how this feature could (even in theory) improve the practice of Rust programming.

From my older thread about the same topic:

At this point, the annotation becomes redundant,<

I have no proof of this. I think coding in Flix for few years will answer this.