From f0ead22f0c014493ba66c76ad8830791cf98fa2a Mon Sep 17 00:00:00 2001 From: josh11b Date: Fri, 2 Jun 2023 16:05:46 -0700 Subject: [PATCH] Allow overlap with a `final impl` if identical (#2868) Allow an `impl` to overlap with a `final impl` if they agree on the overlap. Agreement is defined as all values comparing equal, and functions never comparing equal. Implements the decision in question-for-leads issue #1077. --- docs/design/generics/details.md | 51 +++++++++-- proposals/p2868.md | 147 ++++++++++++++++++++++++++++++++ 2 files changed, 189 insertions(+), 9 deletions(-) create mode 100644 proposals/p2868.md diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 38e005c1c3fc..dcc4d08da702 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4264,20 +4264,20 @@ generic function call, such as using an operator: // Interface defining the behavior of the prefix-* operator interface Deref { let Result:! type; - fn DoDeref[self: Self]() -> Result; + fn Op[self: Self]() -> Result; } // Types implementing `Deref` class Ptr(T:! type) { ... external impl as Deref where .Result = T { - fn DoDeref[self: Self]() -> Result { ... } + fn Op[self: Self]() -> Result { ... } } } class Optional(T:! type) { ... external impl as Deref where .Result = T { - fn DoDeref[self: Self]() -> Result { ... } + fn Op[self: Self]() -> Result { ... } } } @@ -4288,7 +4288,7 @@ fn F[T:! type](x: T) { The concern is the possibility of specializing `Optional(T) as Deref` or `Ptr(T) as Deref` for a more specific `T` means that the compiler can't assume -anything about the return type of `Deref.DoDeref` calls. This means `F` would in +anything about the return type of `Deref.Op` calls. This means `F` would in practice have to add a constraint, which is both verbose and exposes what should be implementation details: @@ -4307,14 +4307,14 @@ class Ptr(T:! type) { ... // Note: added `final` final external impl as Deref where .Result = T { - fn DoDeref[self: Self]() -> Result { ... } + fn Op[self: Self]() -> Result { ... } } } class Optional(T:! type) { ... // Note: added `final` final external impl as Deref where .Result = T { - fn DoDeref[self: Self]() -> Result { ... } + fn Op[self: Self]() -> Result { ... } } } @@ -4323,9 +4323,32 @@ class Optional(T:! type) { ``` This prevents any higher-priority impl that overlaps a final impl from being -defined. Further, if the Carbon compiler sees a matching final impl, it can -assume it won't be specialized so it can use the assignments of the associated -types in that impl definition. +defined unless it agrees with the `final` impl on the overlap. Overlap is +computed between two non-`template` `impl` declaration by +[unifying]() the +corresponding parts. For example, the intersection of these two declarations + +```carbon +final impl forall [T:! type] + T as CommonTypeWith(T) + where .Result = T {} + +impl forall [V:! type, U:! CommonTypeWith(V)] + Vec(U) as CommonTypeWith(Vec(V)) + where .Result = Vec(U.Result) {} +``` + +is found by unifying `T` with `Vec(U)` and `CommonTypeWith(T)` with +`CommonTypeWith(Vec(V))`. In this case, the intersection is when `T == Vec(U)` +and `U == V`. For templated `impl` declarations, overlap and agreement is +delayed until the template is instantiated with concrete types. + +Since we do not require the compiler to compare the definitions of functions, +agreement is only possible for interfaces without any function members. + +If the Carbon compiler sees a matching `final` impl, it can assume it won't be +specialized so it can use the assignments of the associated types in that impl +definition. ``` fn F[T:! type](x: T) { @@ -4336,6 +4359,16 @@ fn F[T:! type](x: T) { } ``` +**Alternatives considered:** + +- [Allow interfaces with member functions to compare equal](/proposals/p2868.md#allow-interfaces-with-member-functions-to-compare-equal) +- Mark associated constants as `final` instead of an `impl` declaration, in + proposals + [#983](/proposals/p0983.md#final-associated-constants-instead-of-final-impls) + and + [#2868](/proposals/p2868.md#mark-associated-constants-as-final-instead-of-an-impl-declaration) +- [Prioritize a `final impl` over a more specific `impl` on the overlap](/proposals/p2868.md#prioritize-a-final-impl-over-a-more-specific-impl-on-the-overlap) + #### Libraries that can contain a `final` impl To prevent the possibility of two unrelated libraries defining conflicting impl diff --git a/proposals/p2868.md b/proposals/p2868.md new file mode 100644 index 000000000000..c3c8f33c333e --- /dev/null +++ b/proposals/p2868.md @@ -0,0 +1,147 @@ +# Allow overlap with a `final impl` if identical + + + +[Pull request](https://github.com/carbon-language/carbon-lang/pull/2868) + + + +## Table of contents + +- [Abstract](#abstract) +- [Problem](#problem) +- [Background](#background) +- [Proposal](#proposal) +- [Rationale](#rationale) +- [Alternatives considered](#alternatives-considered) + - [Allow interfaces with member functions to compare equal](#allow-interfaces-with-member-functions-to-compare-equal) + - [Mark associated constants as `final` instead of an `impl` declaration](#mark-associated-constants-as-final-instead-of-an-impl-declaration) + - [Allow type inequality constraints](#allow-type-inequality-constraints) + - [Prioritize a `final impl` over a more specific `impl` on the overlap](#prioritize-a-final-impl-over-a-more-specific-impl-on-the-overlap) + + + +## Abstract + +Allow an `impl` to overlap with a `final impl` if they agree on the overlap. +Agreement is defined as all values comparing equal, and functions never +comparing equal. Implements the decision in question-for-leads +[issue #1077: find a way to permit impls of CommonTypeWith where the LHS and RHS type overlap](https://github.com/carbon-language/carbon-lang/issues/1077). + +## Problem + +The +[current design](https://github.com/carbon-language/carbon-lang/blob/trunk/docs/design/expressions/if.md#same-type) +includes a `final impl` declaration for the `CommonTypeWith(T)` interface: + +```carbon +final impl forall [T:! type] + T as CommonTypeWith(T) + where .Result = T {} +``` + +[Marking an `impl` declaration `final`](/docs/design/generics/details.md#final-impl-declarations), +prevents any overlapping implementation that would be considered more specific +by the [overlap rule](/docs/design/generics/details.md#overlap-rule). This +includes cases where the overlap is harmless, such as: + +```carbon +impl forall [U:! type, T:! CommonTypeWith(U)] + Vec(T) as CommonTypeWith(Vec(U)) + where .Result = Vec(T.Result) {} +``` + +This is an implementation we would like to define, along with a number of +similar cases. And this `impl` declaration doesn't actually conflict with the +previous `final impl` because the value of `Result`, the only member of the +`CommonTypeWith` interface, agrees where the two implementations overlap. + +## Background + +The `CommonTypeWith(T)` interface and `final impl` above were introduced in +[proposal #911: Conditional expressions](https://github.com/carbon-language/carbon-lang/pull/911). + +[Proposal #983: Generics details 7: final impls](https://github.com/carbon-language/carbon-lang/pull/983) +introduced and defined the rules for `final impl` declarations. + +The overlap rule was introduced in +[proposal #920](https://github.com/carbon-language/carbon-lang/pull/920). + +There were a number of different resolutions for this problem considered in +question-for-leads +[issue #1077: find a way to permit impls of CommonTypeWith where the LHS and RHS type overlap](https://github.com/carbon-language/carbon-lang/issues/1077). +This proposal codifies the resolution of that issue. + +## Proposal + +We allow an `impl` declaration to overlap with a `final impl` declaration if it +agrees on the overlap. Since we do not require the compiler to compare the +definitions of functions, agreement is only possible for interfaces without any +function members. The details about how the intersection is computed and how +templated `impl` declarations are handled have been added to +[the section on `final` impl declarations in the generics design doc](/docs/design/generics/details.md#final-impl-declarations). + +## Rationale + +This proposal is intentionally keeping the language small by making a simple +rule that addresses the only identified use case and nothing more. This benefits + +- [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem) +- [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write) + +by relying on Carbon's commitment to +[software and language evolution](/docs/project/goals.md#software-and-language-evolution) +to update our approach as needed, rather then trying to proactively address +concerns ahead of time. + +## Alternatives considered + +### Allow interfaces with member functions to compare equal + +There are some specific cases where the compiler can verify that two functions +are the same without having to compare their definitions. For example, two +implementations that don't implement a function and instead inherit the default +from the interface could be considered equal. This creates an evolution hazard, +though, that copying the definition from the interface into the implementation +means that the interface could now compare not equal without any change in +behavior. For now, the simple rule that we don't compare functions at all is +sufficient for our identified [use case](#problem). This is something we would +reconsider given new use cases. + +### Mark associated constants as `final` instead of an `impl` declaration + +The biggest benefit from knowing that an `impl` declaration won't be specialized +is being able to use the values of the associated constants, particularly +associated types. Thus, it is natural to focus on associated constants, which +don't have the same concerns as functions with comparing for equality. + +However, for the [motivating use case](#problem), we would still need this +proposal, just restricted to the associated constants that are declared `final`. +So we may still add this feature, if it is warranted by demand, but we did not +yet have that justification. This is essentially the same position as when this +feature was considered in +[proposal #983](/proposals/p0983.md#final-associated-constants-instead-of-final-impls). + +### Allow type inequality constraints + +Another approach would be to provide type inequality constraints so the more +specialized implementation could exclude the overlapping cases. This has some +downsides: + +- The more specialized implementation has to be aware of the `final` impl to + specifically exclude it. This would add extra steps to the development + process since this discovery is likely to occur as the result of a failed + compile. +- The more specialized implementation becomes more verbose, with extra + conditions that don't add any value. +- The current approach for establishing whether two types are equal doesn't in + general provide a way to show two types are not equal in generic code. + +### Prioritize a `final impl` over a more specific `impl` on the overlap + +This was a possible fix, but was seen as a bigger change that we didn't yet have +justification for.