synthesize check and prove stmts for type-carried typestate constraints

[graydon]

A type can carry its own set of constraints. Example:

type ordered_pair = (int,int) : lt(*._0, *._1);

Implicitly, after every initialization of a slot s of type ordered_pair, there
should be a "check lt(s._0, s._1);", and after every copy statement there
should be a "prove lt(s._0, s._1)" statement, so that the implied constraints
become enforced at initialization time and preserved during writes.

This doesn't literally require adding statements -- though that's one approach
-- but it needs to mimic the effect one way or another. Currently such
constraints are simply ignored.

[graydon]

Shifted to rustc.

[pcwalton]

I think we actually don't want to synthesize checks here. It's more consistent IMO to require explicit check and prove statements.

We should never, in general, coerce T to T : pred. They're disjoint types.

[catamorphism]

I agree with Patrick here. I'll implement it this way unless someone yells.

[graydon]

How do you initialize an ordered_pair by that logic? initialize one without the constraint, check it, then move?

[catamorphism]

I'm assuming like:

check lt(a, b);
let p : ordered_pair = (a, b);

where if I omitted the check, the code would fail with a typestate error. Data constructors just get treated like functions, which can also have preconditions...

[graydon]

(a, b) isn't a pred. what's check doing there?

[catamorphism]

Sorry, edited.

[graydon]

Hm. Ok. If you can make it work, that seems sensible.

[catamorphism]

Also see: #869

[jruderman]

I'd like to have a concise form.

How about inserting checks for explicit casts?

let p = (a, b) as ordered_pair;

[catamorphism]

See https://github.com/graydon/rust/wiki/Constrained-types for our current thinking on this (mistakes are solely due to me). A problem with inserting checks for explicit casts is that it still requires further type system restrictions. Like, suppose you wrote:

let p = (a, b) as ordered_pair;
let q : ordered_pair = p;
q = (2, 1);

This is a bad program, because (2, 1) is not of type ordered_pair. But it's not clear how to design the typechecker and typestate so as to reject it. One simple solution is just to disallow ordered_pair as a type on the LHS of a declaration.

So since we have to introduce this restriction anyway, it seems to make sense to limit the introduction forms for things that have constrained types -- that is, the only place where the name of a constrained type can appear in a declaration is a function signature.

This is still very much of an open question, so I'm open to debate. I haven't had breakfast yet, so let me know if any of this doesn't make sense ;-)