[Idea/Pre-Pre-RFC] Additional exhaustiveness checking

language design
1

Extending the exhaustive checks feature might help writing correct programs. Exhaustive checking in the match statement is currently limited to input values only. Output values might also benefit from exhaustive checks. Next to the exhaustive checks, a left- or right-uniqueness check might increase program correctness. As a specific suggestion: Aside of the term match there should also exist an injective_match, a surjective_match and a bijective_match.

Please read this as an idea. It is most likely not sound.

Minimal mathematical foundation

When it comes to exhaustiveness guarantees, there are four properties:

  • right-uniqueness: Every input variable of a match has a single, unique output variable.
  • left-uniqueness: Every output variable has a single, unique input variable.
  • right-totality: Every possible output value is covered.
  • left-totality: Every possible input value is covered.

Currently, only the left-totality exhaustive check is implemented. It is possible to switch off the check by using _ => {}.

Function table

Combining these function properties, there are four common function types. As follows, these function types are named match categories, because function is a term already used in Rust. There are four binary variables right-unique, left-total, right-total and left-unique. We can ignore the left-totality, because default matching is a feature we wish for. Which narrows it down to three binary variables. With that, only the right-unique cases are relevant, which leads to four cases:

right-unique left-total right-total left-unique match category
Y * N N normal match case, the left-totality is already a compile-time guarantee. It can be switched off, by setting the Scrutinee to _, which is the default matching _ => {}.
Y * Y N named surjective_match or match_onto.
Y * N Y named injective_match.
Y * Y Y named bijective_matching
* * * * All other cases are not of relevance for Rusts matching concept.

Example usage

The following example of a bijective_match indicates the use case. Additional exhaustiveness checks and what problems might occur, while implementing:

struct SymbolicNumbers { One, Two, Three }

// this matching is right-total
impl TryFrom<u32> for SymbolicNumbers {
    type Error = ();
    fn try_from(input: u32) -> Result<Self, Self::Error> {
        bijective_match input { // <- the special thing here is the `bijective_match`
            1 => Ok(SymbolicNumbers::One),
            2 => Ok(SymbolicNumbers::Two),
            3 => Ok(SymbolicNumbers::Three),
            _ => { Err(()) }
        }
    }
}

// Same code but a case is commented out.
// So this matching is not right-total. It would cause a compile-time error.
impl TryFrom<u32> for SymbolicNumbers {
    type Error = ();
    fn try_from(input: u32) -> Result<Self, Self::Error> {
        bijective_match input {
            1 => Ok(SymbolicNumbers::One),
            2 => Ok(SymbolicNumbers::Two),
            // this errors in something like:
            //     error[EXXXX]: non-exhaustive right-totality patterns: `SymbolicNumbers::Three` not covered
            // because following line is missing:
            // 3 => Ok(SymbolicNumbers::Three),
            _ => Err(()),
        }
    }
}

Possible problems

  • What about nested enums or long tuples?
  • What about guarded arms (containing if statements)?
  • What about integer matching? The current match implementation allows specifying Range and Integers at the same time for Patterns.
  • To check the soundness of the result types (e.g. right-totality), one would have to traverse into functions and branches within the match-arm expressions. For the current match implementation (Pattern), there is not such a code traversal, as values have to be defined directly in the MatchArm.
  • In the example above (3 => Ok(SymbolicNumbers::Three)): instead of returning the Ok(SymbolicNumbers::Three) directly, a function call might return Ok(SymbolicNumbers::Three) instead. For instance, the body of the arm could be 3 => ok_symbolic_numbers_three(). One could traverse into the return value, but this would open reachability problems. I would suggest to ignore the reachability issues:
    fn ok_symbolic_numbers_three() -> Option<SymbolicNumbers> {
    if false {
        // 1. the compiler could traverse into all functions return instances.
        // 2. this will never be reached at runtime. 
        return Ok(SymbolicNumbers::Three);
    } else {
        // ignore this
        todo!();
    }
}

Request for comments

I did not find a similar proposal or problem description. Please help me with a link, if I can not properly use the search engine of my choice. As I like the idea, I would be really happy if this turns into a discussion! :crab:

2

There's was a RFC for that, but the proposal was dropped

I think I saw a more recent discussion on this here on IRLO, but I can't find it

About your proposal, I think that bjective_match, surjective_match and the likes.. that's too much keywords. Also I think you actually need a theorem prover (or at least something like flux) to prove something is a bijection: naming some language construct bijective_match is mildly misleading because it probably could be used to create things that are not bijections.

3 Likes
3

@dlight This? Doubly-exhaustive match statement

3 Likes
4

It is not a bijective match. Both SymbolicNumbers::try_from(4u32) and SymbolicNumbers::try_from(0u32) return the same (i.e. structurally equal) Err(()).

5

I'd like to reiterate here what I said in the "Doubly-exhaustive match statement" thread: a hypothetical "if this construct can be proven not to produce all possible variants of this enum, I want a compile-time error" marker is much more useful if it's not limited to match expressions. For example, it would be very useful to be able to apply it to FromStr impls for enums, whether or not the body of the function definition involves match at all.

2 Likes