Rfcs: Add datasort refinements to Rust

[steveklabnik]

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?

[Diggsey]

I'm not sure exactly what the requirements are for this to work, but enum tags are not in fact immutable:

use std::mem::swap;

fn main() {
    let mut a = Some(1);
    let mut b = None;
    swap(&mut a, &mut b);

    println!("{:?} {:?}", a, b);
}

And in general, any mutable borrow can alter the enum tag.

[aldanor]

This would be a nice feature to have, and a great alternative to the ever-present catch-all match case.

Same as @Diggsey though, I was wondering what are the implications of enums tags not being immutable...

[kmcallister]

See also #671.

[jonhoo]

I'm confused — is this closed or open?
I assume it relates to https://github.com/rust-lang/rfcs/pull/1450, which has been closed for now?

[chrivers]

I'm working on a code base at the moment, where I have to have enums with structs inside each case. It's not great, ergonomically.

I would also like to request that we either close this (oh teh noes!) or change the title to remove "[closed]", which I believe is an error.

[leonardo-m]

A note: https://users.rust-lang.org/t/enum-field-types-datasort-refinements/11323

[jeschkies]

It seems to me this would be covered by #2593.

[glaebhoerl]

Only the case where the type is refined to a single variant.

[programmerjake]

What needs to happen before this can be implemented?