Remove distinction between pred and fn

[brson]

Writing pure predicates is pretty difficult and a pretty convincing argument was made recently that typestate predicates don't need to be pure. Removing the pred concept would simplify things a lot.

[catamorphism]

I'm not completely sold yet. I think we should discuss this more, particularly (as I think Dave said) with an eye to figuring out exactly what the static guarantees we can give are with whatever predicate language we end up choosing.

[graydon]

Can someone relate this convincing argument? First I've heard of it :)

[catamorphism]

It came up during our meeting with Dan Grossman yesterday. My understanding of it is that type soundness doesn't require the compiler to check, or know anything about, that the relationship between the semantics of the refined type corresponding to a certain typestate predicate, and the semantics of the implementation of that typestate predicate, makes sense. For example:

pred le(uint x, uint y) -> { true }
fn substr(uint start, uint end, str s) : le(start, end)  -> {...}

In this code, the implementation of le is probably not what the user had in mind. As far as whether it matters for soundness, that depends on whether substr calls some unsafe primitive that requires start to be less than or equal to end. But that's a problem even with the current system; everything here is pure.

Similar problems come up in Haskell. For example, you can define an instance of the Monad type class that doesn't satisfy the monad laws. The compiler won't help you there.

So I actually may just have convinced myself that since you run into problems even without considering impurity of the nature of the compiler not being able to check for you that your value semantics actually uphold your type semantics, we might as well just allow any function to be used as a predicate. The story would then be "the programmer has a proof obligation to make sure the typestate system they define for themselves is sound with respect to the semantics of the predicates they use in typestate constraints." This would suggest that those predicates probably have to be referentially transparent, but the compiler won't enforce that.

Let me know if this makes sense...

[eholk]

Where do we see typestate going in the future? Removing all the restrictions purity and whatnot in predicates seems to turn them sort of into C++ Concepts, where the programmer asserts a certain property is true and you write code assuming it's true but the compiler has almost no way to verify it.

Another direction I can see going is to say that right now we only know how to run the code and see if it's true, but in the future we might be able to do deeper reasoning about predicates. This gives the compiler a lot more freedom to omit checks and things when it can prove the condition already holds (for example, using transitivity of less-than).

If we see typestate going more in this direction (which is a very hard and still very researchy direction), then I think it makes sense to start with a more restricted language and extend it as we have a better idea what sorts of things the compiler can prove automatically.

[catamorphism]

In the "deeper reasoning" department, I think if we do go in that direction, it should be modular; instead of magic being baked into the compiler, there should be a way for the user to declare axioms / theorems about relationships between different typestate predicates. I think that would be pretty cool, but it does take us more into theorem-proving-land, and it would make the behavior of the compiler easy to reason about. It seems like in keeping with the philosophy of Rust overall, typestate is about making it very obvious which checks actually happen at runtime. If the compiler starts doing a bunch of automated theorem proving, that could make performance hard to reason about. Small changes to code could stymie a proof search and turn code with no dynamic checks into code with a bunch of dynamic checks all of a sudden.

From the perspective of predictability and control, it might really be better to hang onto the "the compiler doesn't know anything about the semantics of predicates" philosophy. And requiring predicates to be pure seems like a weird halfway point between the full-theorem-proving approach, and the know-nothing approach.

[graydon]

I agree in the sense of "... required for soundness". The typestate system's predicates are certainly operating outside the type system, and their truth or falsity is entirely up to the user to imbue with meaning.

I disagree that it follows that we should give up tracking purity on preds. The point of the typestate system, after all, is to track the evolution of state. In particular when variables change, typestates are invalidated. This happens because we assume the typestate is pure (and applied to immutables). If we give up on the purity as well, there's kinda no point in imagining a typestate holds from one moment to the next. We might as well apply them to mutable values also. The device loses its abstraction-over-flow-control, turns into just a point-in-time judgment. This seems like a serious loss to me. Feels akin to saying "since you might not alter a mutable value, or make a logic error with an immutable value, there's no point really tracking which values are mutable or immutable". I don't buy that. The added guarantee is helpful in "saying what you want to guarantee".

Does this makes sense?

[catamorphism]

Indeed, we might as well apply them to mutable values too if we go this route.

The problem with trying to enforce purity is that whatever we come up with is going to limit expressivity a lot. We might want to write some predicate that's semantically referentially transparent but that mutates local state. For example, we might want to write the substr function above like:

fn substr(uint start, uint end, str s) : le(start, end), le_len_of_str(end, s)  -> {...}

where we would want to write le_len_of_str like:

pred le_len_of_str(uint end, str s) -> bool { end <= str::len(s) }

but we can't do this, because len is impure, and it can't easily be made pure because it contains a for loop and increments a counter. Observably, len is pure, but since we decided not to do an effect system, we can't invoke effect masking there.

It's possible to write a tail-recursive pure version of len, but then I don't like the specter of having to write a "pure" and "pred" version of lots of common functions that are operationally the same.

I don't think there's an easy answer, and I think we should dedicate some time to discussing this. The question doesn't have to be answered right away, because there's still plenty of work I can do exploring what's possible with the current, restricted system.

[graydon]

Yup. This is why we had an effect system in the first place.

Question is whether the absence of effect reasoning in general is severe that all serious preds wind up doing something unsafe to get around the purity limit. If that's true, I agree there's not much point in trying to maintain the restriction. But I am not sure how it will play out. I was hoping a few higher-order (possibly unsafe) preds on each data structure would suffice to build many more safe ones, but maybe that's not true.

[graydon]

Simplifying proposal: preds can call non-pred functions, but can still only apply to immutable values. With further restriction: can only apply to immutable transparent values -- nothing containing objects, functions (or channels/ports/tasks, which will probably all be in libraries as obj and fn types anyways).

This gives you a form of "purity" that, I think, permits as much local state as you want, while still being pure-in-the-arguments. No?

[catamorphism]

Sorry this took so long, but Dave and I had some discussions and we finally have what I think is a feasible way to proceed now:

https://github.com/graydon/rust/wiki/Proposal-for-predicate-language

Graydon (or anyone else who may be following this), let me know your thoughts whenever you get a chance to look at it.

[catamorphism]

I'm marking this resolved for now. "pred" is now "pure fn" and "pure fn" can have a non-bool return typed. Unchecked blocks are implemented, so you can escape out to any code within a pure fn. (This is documented in the .texi file.) I think this is a reasonable solution for now.