Skip to content

Fix the handling of uninhabited types in pattern matching. - #1872

Closed
canndrew wants to merge 3 commits into
rust-lang:masterfrom
canndrew:match-exhaustiveness
Closed

canndrew wants to merge 3 commits into
rust-lang:masterfrom
canndrew:match-exhaustiveness

Conversation

@canndrew

Copy link
Copy Markdown
Contributor

@arielb1

arielb1 commented Jan 25, 2017 •

Copy link
Copy Markdown
Contributor

Copying from the internal threads, there are a few desirable properties of match that are incompatible (now that we have an RFC, we can move the discussion there):

  1. match exhaustiveness is identical between safe and unsafe code
  2. &! is matchck-uninhabited in safe code
  3. matches don't assert deep validity in unsafe code
  4. uninhabited types are not treated specially for UB
  5. if a match is exhaustive, every arm you add to its end can never be reached

The problem is:
Because of (2), you can write this code:

    let x: &! = get();
    match x {
    }

From (1), we also get

    unsafe {
        let x: &! = get();
        match x {
        }
    }

On the other hand, we also want this to be non-UB - aka (3)

    unsafe {
        let x: &Whatever = get();
        match x {
            y => println!("hi {:?}", y as *const _)
        }
    }

Because of (4), this is equivalent to

    unsafe {
        let x: &! = get();
        match x {
            y => println!("hi {:?}", y as *const _)
        }   
    }

Which contradicts (5)

@arielb1

arielb1 commented Jan 25, 2017

Copy link
Copy Markdown
Contributor

I think this RFC proposal denies (5) while keeping (1)-(4). @nikomatsakis has a good argument for (5), but I'll prefer that he present it.

@Ericson2314

Copy link
Copy Markdown
Contributor

My alternative of https://internals.rust-lang.org/t/recent-change-to-make-exhaustiveness-and-uninhabited-types-play-nicer-together/4602/57?u=ericson2314 where match { } is always a just a 1-deep match should get all 5 at the cost of some verbosity.

@arielb1

arielb1 commented Jan 25, 2017 •

Copy link
Copy Markdown
Contributor

@Ericson2314

To repeat this in the thread, the proposal is:

    unsafe {
        let x: &! = get();
        match x {
            _ /* no arm needed */,
        }
    }

I consider that !(2), but it requires bikesheddy syntax.

@Ericson2314

Ericson2314 commented Jan 25, 2017 •

Copy link
Copy Markdown
Contributor

@arielb1 hmm? In my alternative one would need to do:

unsafe {
    let x: &! = get();
    match x {
        &_, // no arm needed
    }
}

The idea is by bothering to pattern match down to the trivially uninhabited case, [unsafe | all, depending on what we want] code is asserting that the branch is unreachable.

unsafe {
    let x: &! = get();
    let y = match x { y => y };
    println!("I'm alive!"); // not dead code, because unsafe + insufficiently deep match
}

@Ericson2314

Ericson2314 commented Jan 25, 2017 •

Copy link
Copy Markdown
Contributor

Hmm, I just realized if one has a tuple of &!, and only some of them are valid, punning on _ isn't so good. Let me amend my alternative so ! is a pattern that asserts the thing it is matching is "trivially" uninhabited.

Examples:

  1. unsafe {
      match get(): &! {
        &!, // no arm needed
      }
    }
  2. unsafe {
      match get(): Void {
        !, // overkill, but accepted.
      }
    }
  3. unsafe {
      match get(): Result<usize, !> {
        Ok(n) => println!("going strong {}", n);
        Err(_) => println!("still alive!");
      }
    }
  4. unsafe {
      match get(): Result<(usize, !), (Void, !)> {
        Ok((n, _)) => println!("still alive! {}", n);
        Err((_, !)), // only 1 `!` needed
      }
    }

This is great for those coming from Haskell [haha, what a pedagogical priority], because if you really really drunkenly squint, asserting uninhabitedness is like forcing a binding (with !), and and @arielb1's trap representations are like the bottom value.

