Allow modifications to local variables in pure functions

[kud1ing]

I know this issue is on someone's plate, but i could not find a related issue.

Currently we can not iterate over strings, vectors, lists etc using pure functions. That means that functions like str::is_whitespace() can not be declared pure either, even though logically they are.

[marijnh]

You'd still not be able to make iter pure, since it calls one of its arguments and can't prove that this argument is pure.

You can add more rules to handle that, but it just goes down deeper and deeper. As we found out before (there was an effect system early last year that was dumped again), you can't really do any kind of sane purity checking on a language like Rust. I would prefer going back to a system where you can simply annotate a function that you want to use as a predicate as pure (or, preferably, pred), and give up on any checking of this purity.

[kud1ing]

It would not be possible to add the "pure" declaration to a higher-order function's arguments? Like

pure fn any<T>(v: [T], f: pure fn(T) -> bool) -> bool

[marijnh]

We could make purity part of a function's type. But that still doesn't come close to solving the problem. Consider this:

fn count_zeroes(x: [int]) -> uint {
    let cnt = 0u;
    vec::iter(x, {|elt| if (elt == 0) { cnt += 1u; }});
    ret cnt;
}

Is this pure? The block passed to iter sure isn't. (And sure, you can come up with more and more rules to cover more and more cases, but it'll get really complicated and hard to understand. Also, actually annotating all pure functions, not just those that are used as predicates, is very much like "const correctness" in C++ -- people will forget or not bother, and as a result the whole system, which requires consistency, falls apart.)

[kud1ing]

My naive defininition of "pure" is: "a pure function can do whatever it wants, unless that impureness does not escape its scope".

• The block {|elt| if (elt == 0) { cnt += 1u; }} is not pure, since it affects state outside of its scope.
• "count_zeroes()" would still be pure, because its impure implentation does not escape its scope.

Does that make sense?

Or simpler:

pure fn a_number() -> uint {
    let cnt = 0u;
    cnt += 42u;
    ret cnt;
}

Would use state-manipulation internally, but it would not escape.

[marijnh]

Sure that makes sense. Formalizing that sensible definition is where the problem lies.

[kud1ing]

There seemed to be a paper “Grafting Functional Support on Top of an Imperative Language” by Andrei Alexandrescu on D's implementation of purity, but i can not find it.

Their definition of "pure" can be found here: http://www.d-programming-language.org/function.html

[catamorphism]

Marijn -- I'm confused about this comment "I would prefer going back to a system where you can simply annotate a function that you want to use as a predicate as pure (or, preferably, pred), and give up on any checking of this purity." This is exactly what unchecked blocks do, which I added back in August or September. (I can't remember what the exact syntax we decided on was.) Or did those go away?

[marijnh]

We have unchecked blocks, but we also have an attempt at formal purity checking. I'm proposing we get rid of the second, since it's just annoying and broken, and just implicitly not check purity, just believing the programmer whenever he/she annotates a function as pure.

[catamorphism]

I feel like we already discussed the "get rid of purity checking" possibility back in the summer when we were discussing these issues thoroughly -- has anything changed since then?

[marijnh]

What was the conclusion of that discussion?

[catamorphism]

The conclusion was that it's important to give the programmer the freedom to choose to write their typestate predicates a restricted sublanguage that is statically guaranteed to be pure, because otherwise they're not getting strong guarantees from the compiler. At the same time, they also have the freedom to use unchecked blocks to say "trust me"; leaving purity checking in doesn't take away freedom from someone who only wants to use the "unchecked block" option. They can just throw an unchecked block around all predicates.

[ssylvan]

Would something like Haskell's ST monad help? Not necessarily explicitly using a monad of course (indeed, it would be ideal if you didn't even know this was going on under the covers!).

The general idea is that each mutable value would be tagged with a specific type variable (one that's "fresh" for the given "pure" function), and every time you do something with mutable variable you just thread this type variable through everything (making sure they match). Then at the end you strip it out in the "runST" call. Since the result value's type doesn't have access to this type variable, it couldn't posssibly contain any mutable references leaking side effects.

Maybe typestate could be used to do the same kind of tracking (with modifications). They key point is that anything impure is associated with a fresh "tag" introduced by the "pure" annotation, and that you ensure that nothing tagged with this "tag" can escape the function, statically.

BTW, this not only means you can modify local variables on the stack, you can modify local heap allocations too.

[catamorphism]

Assigning this to myself, but I don't think it's wise to spend time on it until we reach a clearer consensus about what we want in the long term w.r.t typestate and purity checking (if anything) -- see #2178.

[nikomatsakis]

as part of the borrowing check that I am working on, I have all the capabilities to solve this in a nice way (as I already have to know which data is interior to the stack frame and what is not).

[ssylvan]

It would be interesting to add some kind of warning about a function that's really pure not being marked as such. Then you can measure how many functions are really pure in a code base. If the pure to impure ratio on some real programs is more than, say, 50% (or even lower), maybe the modifier should be inverted so that pure is the default.

[nikomatsakis]

you can now modify local state (that is, state which is uniquely tied to the current stack frame) in pure fns. there is still the question of allowing pure fns to invoke closures and so forth---I think this is best addressed by an adapted version of the Lighweight Polymorphic Effects functions, which basically allow a function to be "as pure as its argument closures are"---but that seems like a separate issue.

[kud1ing]

Great, thanks.