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

Explain more on the difference of where constraints #4551

Merged
merged 5 commits into from
Nov 21, 2024

Conversation

danakj
Copy link
Contributor

@danakj danakj commented Nov 18, 2024

This adds language to explain where the types of constraints can or can not appear (attached-to an impl-as vs in-a type expression). And describes the impact of using a rewrite vs same-type constraint inside the body of the affected code, and thus why a rewrite is preferable when the constraint is of a single facet type.

@github-actions github-actions bot added the documentation An issue or proposed change to our documentation label Nov 18, 2024
@danakj danakj force-pushed the where-explain branch 2 times, most recently from 847b284 to 1a5aaab Compare November 18, 2024 20:12
This adds language to explain where the types of constraints can or can
not appear (attached-to an impl-as vs in-a type expression). And
describes the impact of using a rewrite vs same-type constraint inside
the body of the affected code, and thus why a rewrite is preferable when
the constraint is of a single facet type.
- Inside a type expression. Here it is used to constrain the possible values
of facets and/or their associated constants.
```
fn F[T: Interface where T.A impls OtherInterface](t: T) { ... }
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We currently don't allow you to use the name of the binding inside the type of the binding, so this is written instead like:

Suggested change
fn F[T: Interface where T.A impls OtherInterface](t: T) { ... }
fn F[T: Interface where .A impls OtherInterface](t: T) { ... }

@@ -2505,8 +2505,24 @@ binary operator:
- _Same-type constraints_: `where`...`==`...
- _Implements constraints_: `where`...`impls`...

And there are two positions that `where` can be written:
Copy link
Contributor

@josh11b josh11b Nov 19, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've been discussing this with @zygoloid , and we're ending up in a slightly different position. The right of an impl as declaration can have any where constraint. Rewrite constraints are the only thing that can assign values to associated constants. Other constraints are allowed, but would not normally be written. They can arise as part of using a named constraint, though, and when they do they have a meaning: if they are not satisfied by the impl declaration, a diagnostic will be issued. They don't otherwise enable anything in the impl, so it doesn't accomplish anything to write them.

Example of using a named constraint:

interface Container {
  let IteratorType:! Iterator;
}
constraint RandomContainer {
  extend Container where .IteratorType impls RandomAccessIterator;
}
// The following is equivalent to:
//    impl MyContainer as
//        (Container where .IteratorType impls RandomAccessIterator)
//        where .IteratorType = MyIteratorType
// This checks at compile time that `MyIteratorType impls RandomAccessIterator`,
// but is otherwise equivalent to:
//    impl MyContainer as Container where .IteratorType = MyIteratorType
impl MyContainer as RandomContainer where .IteratorType = MyIteratorType {
  // ...
}

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you think it would be fair to describe the named constraint case as a separate 3rd position, as it has different meaning there? Or is it important to note here that you could write that type of constraint on a class impl-as as well?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The design intent is that the language avoids distinguishing any kind of facet type from any other. This both simplifies the language and allows some evolution transitions to occur in a compatible way.

@danakj danakj requested a review from josh11b November 20, 2024 17:25
@@ -2534,20 +2531,19 @@ constraint.
> constraint is satisfied.

A same-type constraint is written `where X == Y`, where `X` and `Y` both name
facets. The constraint is that `X as type` must be the same as `Y as type`. It
can be used only in the type expression position.
facets. The constraint is that `X as type` must be the same as `Y as type`.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe say "It would normally only be used in the type expression position." here and below?

@danakj danakj requested a review from josh11b November 21, 2024 18:30
@josh11b josh11b added this pull request to the merge queue Nov 21, 2024
Merged via the queue into carbon-language:trunk with commit 4cf2c07 Nov 21, 2024
8 checks passed
@danakj danakj deleted the where-explain branch November 21, 2024 19:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation An issue or proposed change to our documentation
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants