Match ergonomics design axioms and typing rules

# Match ergonomics redesign My own personal notes. Documents from the successive design meetings: - 2023-12-13: https://hackmd.io/YLKslGwpQOeAyGBayO9mdw - 2024-05-15: https://hackmd.io/9SstshpoTP60a8-LrxsWSA - 2024-06-07: https://hackmd.io/4hJmztFnS_KWG47Zemx-lw - Latest source for accepted rules: https://github.com/rust-lang/rfcs/pull/3627 ## Design axioms The ones that feel most crucial: 1. Patterns do what I mean: writing the right pattern doesn't require sigil-golf to appease the type-checker; 1. Patterns can be fully precise: I can spell out exactly which places I want to access with a pattern; - Consequence: in an unsafe block I have confidence I'm not triggering anything unexpected. 1. References get out of the way: I can write a pattern without `&`/`&mut`/`ref`/`ref mut` and it will do the obvious thing; 1. Patterns are polymorphic: the behavior of a pattern doesn't change if I make a generic type more specific; The ones that feel important to figure out the proposal: 5. References get out of the way: If I don't need mutability, I can treat `&mut T` like it's `&T`; 1. Mutability is predictable: A `&mut` pattern gives mutable access to the place inside it; 1. Mutability is predictable: A `&` pattern prevents mutable access to any place inside it; 1. If `x: &T`, I can copy out the value by writing `&` before the binding; 1. Inherited and real references are indistinguishable; 1. I can make any binding mutable by adding `mut` before it; Vaguer ones: 12. Patterns accomodate semantically-irrelevant code changes; 1. Patterns compose: `if let <pat1>(<pat2>) = <expr>` behaves the same as `if let <pat1>(x) = <expr> && let <pat2> = x`; 1. Patterns mirror expressions; 1. Patterns borrow as little as needed; We mostly have mirroring and composition for patterns without `&`/`&mut`/`ref`/`ref mut` (which I would call "purely structural patterns"). It gets tricky with references. We could also extend these to cover my other pattern work with axioms like: 16. Smart pointers get out of the way: the ergonomic distance between using a reference and a smart pointer is as small as necessary; 1. Patterns accomodate semantically-irrelevant code changes: switching from `Rc` to `Arc` should require minimal code changes; 1. Impossible cases can be omitted: I shouldn't have to write code for cases that are statically impossible; 1. Pattern semantics are predictable: I can tell what data a pattern touches by looking at it. This is crucial when matching on partially-initialized data. ## Typing rules NOTE: this has been superceded by further discussions; it is kept for posterity only. I want to formulate match ergonomics in terms of types, ideally as a typing rule. The rule would look like: `<pat> @ <expr> : <type>` so we can track which place is tested or used for bindings. Given a pattern `p` and a type `T`, we start with `p @ q: T` (where `q` is a dummy scrutinee expression to) and apply the rules. This will either error or assign each binding to an expression and a type. I implemented these rules and variations in a little tool: https://github.com/Nadrieril/typing-rust-patterns. The expression is the only implicit state that is tracked. This is a feature: implicit state is confusing. This means we don't get match ergonomics 2024 rule 3. Interestingly, the expression implicitly tracks the DBM: it can be either a place (corresponding to `move` DBM), `&<place>` (corresponding to `ref` DBM) or `&mut <place>` (corresponding to `ref mut` DBM). Note that we only inspect the expression for bindings, never in the middle of a pattern. Note: a rule looks like: ``` <precondition1>, <precondition2>, ... ------------------------------------- "Rule name" <postcondition>, <side conditions> ``` It is applied bottom-to-top. Read the rule like "to get `bottom thing`, if side conditions apply, we need `top things` to be (recursively) true". At most one rule should apply to any given case; if no rule applies, then the pattern is not valid for that type. The example derivations below should help understand how this works. ```rust //! Syntax of patterns: //! - `(mut)? (ref)? (mut)? x`: a binding; //! - `[p]`: a tuple with one elements; //! - `[p0, p1]`: a tuple with two elements; //! - `&p`, `&mut p`: dereferencing patterns. //! //! We use tuples for illustration; this applies identially to any adt patterns. //// Constructor rules /// Matching a constructor against its type p0 @ q.0: T0, p1 @ q.1: T1, .. -------------------------------- "Constructor" [p0, p1, ..] @ q: [T0, T1, ..] /// Matching a constructor against a reference p0 @ &(*q).0: &T0, p1 @ &(*q).1: &T1, .. ------------------------------------------ "ConstructorRef" [p0, p1, ..] @ q: &[T0, T1, ..] p0 @ &mut (*q).0: &mut T0, p1 @ &mut (*q).1: &mut T1, .. ---------------------------------------------------------- "ConstructorRef" [p0, p1, ..] @ q: &mut [T0, T1, ..] /// Matching a constructor against nested references [p0, ..] @ *q: &T ----------------- "ConstructorMultiRef" [p0, ..] @ q: &&T [p0, ..] @ &**q: &T --------------------- "ConstructorMultiRef" [p0, ..] @ q: &&mut T [p0, ..] @ *q: &T --------------------- "ConstructorMultiRef" [p0, ..] @ q: &mut &T [p0, ..] @ &mut **q: &mut T --------------------------- "ConstructorMultiRef" [p0, ..] @ q: &mut &mut T //// Dereferencing rules p @ *q: T ---------- "Deref(EatOuter)" &p @ q: &T p @ *q: T ------------------ "Deref(EatOuter)" &mut p @ q: &mut T // If we allow using a `&` pattern on `&mut` (aka match ergo 2024 rule 5). // The reborrow prevents `&(ref mut x)`, see the "Mutability is predictable" axiom. &p @ &*q: &T -------------- "DerefMutWithShared(EatOuter)" &p @ q: &mut T //// Binding rules // Success case let x: T = q ------------ "Binding" x @ q: T // The extra constraint on `q` is because we inspect the DBM. // If we removed the constraint we'd get the more natural behavior of "just working". let mut x: T = q ---------------------------------- "Binding" mut x @ q: T, q is not a reference // Stable behavior: `mut x` resets the DBM. // Error instead for match ergo 2024 rule 1. mut x @ q: T -------------- "MutBindingResetBindingMode" mut x @ &q: &T // Stable behavior: `mut x` resets the DBM. // Error instead for match ergo 2024 rule 1. mut x @ q: T ---------------------- "MutBindingResetBindingMode" mut x @ &mut q: &mut T // The extra constraint on `q` is to avoid referencing a temporary. x @ &q: &T ---------------------------------- "BindingBorrow" ref x @ q: T, q is not a reference x @ &mut q: &mut T -------------------------------------- "BindingBorrow" ref mut x @ q: T, q is not a reference // Stable behavior: `ref x` resets the DBM. ref x @ q: T -------------- "RefBindingResetBindingMode" ref x @ &q: &T ref x @ q: T ---------------------- "RefBindingResetBindingMode" ref x @ &mut q: &mut T ref mut x @ q: T ------------------ "RefBindingResetBindingMode" ref mut x @ &q: &T ref mut x @ q: T -------------------------- "RefBindingResetBindingMode" ref mut x @ &mut q: &mut T ``` Compared to the rules in https://github.com/rust-lang/rust/issues/127559: - Rule 1: :heavy_check_mark:; - Rule 2: partially: we do get `[&x]: &[&T] => x: &T` but not `[&mut x]: &[&mut T]`; - Rule 3: partially: we accept `&[[&x]]: &[&mut [T]]` but not `&[[x]]: &[&mut [T]]`; - Rule 4: I _think_ we do "rule 4 early", see the below derivations; - Rule 5: :heavy_check_mark:. ### Example derivations - `Some((&x, ref y)): &Option<(T, U)>` => `x: T`, `y: &U` ```rust Some((&x, ref y)) @ p: &Option<(T, U)> // <= (constructor rule) (&x, ref y) @ &(*p as Some).0: &(T, U) // <= (constructor rule) &x: &(*&(*p as Some).0).0: &T ref y: &(*&(*p as Some).0).1: &U // <= (dereferencing rule on the first one) x: *&(*&(*p as Some).0).0: T ref y: &(*&(*p as Some).0).1: &U // <= (binding rules on both, assuming the version of today's rust) let x: T = *&(*&(*p as Some).0).0 let y: &U = &(*&(*p as Some).0).1 // Final bindings (simplified): let x: T = (*p as Some).0.0; let y: &U = &(*p as Some).0.1; ``` - `[&x]: &[&T]` => `x: &T` ```rust [&x] @ p: &[&T] // Applying rule `ConstructorRef` &x @ &(*p).0: &&T // Applying rule `Deref(EatOuter)` x @ *&(*p).0: &T // Applying rule `Binding` let x: &T = *&(*p).0 // Final bindings (simplified): let x: &T = (*p).0; ``` - `[&x]: &[&mut T]` => `x: &mut T`, move error ```rust [&x] @ p: &[&mut T] // Applying rule `ConstructorRef` &x @ &(*p).0: &&mut T // Applying rule `Deref(EatOuter)` x @ *&(*p).0: &mut T // Applying rule `Binding` let x: &mut T = *&(*p).0 // Final bindings (simplified): let x: &mut T = (*p).0; // Borrow-check error: CantCopyRefMut ``` - `[&&mut x]: &[&mut T]` => `x: T` ```rust [&&mut x] @ p: &[&mut T] // Applying rule `ConstructorRef` &&mut x @ &(*p).0: &&mut T // Applying rule `Deref(EatOuter)` &mut x @ *&(*p).0: &mut T // Applying rule `Deref(EatOuter)` x @ **&(*p).0: T // Applying rule `Binding` let x: T = **&(*p).0 // Final bindings (simplified): let x: T = *(*p).0; ``` - `[&mut x]: &mut [&T]` => `x: &T` ```rust [&mut x] @ p: &mut [&T] // Applying rule `ConstructorRef` &mut x @ &mut (*p).0: &mut &T // Applying rule `Deref(EatOuter)` x @ *&mut (*p).0: &T // Applying rule `Binding` let x: &T = *&mut (*p).0 // Final bindings (simplified): let x: &T = (*p).0; ``` - `[&mut x]: &[&mut T]` => type error ```rust [&mut x] @ p: &[&mut T] // Applying rule `ConstructorRef` &mut x @ &(*p).0: &&mut T // Type error for `&mut x @ &(*p).0: &&mut T`: MutabilityMismatch ``` - `&[[x]]: &[&mut [T]]` => `x: &mut T`, borrow error ```rust &[[x]] @ p: &[&mut [T]] // Applying rule `Deref(EatOuter)` [[x]] @ *p: [&mut [T]] // Applying rule `Constructor` [x] @ (*p).0: &mut [T] // Applying rule `ConstructorRef` x @ &mut (*(*p).0).0: &mut T // Applying rule `Binding` let x: &mut T = &mut (*(*p).0).0 // Final bindings (simplified): let x: &mut T = &mut (*(*p).0).0; // Borrow-check error: MutBorrowBehindSharedBorrow ``` - `&[[&x]]: &[&mut [T]]` => `x: T`, borrow error if we don't use simplification rules ```rust &[[&x]] @ p: &[&mut [T]] // Applying rule `Deref(EatOuter)` [[&x]] @ *p: [&mut [T]] // Applying rule `Constructor` [&x] @ (*p).0: &mut [T] // Applying rule `ConstructorRef` &x @ &mut (*(*p).0).0: &mut T // Applying rule `DerefMutWithShared(EatOuter)` &x @ &*&mut (*(*p).0).0: &T // Applying rule `Deref(EatOuter)` x @ *&*&mut (*(*p).0).0: T // Applying rule `Binding` let x: T = *&*&mut (*(*p).0).0 // Final bindings (simplified): let x: T = (*(*p).0).0; ``` - `&[[&mut x]]: &[&mut [T]]` => `x: T`, borrow error if we don't use simplification rules ```rust &[[&mut x]] @ p: &[&mut [T]] // Applying rule `Deref(EatOuter)` [[&mut x]] @ *p: [&mut [T]] // Applying rule `Constructor` [&mut x] @ (*p).0: &mut [T] // Applying rule `ConstructorRef` &mut x @ &mut (*(*p).0).0: &mut T // Applying rule `Deref(EatOuter)` x @ *&mut (*(*p).0).0: T // Applying rule `Binding` let x: T = *&mut (*(*p).0).0 // Final bindings (simplified): let x: T = (*(*p).0).0; ``` - `[&ref mut x]: &mut [T]` => `x: &mut T`, borrow error ```rust [&ref mut x] @ p: &mut [T] // Applying rule `ConstructorRef` &ref mut x @ &mut (*p).0: &mut T // Applying rule `DerefMutWithShared(EatOuter)` &ref mut x @ &*&mut (*p).0: &T // Applying rule `Deref(EatOuter)` ref mut x @ *&*&mut (*p).0: T // Applying rule `BindingBorrow` x @ &mut *&*&mut (*p).0: &mut T // Applying rule `Binding` let x: &mut T = &mut *&*&mut (*p).0 // Final bindings (simplified): let x: &mut T = &mut *&(*p).0; // Borrow-check error: MutBorrowBehindSharedBorrow ```

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.