Hi,
I've been thinking about the unhappiness with Typestate (see e.g. issue #1105).
Let me first give a naive example:
I want to access the second element of a vector using "head()"/"tail()":
let a = [1, 2, 3];
let b = vec::head(vec::tail(a));
But Typestate wants me to write:
let a = [1, 2, 3];
check vec::is_not_empty(a);
let b = vec::tail(a);
check vec::is_not_empty(b);
let c = vec::head(b);
Here is a dopey idea:
First let's replace "head"'s predicate "is_not_empty()" with a different
predicate "has_minimum_length_one()". Let's now look at the above example in
reverse:
let c = vec::head(b); // b's length must be >= 1, in order to satisfy
"has_minimum_length_one(b)"
let b = vec::tail(a); // "tail()" drops the head element, thus a's length must
be >= 2
let a = [1, 2, 3]; // a's length is 3, which is >= 2, everything is fine
So
let a = [1, 2, 3]; let b = vec::head(vec::tail(a));
could be deduced to compile and be correct, if we could
1) make Typestate know that some functions ("tail()" in this example) change
properties, which are relevant to the predicates it verifies
2) make Typestate backtrack those property changes and predicates.
Does that make sense?
Bye,
Lenny
_______________________________________________
Rust-dev mailing list
[email protected]
https://mail.mozilla.org/listinfo/rust-dev
