Skip to content
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

Closed
catamorphism opened this issue Aug 26, 2011 · 15 comments
Closed

Implement nominal records #869

catamorphism opened this issue Aug 26, 2011 · 15 comments

Comments

@catamorphism
Copy link
Contributor

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 of type, like, for example:

record path_ = {global: bool, idents: [ident], types: [@ty]}
   : ast_util::same_len_non_empty(*.idents, *.types);

Constrained types would have to have nominal records (or simpler types) as their base types, not tuples or structural types.

@ghost ghost assigned catamorphism Aug 26, 2011
@graydon
Copy link
Contributor

graydon commented Aug 26, 2011

I remain ... unclear on the exact motive for this. Can you elaborate a bit?

@catamorphism
Copy link
Contributor Author

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 {x: 5, y:6}. What is the type of this record? {x: int, y:int}? Or, with constraints: {x:int, y:int} : odd(x), even(y)? Or {x:int, y:int} : lt(x, 6), lt(y, 7)`? Or... of course, an infinite number of possible types. Restricting constrained types to have a nominal record type as their base type lets us assign a unique type to any record literal.

@marijnh
Copy link
Contributor

marijnh commented Aug 27, 2011

do this:

tag myname = {field1: int, field2: str};

You now have a nominal record type (myname), that you construct with myname({field1: 10, field2: "hi"}). You can, as long as we have autoderef, then simply do value.field1 on the value, or *value to explicitly get out the record.

@catamorphism
Copy link
Contributor Author

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.

@msullivan
Copy link
Contributor

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?).

@catamorphism
Copy link
Contributor Author

Sully: you're right, my bad. The example declaration should have looked like:

record path_ = P {global: bool, idents: [ident], types: [@ty]}
   : ast_util::same_len_non_empty(*.idents, *.types);

where P would be the name of the constructor in this example. (Don't take the syntax too seriously.) Requiring a constructor is the entire point. That way, any preconditions/postconditions arising from the constraints in the type can get attached to the data constructor.

@graydon
Copy link
Contributor

graydon commented Aug 30, 2011

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?

@catamorphism
Copy link
Contributor Author

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." ?

@graydon
Copy link
Contributor

graydon commented Aug 30, 2011

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 { ... }.

@catamorphism
Copy link
Contributor Author

Oh, I see.

Supposing I write:

tag myname {
      myname ({field1: int, field2: str});
}

does Rust give any guarantees as to the runtime representation of myname? That is, is the eventual plan that the language should guarantee that the compiler won't box the inner product type {field1: int, field2: str} (in other words, will this behave like newtype in Haskell?)

@graydon
Copy link
Contributor

graydon commented Aug 30, 2011

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.

@marijnh
Copy link
Contributor

marijnh commented Aug 30, 2011

This is already optimized - one-variant tags never store their tag ID

@pcwalton
Copy link
Contributor

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.

@catamorphism
Copy link
Contributor Author

Patrick: I think that's right.

@graydon
Copy link
Contributor

graydon commented Feb 14, 2012

Whatever remains here is, I think, firmly in the bug on implementing classes. Closing as obsolete.

@graydon graydon closed this as completed Feb 14, 2012
@catamorphism catamorphism removed their assignment Jun 16, 2014
coastalwhite pushed a commit to coastalwhite/rust that referenced this issue Aug 5, 2023
Co-authored-by: bjorn3 <bjorn3@users.noreply.github.com>
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants