Add datasort refinements to Rust

[catamorphism]

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?

[graydon]

• This is a good observation and in general I agree with it.
• Disjoint unions are implemented using typestate in Hermes, using this mechanism. Check the papers :)
• I've proposed permitting tag constructor names as implicit predicates in the past, precisely for this reason.
• I don't see a strong distinction between "datasort refinement" and "predicate applied to single immutable value". Except possibly implementation mechanism. Can you elaborate on the difference?

[catamorphism]

In response to the last question: the difference is just that the compiler has special knowledge about datasort refinements and can use it to eliminate checks. In the example I already gave, if bar had one field, then if whee was given a refined type, the compiler could compile away the alt and just extract the field directly -- no tag checking would be needed.

In general it's hard to see how arbitrary predicates applied to single immutable values can be exploited by the compiler to do optimizations.

[marijnh]

now that I'm going through and making all alts exhaustive

Please don't. I agree that alts should be exhaustive by default, but some just aren't, and being able to use a non-exhaustive alt as an assertion is a very valuable thing to have.

I assume you're just adding _ { fail "something..."; } clauses to such non-exhaustive alts. This tends to clutter the code, and produce no more informative error message than the default failure generated for such things by the compiler.

I'd much prefer if you added a way to explicitly specify that an alt is non-exhaustive, which would disable the warning/error for non-exhaustiveness, and make the compiler generate the implicit error path that current alts have.

[catamorphism]

Marijn: What do you think of the proposal above? It accomplishes the same goal as your suggestion ("a way to explicitly specify that an alt is non-exhaustive"), but with less clutter (because annotations are part of a type signature, there will be fewer of them), and with a static guarantee that there will be no non-exhaustive alt failures (because it becomes possible to check statically that all alts are actually exhaustive).

[marijnh]

The problem is that proving that a given value was constructed by a specific (subset of) variant will, in a lot of situations, be equivalent to the halting problem. So you get the same thing that makes typestate painful to use: you'll have to run a check on your value (and probably also first put it in a local variable), to be able to pattern-match on it.

In some programs this might work out, but I think there'll be enough cases where it won't, in which a non-statically-proven-safe form of non-exhaustive alt is still useful.

[catamorphism]

Another problem that I see is that inserting an "alt-unsafe" (or whatever) form doesn't encourage the programmer to document why it's actually safe to assume that the alt will actually match. Allowing the programmer to state invariants by giving more precise types to values than is currently possible encourages more rigorous reasoning, IMO. "alt-unsafe" could encourage people to just throw it in until the compiler is happy.

[catamorphism]

Where I'm coming from with this is that I'm looking at the many, many non-exhaustive alts in rustc and asking: "Why is this alt guaranteed to be exhaustive? What's the invariant?" And since in every single case, there is no documentation of why the code author expected that to be true, it's always unclear whether the non-exhaustivity is an error (that has coincidentally worked so far) or intentional. And I don't think having a different alt-unsafe form does much about that problem. I guess it does document one bit of information about the programmer's intent (that they believe there's an invariant), but not what the invariant is.

[marijnh]

Well, at the risk of sounding somewhat snarky, the invariant is that one of the patterns in the alt will match. I agree this doesn't usually amount to a perfect explanation, but neither will a special type or a predicate being applied to the value.

(Don't get me wrong, I think the feature proposed here would be awesome. I just don't think it's a full solution to the unexhastive alt problem.)

[catamorphism]

Well, you could also say that in a unityped language, the invariant is that there will be no dynamic type errors. However, statically typed languages allows richer invariants to be specified through the type system.

In this case, the reason why the programmer believes that one of the pattern will match presumably has something to do with dataflow and control flow properties, and types are a way to express an approximation to these properties. As you pointed out, the properties that need to be specified may be undecidable in general, but I would say that if it's not the case that most invariants that currently underlie inexhaustive cases in rustc are simple to state, then there's something wrong. The whole principle behind static typing is that while some of the properties we might like to check are undecidable, many useful properties can be captured in a decidable type system.

[graydon]

I have a wondrous solution!

You know how we have if check that combines the flow-control goodness of if with the typestate nutrition of check?

I hereby propose alt check which does the same. Specifically:

• The form of the alt has to be a simple N-way branch on the enum ctors. No nested matching or guards.
• If control passes the alt, it went through one of the arms, so the enum refinement of the disjunction-of-the-arms is valid in the poststate.
• If you didn't say alt check then nonexhaustive matches warn. You can inhibit the warning if you want.
• You can write _ { } if you want fallthrough.
• If a given enum-refinement already holds, it can be used to prove a non-exhaustive alt legal anyways. IOW
  if you were to say check x | some(*); alt x { some(y) { ... } } this would compile w/o error.

This actually generalizes nicely to refutable patterns in let bindings too. Add let check:

• let check some(y) = x; establishes the enum refinement on x (or fails), then unpacks its value to y.
• check x | some(*); let some(y) = x; means the same thing and compiles w/o error.
• let some(y) = x on its own gives a refutable-pattern warning (that you can inhibit).

[graydon]

(Granted, this has the slightly non-intuitive behavior that you have to write alt check to get the alt that fails at runtime, where you might think alt check is actually the strict alt that demands exhaustiveness. Tolerable UI idiosyncracy? I do think we want alt to default to exhaustiveness-checking, that's the thing ... which argues for "you have to say a little bit more to get non-exhaustiveness")

[marijnh]

check can be interpreted as 'adds a run-time exhaustiveness check'. I think it's fine.

[catamorphism]

Graydon: this looks OK to me, though I would prefer to call it something different from "alt check" (I'm not sure what). A construct like "alt check" would be necessary anyway for introducing values that have refined types. The only thing non-standard in what you're suggesting is that, basically, the "failure" case would be implicit (the compiler would insert an implicit fail in the case where none of the listed constructors match).

[catamorphism]

I think the name "alt check" is confusing because "if check" is the version of "check" that never aborts the program if the check fails -- whereas an "alt check" can abort the program.