查看类型 redux 和抽象字段 · 婴儿步伐

View Types Introduction: A few years ago, the author proposed view types as an extension to Rust's type system to address false inter-procedural borrow conflicts. The basic idea is to introduce "view types" like {f1, f2} Type, meaning an instance of Type where only specific fields can be accessed.
Example: The Data Type: The Data type collects experiments with names and f32 values, along with a counter successful. Helper functions are provided to access experiment names and data.
Tracking Successful Experiments Problem: Using the Data type as it is, there is a composition hazard. For example, when iterating over experiments and adjusting the successful counter, a borrow conflict occurs as the experiment_names function borrows self for the loop duration while add_successful requires a mutable borrow.
Using View Types to Fix: By changing function signatures to &{experiments} self and &mut {successful} Self, we can express what fields may be accessed. This allows the code to compile today and prevent future bugs.
Getting More Formal: View types can be integrated into Rust's type grammar, and a place expression is used to define a view onto a place. Checking field accesses against view types involves tracking the type of data and the allowed fields.
Inferring Allow Sets: When type-checking calls to functions with view types, place-set variables need to be inferred. These variables are used in inference and integrated into HIR type check inference.
Abstract Fields: Abstract fields allow us to address the problem of private field names becoming part of the interface. They are aliases for a set of fields and permit refactoring.
Frequently Asked Questions:
- Abstract fields can be mapped to an empty set.
- View types interact with traits and impls in various ways, such as implementing Deref for a view on a struct.
- View types can include more complex paths like {foo.bar} Baz.
- View types can be involved in moves.
- There are subtyping rules for view types.
- Abstract fields are useful in integrating with theorem provers and replacing phantom data.
- The parts of an abstract field include aliases for real fields, types for non-() abstract fields, and anonymous abstract fields.
- View types can potentially be applied to other types in the future.
Conclusion: The exploration of view types changed during writing. View types seem to be a useful type constructor on their own and need to be addressed in Rust. Prototype them in a-mir-formality to see if there are other surprises.