mozilla/rust — Issue #1679: Add datasort refinements to Rust
Author: catamorphism
Created: 2012-01-26 19:50:55+00:00
State: open
Labels: design, feature, rfc

Looking through the rustc source code, it seems like many potential areas for typestate predicates involve cases where a value has an enum type and is known to be built with one of a subset of that enum type's constructors. I'm especially noticing this now that I'm going through and making all `alt`s exhaustive. For example:

```
enum foo {bar, quux, baz}

fn whee(x: foo) -> int {
alt x {
bar { 42 }
_ { fail "The impossible happened!"; }
}
}
```
We'd like to give `whee` a type that says `x` must be constructed with constructor `bar` -- in other words, a type that's a refinement on `foo`. We can do this right now with typestate predicates. However, datasort refinements seem to be a common enough case that it might be worth treating them separately. Also, datasort refinements can be implemented without needing to worry about any of the purity issues that have made typestate difficult, because once something of `enum` type is constructed, its tag is immutable.

The other reason to handle this separately from typestate is that the compiler never uses typestate information to eliminate any checks (since predicates may be unsound), whereas datasort refinements can be checked statically and used to eliminate unnecessary tests in `alt`s.

Thoughts?