Add datasort refinements to Rust

Issue by catamorphism
Thursday Jan 26, 2012 at 19:50 GMT

For earlier discussion, see https://github.com/rust-lang/rust/issues/1679

This issue was labelled with: A-typesystem, I-enhancement in the Rust repository

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 alts 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 -- so that we don't need to write the fail case (because we can statically check that x is in the right subset of 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 alts.

Thoughts?

Start with the rustc source areas for typestate predicates, enum constructors, and exhaustive alt handling named in the issue. Compare datasort refinements with the existing typestate approach. Done means enum constructor subsets can be checked statically and unnecessary alt tests can be eliminated without relying on typestate purity assumptions.