@aturon aturon added the T-lang Relevant to the language team, which will review and decide on the RFC. label Jan 26, 2017
Comment thread text/0000-match-exhaustiveness.md Outdated
```rust
let t = match never_fails() {
Ok(t) => t,
Err(e) => match {},

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be match e {}.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks.

@nikomatsakis nikomatsakis self-assigned this Jan 26, 2017
@canndrew

Copy link
Copy Markdown
Contributor Author

@Ericson2314

I would prefer to go with what's proposed in the RFC because it's consistent with how we match on non-empty sum types and because forcing users to handle trap representations in matches kinda defeats the point of having types.

However, there's no reason why we couldn't do both the RFC and your suggestion. There's a Pre-RFC proposing to generalise the use of | in matches. From a certain point of view your ! pattern would be the identity of the | pattern operator, meaning you could match on any type with it but it wouldn't match any values:

match x: u32 {
    0 | 1 | 2 => ..., // match on 3 different values
    4 | 5 => ...,     // match on 2 different values
    6 => ...,         // match on 1 value
    ! => ...,         // match on 0 values. Because this match is unsatisfiable
                      // the arm (everything right of and uncluding =>) is optional

    7 | ! => ...,     // only matches 7

    _ => ...,
}

However if people weren't forced to use this then it would be pretty pointless.

@Ericson2314

Copy link
Copy Markdown
Contributor

@canndrew yeah I prefer yours too, but I also prefer mine to the status quo so consider it a hedge :).

Also, thank you for the identify-of-| language! I was looking for something like that. I think that line of thinking will ultimately clarify what (5) is really about.

@Ericson2314

Copy link
Copy Markdown
Contributor

Hmm the clarity of ! might especially be good in irrefutable patterns (lets, function parameters).

@canndrew

Copy link
Copy Markdown
Contributor Author

So.... what's happening with this? I'm hearing rumors that decisions have been made here and there about how to handle empty patters, uninitialized etc? I wrote up some RFCs so that my views could find their way into that conversation, I don't know how successful that's been and I haven't managed to coax much information out the other way.

@aturon

aturon commented Sep 6, 2017

Copy link
Copy Markdown
Contributor

@canndrew Oof, my apologies for the total silence from the lang team. I'm going to nominate this RFC for discussion so we can bring it back into cache and try to suggest a trajectory.

@canndrew

canndrew commented Sep 6, 2017

Copy link
Copy Markdown
Contributor Author

@aturon That's fine, I recognize this isn't exactly a high priority.

@nikomatsakis

Copy link
Copy Markdown
Contributor

@rfcbot fcp postpone

We discussed this in the @rust-lang/lang meeting today. We would very much like to see progress towards stabilizing ! in general, but this particular point -- the question about the meaning of matching on an uninhabited type -- remains contentious and tied in with unsafe code. I move that we postpone this RFC, basically trying to move it into the unsafe code guidelines area. (Hopefully, we will also be trying to "reboot" progress in that department.)

@rfcbot

rfcbot commented Jan 18, 2018 •

Copy link
Copy Markdown

Team member @nikomatsakis has proposed to postpone this. The next step is review by the rest of the tagged teams:

No concerns currently listed.

Once these reviewers reach consensus, this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

@rfcbot rfcbot added the proposed-final-comment-period Currently awaiting signoff of all team members in order to enter the final comment period. label Jan 18, 2018
@rfcbot

rfcbot commented Jan 31, 2018

Copy link
Copy Markdown

🔔 This is now entering its final comment period, as per the review above. 🔔

1 similar comment
@rfcbot

rfcbot commented Jan 31, 2018

Copy link
Copy Markdown

🔔 This is now entering its final comment period, as per the review above. 🔔

@rfcbot rfcbot added final-comment-period Will be merged/postponed/closed in ~10 calendar days unless new substational objections are raised. and removed proposed-final-comment-period Currently awaiting signoff of all team members in order to enter the final comment period. labels Jan 31, 2018
@rfcbot

rfcbot commented Feb 10, 2018

Copy link
Copy Markdown

The final comment period is now complete.

@aturon

aturon commented Feb 14, 2018

Copy link
Copy Markdown
Contributor

Closing as postponed. Thanks @canndrew!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

final-comment-period Will be merged/postponed/closed in ~10 calendar days unless new substational objections are raised. T-lang Relevant to the language team, which will review and decide on the RFC.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

7 participants