Associated constant assignment versus equality #2173
Conversation
zygoloid
added
proposal
zygoloid
force-pushed
the
proposal-assoc-const-where
branch
from
897c772
to
3a77036
Compare
zygoloid
changed the title
zygoloid
force-pushed
the
proposal-assoc-const-where
branch
from
3a77036
to
c13be2d
Compare
github-actions
bot
added
the
proposal rfc
Co-authored-by: josh11b <[email protected]>
Remove the "recursively uses the same rewrite" rule which appears to be unnecessary to guarantee termination.
Implements basic support for rewrite constraints as proposed in carbon-language#2173. Support for associated constants and complex constraints in general is also made more robust: argument deduction now properly computes and substitutes witnesses, and interface declarations track a more correct description of the constraint that they introduce than the one we previously built.
…sfied (#2294) Add checking that a type only satisfies a constraint if it satisfies all of that constraint's equality and rewrite constraints. Enforce the rule that `=` must be used in impls when specifying associated constant values rather than `==`. Turn off the pre-#2173 single-step equality behavior. This is getting somewhat ahead of the approved design, but it's a one-line change to restore the old behavior. Fix `CARBON_CHECK` to handle top-level `,`s in its argument, such as may happen in template argument lists, as this change introduces such a check.
) Instead of checking and resolving rewrites eagerly, defer doing so until a constraint is applied to a binding. Actual resolution of rewrites is not yet implemented, so this is mostly just refactoring, but the eventual goal is to support things like `(Constraint where .T = .U) & (Constraint where .U = V)` (however they are reached) by applying one rewrite to the other, as agreed with @josh11b in discussion of #2173. One nice consequence is that substitution into a constraint type no longer has a failure path, so substitution is once again not able to fail.
There was a problem hiding this comment.
Two real things I think are still needed here:
- Updating to the new terminology direction, and
- Clarifying (and maybe tweaking) the
impl asconstraints.
I'm suggesting (1) here even in the proposal because I suspect this particular proposal and write-up will end up fairly heavily read and cited, so it seems worthwhile to align it to the newer terminology and stuff like type to avoid confusion in the future.
proposals/p2173.md
Outdated
| rule cannot be readily understood by a developer nor effectively worked | ||
| around. | ||
| - Rust also has an | ||
| [undecidable type system (content warning: swear words)](https://sdleffler.github.io/RustTypeSystemTuringComplete/) |
There was a problem hiding this comment.
Trivial nit: slightly more precise / clear CW?
| [undecidable type system (content warning: swear words)](https://sdleffler.github.io/RustTypeSystemTuringComplete/) | |
| [undecidable type system (content warning: profanity)](https://sdleffler.github.io/RustTypeSystemTuringComplete/) |
Also, wow, this is such a rabbit hole of esoteric languages...
There was a problem hiding this comment.
I'd like to push back on this suggestion just a little: in this context, the word in question is not being used as profanity but simply as part of a proper noun, but it is nonetheless objectively a swear word. Happy to accept the suggestion if you still think it's a beneficial change given that argument.
There was a problem hiding this comment.
I see your point there.
I struggle with "swear words" because for me it seems like a slang term or idiom and doesn't unambiguously communicate the severity of the word choice. A result is that I'm not sure it'll serve its purpose reliably.
Maybe "obscenities" or "obscene words" or "obscene language" would work to avoid talking about the usage but still make the warning a bit more pointed?
There was a problem hiding this comment.
I've tried a rewrite to make this clearer, at the expense of being a lot more verbose :)
…or review comments.
only changing the semantics.
|
IS this ready for another round of review? (It wasn't marked as such, but looks like it might be...) |
Yes. What kind of marking are you looking for? |
There was a problem hiding this comment.
I think this is in great shape. One comment below is just a discussion topic I wrote down to avoid forgetting. The rest I think are super minor. If they all make sense, don't block, but feel free to ping for a quick look. I don't tihnk anything left needs re-reading significant sections.
Also, this is a fantastic write-up and I'm really excited about the whole thing. It's a remarkably complex problem and area, and the treatment here I think is great.
| import – and changing the type, such as by writing a different expression after | ||
| a `:` or `:!`. Changing the type of a value is expected to be able to change the |
There was a problem hiding this comment.
IIUC, with the new terminology, a different expression in type position doesn't change the type of the value any more? Guessing this is just another place needing a terminology update.
There was a problem hiding this comment.
What I mean here is that changing from a: i32 to a: f32 changes the type of a, and changing from T:! C to T:! C where .X = 5 changes the type of T. I think what you're observing is that changing from T:! C = i32 to T:! (C where .X = 5) = i32 doesn't change the type of a: T -- either way, it's a: i32, because the right-hand side of : is converted to type.
Is there some way I can update this paragraph to make it clearer what I'm talking about?
There was a problem hiding this comment.
I can't think of anything.
The root issue is "writing a different expression after a : or :!." -> we've just recently allowed that to not always change the type, so I get a little surprised when that is the first example of how to change the type of the value. But of course, it is, and different expressions that don't change the type of the value are the exception and not the rule. So I think its ultimately fine. =D
proposals/p2173.md
Outdated
| rule cannot be readily understood by a developer nor effectively worked | ||
| around. | ||
| - Rust also has an | ||
| [undecidable type system (content warning: swear words)](https://sdleffler.github.io/RustTypeSystemTuringComplete/) |
There was a problem hiding this comment.
I see your point there.
I struggle with "swear words" because for me it seems like a slang term or idiom and doesn't unambiguously communicate the severity of the word choice. A result is that I'm not sure it'll serve its purpose reliably.
Maybe "obscenities" or "obscene words" or "obscene language" would work to avoid talking about the usage but still make the warning a bit more pointed?
| import – and changing the type, such as by writing a different expression after | ||
| a `:` or `:!`. Changing the type of a value is expected to be able to change the |
There was a problem hiding this comment.
I can't think of anything.
The root issue is "writing a different expression after a : or :!." -> we've just recently allowed that to not always change the type, so I get a little surprised when that is the first example of how to change the type of the value. But of course, it is, and different expressions that don't change the type of the value are the exception and not the rule. So I think its ultimately fine. =D
First step in updating `docs/design/generics/details.md`. It incorporates changes from proposals: #989 #2138 #2173 #2200 #2360 #2964 #3162 , but there are still more changes from those proposals to be made. It also switches away from suggesting static-dispatch witness tables, and creates an appendix to describe that decision. --------- Co-authored-by: Richard Smith <[email protected]>
Continued from part 1: #3231. Second step updating `docs/design/generics/details.md`. There remains some work to incorporate proposal #2200. - The biggest changes are incorporating much of the text of proposals: - #2173 - #2687 - It incorporates changes from proposals: - #989 - #1178 - #2138 - #2200 - #2360 - #2964 - #3162 - It also updates the text to reflect the latest thinking from leads issues: - #996 - #2153 -- most notably deleting the section on `TypeId`. - Update to rule for prioritization blocks with mixed type structures from [discussion on 2023-07-18](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.7jxges9ojgy3) - Adds reference links to proposals, issues, and discussions relevant to the text. - Also tries to use more precise language when talking about implementations, to avoid confusing `impl` declaration and definitions with the `impls` operator used in `where` clauses, an issue brought up in - #2495 - #2483 --------- Co-authored-by: Richard Smith <[email protected]>
Split the
where A == Bconstraint in two:where .A = Bproduces a newconstraint from an old one, where the value of
.Ain the new constraint isknown and eagerly rewritten to
B, andwhere A == B, which does not causeAandBto be considered as identical by language rules but does permitimplicit (no-op) conversion between them.
This aims to provide an efficiently-computable and human-understandable type
equality rule, with type canonicalization and therefore transitive type
equality, without sacrificing too much in the way of ergonomics and without
sacrificing determinism, while still providing the full power of a general type
constraint system in a less ergonomic form.