-
Notifications
You must be signed in to change notification settings - Fork 12.8k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Implement nominal records #869
Comments
I remain ... unclear on the exact motive for this. Can you elaborate a bit? |
Without nominal records, it's unclear how to introduce a record literal that has a constrained type. There are also some notes at https://github.com/graydon/rust/wiki/Constrained-types that explain some of the relevant thinking further. With nominal records, the constructor for a record that has a constrained type is analogous to a function with constraints on its arguments, and that way we have constrained types. Suppose we didn't have nominal records -- consider the record literal |
do this:
You now have a nominal record type ( |
Marijn: But we don't currently support constraints on variants. The documentation doesn't say anything about it either. I was thinking it might be useful, but that would also be an addition to the language. |
If you declared a nominal record {x: int, y: int} would this prevent you from using the structural record {x: str, y: str} somewhere else? I think we would want an explicit constructor for the nominal record (which might mean we should try to integrate it with single variant tags?). |
Sully: you're right, my bad. The example declaration should have looked like:
where |
I tend to favour marijn's suggestion here simply because it errs on the side of minimalism; we can do what you're trying to do here without adding an entirely new type constructor. Can we not just do that? |
Graydon: what do you think about the comment I directed at Marijn, specifically: "But we don't currently support constraints on variants. The documentation doesn't say anything about it either. I was thinking it might be useful, but that would also be an addition to the language." ? |
Sorry, I wasn't clear: I think that (constrained records) sounds like a smaller, easier change, so am requesting / suggesting that rather than a full additional type constructor. It achieves the same end, no? The only penalty is having to write foo({...}) rather than foo { ... }. |
Oh, I see. Supposing I write:
does Rust give any guarantees as to the runtime representation of |
I think if you do tag myname = { ... } then yes. Not sure when it prepends a word of tag-info these days, but in any case it wouldn't box the inner type. At worst just prepend a tag. |
This is already optimized - one-variant tags never store their tag ID |
If I understand this correctly, a constrained record cannot exist outside of a variant. This means that we would have to divide the universe of types into (all types minus constrained-record) and (all types including constrained record), and variant types would include the latter. This seems more complex to me than just having nominal records. |
Patrick: I think that's right. |
Whatever remains here is, I think, firmly in the bug on implementing classes. Closing as obsolete. |
Co-authored-by: bjorn3 <[email protected]>
* Only compile as binary target if verifying main function In order to verify a harness using `kani` command, user either have to have a `main` function defined in their crate or they have to set the env variable RUSTFLAGS to include --crate-type lib. With these changes, Kani will pick the crate type based on the --function argument. * Update call_single_file.rs
We should have nominal records at least as an option, in addition to structural records, whether or not we get rid of structural records.
A nominal record could be declared with
record
instead oftype
, like, for example:Constrained types would have to have nominal records (or simpler types) as their base types, not tuples or structural types.
The text was updated successfully, but these errors were encountered: