From 6cd9e53b9199b53fa8a29cc6913a6c702abecc55 Mon Sep 17 00:00:00 2001 From: Josh L Date: Wed, 16 Feb 2022 13:15:58 -0800 Subject: [PATCH 01/20] Filling out template with PR 1088 --- proposals/p1088.md | 62 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 proposals/p1088.md diff --git a/proposals/p1088.md b/proposals/p1088.md new file mode 100644 index 0000000000000..77d7b5cefe87e --- /dev/null +++ b/proposals/p1088.md @@ -0,0 +1,62 @@ +# Generic details 10: interface implemented requirements + + + +[Pull request](https://github.com/carbon-language/carbon-lang/pull/1088) + + + +## Table of contents + +- [Problem](#problem) +- [Background](#background) +- [Proposal](#proposal) +- [Details](#details) +- [Rationale based on Carbon's goals](#rationale-based-on-carbons-goals) +- [Alternatives considered](#alternatives-considered) + + + +## Problem + +TODO: What problem are you trying to solve? How important is that problem? Who +is impacted by it? + +## Background + +TODO: Is there any background that readers should consider to fully understand +this problem and your approach to solving it? + +## Proposal + +TODO: Briefly and at a high level, how do you propose to solve the problem? Why +will that in fact solve it? + +## Details + +TODO: Fully explain the details of the proposed solution. + +## Rationale based on Carbon's goals + +TODO: How does this proposal effectively advance Carbon's goals? Rather than +re-stating the full motivation, this should connect that motivation back to +Carbon's stated goals for the project or language. This may evolve during +review. Use links to appropriate goals, for example: + +- [Community and culture](/docs/project/goals.md#community-and-culture) +- [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem) +- [Performance-critical software](/docs/project/goals.md#performance-critical-software) +- [Software and language evolution](/docs/project/goals.md#software-and-language-evolution) +- [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write) +- [Practical safety and testing mechanisms](/docs/project/goals.md#practical-safety-and-testing-mechanisms) +- [Fast and scalable development](/docs/project/goals.md#fast-and-scalable-development) +- [Modern OS platforms, hardware architectures, and environments](/docs/project/goals.md#modern-os-platforms-hardware-architectures-and-environments) +- [Interoperability with and migration from existing C++ code](/docs/project/goals.md#interoperability-with-and-migration-from-existing-c-code) + +## Alternatives considered + +TODO: What alternative solutions have you considered? From 02a69c0ed34da087f791dc1930fce7308f86f857 Mon Sep 17 00:00:00 2001 From: Josh L Date: Wed, 16 Feb 2022 14:40:24 -0800 Subject: [PATCH 02/20] Initial list of things to do --- proposals/p1088.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/proposals/p1088.md b/proposals/p1088.md index 77d7b5cefe87e..1ffe8599efe35 100644 --- a/proposals/p1088.md +++ b/proposals/p1088.md @@ -33,6 +33,21 @@ this problem and your approach to solving it? ## Proposal +- Requiring another type to implement an interface + ``` + interface IntLike { + impl i32 as As(Self); + } + interface CommonTypeWith(T:! Type) { + impl T as CommonTypeWith(Self); + } + ``` +- Difficulty of `where` clauses, see + [discussion in #generics on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940), + [examples of problematic overlap that can't be checked locally](https://gist.github.com/zygoloid/2023db2ac55cd517c6e2732e3c37fd08/revisions) +- Observe declarations for saying types implement interfaces, see + [discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) + TODO: Briefly and at a high level, how do you propose to solve the problem? Why will that in fact solve it? From 3052c790fa155ddd99d76b3eb2ec0d81569d701d Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 17 Feb 2022 15:49:17 -0800 Subject: [PATCH 03/20] Checkpoint progress. --- docs/design/generics/details.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 356da99dbf463..8a80925642199 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -1172,6 +1172,8 @@ def DoHashAndEquals[T:! Hashable](x: T) { **Comparison with other languages:** [This feature is called "Supertraits" in Rust](https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#using-supertraits-to-require-one-traits-functionality-within-another-trait). +**Note:** The design for this feature is continued in a later section. FIXME + ### Interface extension When implementing an interface, we should allow implementing the aliased names @@ -4433,6 +4435,21 @@ There are a few reasons for this feature: Note that this applies to associated entities, not interface parameters. +# Interface requiring other interfaces revisited + +Recall that an +[interface can require another interface be implemented for the type](#interface-requiring-other-interfaces), +as in: + +``` +interface Iterable { + fn Advance[addr me: Self*]() -> bool; + impl as Equatable; +} +``` + +FIXME + ## Future work ### Dynamic types From 2566085a186c2994141ba0565f6e5799e7266354 Mon Sep 17 00:00:00 2001 From: Josh L Date: Sat, 19 Feb 2022 08:35:07 -0800 Subject: [PATCH 04/20] Observe blanket impls --- docs/design/generics/details.md | 6 ++++-- proposals/p1088.md | 22 ++++++++++++++++++++++ 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 8a80925642199..28536f701ede5 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -95,6 +95,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Interface members with definitions](#interface-members-with-definitions) - [Interface defaults](#interface-defaults) - [`final` members](#final-members) +- [Interface requiring other interfaces revisited](#interface-requiring-other-interfaces-revisited) - [Future work](#future-work) - [Dynamic types](#dynamic-types) - [Runtime type parameters](#runtime-type-parameters) @@ -1172,7 +1173,8 @@ def DoHashAndEquals[T:! Hashable](x: T) { **Comparison with other languages:** [This feature is called "Supertraits" in Rust](https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#using-supertraits-to-require-one-traits-functionality-within-another-trait). -**Note:** The design for this feature is continued in a later section. FIXME +**Note:** The design for this feature is continued in +[a later section](#interface-requiring-other-interfaces-revisited). ### Interface extension @@ -4435,7 +4437,7 @@ There are a few reasons for this feature: Note that this applies to associated entities, not interface parameters. -# Interface requiring other interfaces revisited +## Interface requiring other interfaces revisited Recall that an [interface can require another interface be implemented for the type](#interface-requiring-other-interfaces), diff --git a/proposals/p1088.md b/proposals/p1088.md index 1ffe8599efe35..dde960a886ef6 100644 --- a/proposals/p1088.md +++ b/proposals/p1088.md @@ -47,6 +47,28 @@ this problem and your approach to solving it? [examples of problematic overlap that can't be checked locally](https://gist.github.com/zygoloid/2023db2ac55cd517c6e2732e3c37fd08/revisions) - Observe declarations for saying types implement interfaces, see [discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) + and not just for interface-interface dependencies, but also blanket impls + + ``` + interface A { } + interface B { } + interface C { } + interface D { } + impl [T:! A] T as B { } + impl [T:! B] T as C { } + impl [T:! C] T as D { } + fn RequiresD(T:! D)(x: T); + fn RequiresA(T:! A)(x: T) { + // Illegal: No implementation of D for type T implementing A + // RequiresD(x); + // T is B from implementation of B from A + observe T is B; + // T is C from implementation of C from B + observe T is C; + // Allowed: Implementation of D from C + RequiresD(x); + } + ``` TODO: Briefly and at a high level, how do you propose to solve the problem? Why will that in fact solve it? From 0b265c997170cf9abaef2274d03972d13a0e2c7e Mon Sep 17 00:00:00 2001 From: Josh L Date: Tue, 22 Feb 2022 17:48:57 -0800 Subject: [PATCH 05/20] Basic interface requirements on other types --- docs/design/generics/details.md | 73 ++++++++++++++++++++++++++++++++- 1 file changed, 72 insertions(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 28536f701ede5..9b0d632672494 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4445,11 +4445,81 @@ as in: ``` interface Iterable { - fn Advance[addr me: Self*]() -> bool; impl as Equatable; + // ... +} +``` + +This states that the type implementing the interface `Iterable`, which in this +context is called `Self`, must also implement the interface `Equatable`. As is +done with [conditional conformance](#conditional-conformance), we allow another +type to be specified between `impl` and `as` to say some type other than `Self` +must implement an interface. For example, + +``` +interface IntLike { + impl i32 as As(Self); + // ... +} +``` + +says that if `Self` implements `IntLike`, then `i32` must implement `As(Self)`. +Similarly, + +``` +interface CommonTypeWith(T:! Type) { + impl T as CommonTypeWith(Self); + // ... } ``` +says that if `Self` implements `CommonTypeWith(T)`, then `T` must implement +`CommonTypeWith(Self)`. + +The previous description of `impl as` in an interface definition matches the +behavior of using a default of `Self` when the type between `impl` and `as` is +omitted. So the previous definition of `interface Iterable` is equivalent to: + +``` +interface Iterable { + // ... + impl Self as Equatable; + // Equivalent to: impl as Equatable; +} +``` + +When implementing an interface with an `impl as` requirement, that requirement +must be satisfied either by an implementation in an imported library or an +implementation somewhere in the same file. Implementing the requiring interface +is a promise that the requirement will be implemented. This is like a + + + +forward declaration of an impl except that the definition can be broader instead +of being required to match exactly. + +``` +external impl Vector(i32) as Iterable { ... } + +fn RequiresEquatable[T:! Equatable](x: T) { ... } +fn ProcessVector(v: Vector(i32)) { + // ✅ Allowed since `Vector(i32)` is known to + // implement `Equatable`. + RequiresEquatable(v); +} + +// Satisfies requirement that `Vector(i32)` must +// implement `Iterable` since `i32` is `Equatable`. +external impl Vector(T:! Equatable) as Equatable { ... } +``` + +In some cases, the interface's requirement can be trivially satisfied by the +implementation itself, as in: + +``` +impl [T:! Type] T as CommonTypeWith(T) { ... } +``` + FIXME ## Future work @@ -4582,3 +4652,4 @@ be included in the declaration as well. - [#983: Generic details 7: final impls](https://github.com/carbon-language/carbon-lang/pull/983) - [#990: Generics details 8: interface default and final members](https://github.com/carbon-language/carbon-lang/pull/990) - [#1013: Generics: Set associated constants using where constraints](https://github.com/carbon-language/carbon-lang/pull/1013) +- [#1088: Generic details 10: interface implemented requirements](https://github.com/carbon-language/carbon-lang/pull/1088) From 5fda34513a25a54935f589b662a14ceb9e12163d Mon Sep 17 00:00:00 2001 From: Josh L Date: Tue, 22 Feb 2022 18:07:19 -0800 Subject: [PATCH 06/20] Sketching remaining sections --- docs/design/generics/details.md | 61 ++++++++++++++++++++++++++++++++- 1 file changed, 60 insertions(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 9b0d632672494..04903f254d70f 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -96,6 +96,10 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Interface defaults](#interface-defaults) - [`final` members](#final-members) - [Interface requiring other interfaces revisited](#interface-requiring-other-interfaces-revisited) + - [Requirements with `where` constraints](#requirements-with-where-constraints) +- [Observing a type implements an interface](#observing-a-type-implements-an-interface) + - [Observing interface requirements](#observing-interface-requirements) + - [Observing blanket impls](#observing-blanket-impls) - [Future work](#future-work) - [Dynamic types](#dynamic-types) - [Runtime type parameters](#runtime-type-parameters) @@ -4520,7 +4524,62 @@ implementation itself, as in: impl [T:! Type] T as CommonTypeWith(T) { ... } ``` -FIXME +### Requirements with `where` constraints + +FIXME: +[discussion in #generics on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940), +[examples of problematic overlap that can't be checked locally](https://gist.github.com/zygoloid/2023db2ac55cd517c6e2732e3c37fd08/revisions) + +## Observing a type implements an interface + +An [`observe` declaration](#observe-declarations) to show that two types are +equal so code can pass type checking without explicitly writing casts, without +requiring the compiler to do a unbounded search that may not terminate. The +compiler may need another form of `observe` declaration to see that a type +implements an interface. + +### Observing interface requirements + +FIXME: +[Interface requiring other interfaces revisited](#interface-requiring-other-interfaces-revisited) + +FIXME: +[discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) + +### Observing blanket impls + +FIXME: [Blanket impls](#blanket-impls) + +``` +interface A { } +interface B { } +interface C { } +interface D { } + +impl [T:! A] T as B { } +impl [T:! B] T as C { } +impl [T:! C] T as D { } + +fn RequiresD(T:! D)(x: T); + +fn RequiresA(T:! A)(x: T) { + // ❌ Illegal: No implementation of `D` for type + // `T` implementing `A` + // RequiresD(x); + + // There is a blanket implementation of `B` for + // types implementing `A`. + observe T is B; + + // There is a blanket implementation of `C` for + // types implementing `B`. + observe T is C; + + // ✅ Allowed: There is a blanket implementation + // of `D` for types implementing `C`. + RequiresD(x); +} +``` ## Future work From 13a47687e8e594395e667fea0c40090ca6349416 Mon Sep 17 00:00:00 2001 From: Josh L Date: Fri, 4 Mar 2022 22:34:05 +0000 Subject: [PATCH 07/20] Restrictions on `where` clauses. --- docs/design/generics/details.md | 25 +++++++- proposals/p1088.md | 105 ++++++++++++++++++++++++-------- 2 files changed, 103 insertions(+), 27 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 04903f254d70f..23e9321abf9bd 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4526,9 +4526,28 @@ impl [T:! Type] T as CommonTypeWith(T) { ... } ### Requirements with `where` constraints -FIXME: -[discussion in #generics on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940), -[examples of problematic overlap that can't be checked locally](https://gist.github.com/zygoloid/2023db2ac55cd517c6e2732e3c37fd08/revisions) +An interface implementation requirement with a `where` clause is harder to +satisfy. Consider an interface `B` that has a requirement that interface `A` is +also implemented. + +``` +interface A(T:! Type) { + let Result:! Type; +} +interface B(T:! Type) { + impl as A(T) where .Result == i32; +} +``` + +An implementation of `B` for a set of types can only be valid if there is a +visible implementation of `A` with the same `T` parameter for those types with +the `.Result` associated type set to `i32`. That is +[not sufficient](/proposals/p1088.md#less-strict-about-requirements-with-where-clauses), +though, unless the implementation of `A` can't be specialized, either because it +is [marked `final`](#final-impls) or is not +[parameterized](#parameterized-impls). Implementations in other libraries can't +make `A` be implemented for fewer types, but can cause `.Result` to have a +different assignment. ## Observing a type implements an interface diff --git a/proposals/p1088.md b/proposals/p1088.md index dde960a886ef6..e799169f90644 100644 --- a/proposals/p1088.md +++ b/proposals/p1088.md @@ -18,6 +18,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Details](#details) - [Rationale based on Carbon's goals](#rationale-based-on-carbons-goals) - [Alternatives considered](#alternatives-considered) + - [Less strict about requirements with `where` clauses](#less-strict-about-requirements-with-where-clauses) @@ -42,34 +43,11 @@ this problem and your approach to solving it? impl T as CommonTypeWith(Self); } ``` -- Difficulty of `where` clauses, see - [discussion in #generics on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940), - [examples of problematic overlap that can't be checked locally](https://gist.github.com/zygoloid/2023db2ac55cd517c6e2732e3c37fd08/revisions) +- Difficulty of `where` clauses. - Observe declarations for saying types implement interfaces, see [discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) and not just for interface-interface dependencies, but also blanket impls - ``` - interface A { } - interface B { } - interface C { } - interface D { } - impl [T:! A] T as B { } - impl [T:! B] T as C { } - impl [T:! C] T as D { } - fn RequiresD(T:! D)(x: T); - fn RequiresA(T:! A)(x: T) { - // Illegal: No implementation of D for type T implementing A - // RequiresD(x); - // T is B from implementation of B from A - observe T is B; - // T is C from implementation of C from B - observe T is C; - // Allowed: Implementation of D from C - RequiresD(x); - } - ``` - TODO: Briefly and at a high level, how do you propose to solve the problem? Why will that in fact solve it? @@ -97,3 +75,82 @@ review. Use links to appropriate goals, for example: ## Alternatives considered TODO: What alternative solutions have you considered? + +### Less strict about requirements with `where` clauses + +We could allow +[requirements with `where` constraints](/docs/design/generics/details.md#requirements-with-where-constraints) +to be satisfied by implementations that could be specialized, as long as the +constraints were still satisfied. Unfortunately, this is not a condition that +can be checked locally. Continuing the example from that section, consider four +packages + +- A package defining the two interfaces + + ``` + package Interfaces api; + interface A(T:! Type) { + let Result:! Type; + } + interface B(T:! Type) { + impl as A(T) where .Result == i32; + } + ``` + +- A package defining a type that is used as a parameter to interfaces `A` and + `B` in blanket impls: + + ``` + package Param api; + import Interfaces; + class P {} + external impl [T:! Type] T as Interfaces.A(P) where .Result = i32 { } + // Question:Is this blanket impl of `Interfaces.A(P)` sufficient + // to allow us to make this blanket impl of `Interfaces.B(P)`? + external impl [T:! Type] T as Interfaces.B(P) { } + ``` + +- A package defining a type that implements the interface `A` with a wildcard + impl: + + ``` + package Class api; + import Interfaces; + class C {} + external impl [T:! Type] C as Interfaces.A(T) where .Result = bool { } + ``` + +- And a package that tries to use the above packages together: + + ``` + package Main; + import Interfaces; + import Param; + import Class; + + fn F[V:! Interfaces.B(Param.P)](x: V); + fn Run() { + var c: Class.C = {}; + // Does Class.C implement Interfaces.B(Param.P)? + F(c); + } + ``` + +Package `Param` has an implementation of `Interfaces.B(Param.P)` for any `T`, +which should include `T == Class.C`. The requirement in `Interfaces.B` in this +case is that `T == Class.C` must implement `Interfaces.A(Param.P)`, which it +does, and `Class.C.(Interfaces.A(Param.P).Result)` must be `i32`. This would +hold using the blanket implementation defined in `Param`, but the wildcard impl +defined in package `Class` has higher priority and sets the associated type +`.Result` to `bool` instead. + +The conclusion is that this problem would only be detected during +monomorphization, and could cause independent libraries to be incompatible with +each other even when they work separately. These were significant enough +downsides that we wanted to see if we could live with the restrictions that +allowed local checking first. We don't know if developers will want to declare +their parameterized implementations `final` in this situation anyway, even with +[the limitations on `final`](/docs/design/generics/details.md#libraries-that-can-contain-final-impls). + +This problem was discussed in +[the #generics channel on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940). From ff4ecb1f7d0361fefba54cf39e3f0dd12606eae0 Mon Sep 17 00:00:00 2001 From: Josh L Date: Sat, 5 Mar 2022 01:48:23 +0000 Subject: [PATCH 08/20] observe...is --- docs/design/generics/details.md | 60 ++++++++++++++++++++++++++------- proposals/p1088.md | 26 +++++++++++--- 2 files changed, 69 insertions(+), 17 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 23e9321abf9bd..79f49b865897b 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -3730,12 +3730,6 @@ types, possibly with different implementations. In general, `X(T).F` can only mean one thing, regardless of `T`. -**Concern:** The conditional conformance feature makes the question "is this -interface implemented for this type" undecidable in general. -[This feature in Rust has been shown to allow implementing a Turing machine](https://sdleffler.github.io/RustTypeSystemTuringComplete/). -The acyclic restriction may eliminate this issue, otherwise we will likely need -some heuristic like a limit on how many steps of recursion are allowed. - **Comparison with other languages:** [Swift supports conditional conformance](https://github.com/apple/swift-evolution/blob/master/proposals/0143-conditional-conformances.md), but bans cases where there could be ambiguity from overlap. @@ -4551,16 +4545,51 @@ different assignment. ## Observing a type implements an interface -An [`observe` declaration](#observe-declarations) to show that two types are -equal so code can pass type checking without explicitly writing casts, without -requiring the compiler to do a unbounded search that may not terminate. The -compiler may need another form of `observe` declaration to see that a type +An [`observe` declaration](#observe-declarations) can be used to show that two +types are equal so code can pass type checking without explicitly writing casts, +without requiring the compiler to do a unbounded search that may not terminate. +The compiler may need another form of `observe` declaration to see that a type implements an interface. ### Observing interface requirements -FIXME: -[Interface requiring other interfaces revisited](#interface-requiring-other-interfaces-revisited) +One situation where this occurs is when there is a chain of +[interfaces requiring other interfaces](#interface-requiring-other-interfaces-revisited). +Normally, Carbon will only consider the interfaces that are direct requirements +of the interfaces the type is known to implement. An `observe...is` declaration +can be used to add an interface that is a direct requirement to the set of +interfaces whose direct requirements will be considered for that type. This +allows a developer to provide a proof that there is a sequence of requirements +that demonstrate that a type implements an interface, as in this example: + +``` +interface A { } +interface B { impl as A; } +interface C { impl as B; } +interface D { impl as C; } + +fn RequiresA[T:! A](x: T); +fn RequiresC[T:! C](x: T); +fn RequiresD[T:! D](x: T) { + // ✅ Allowed: `D` directly requires `C` to be implemented. + RequiresC(x); + + // ❌ Illegal: No direct connection between `D` and `A`. + // RequiresA(x); + + // `T` is `D` and `D` directly requires `C` to be + // implemented. + observe T is C; + + // `T` is `C` and `C` directly requires `B` to be + // implemented. + observe T is B; + + // ✅ Allowed: `T` is `B` and `B` directly requires + // `A` to be implemented. + RequiresA(x); +} +``` FIXME: [discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) @@ -4580,8 +4609,13 @@ impl [T:! B] T as C { } impl [T:! C] T as D { } fn RequiresD(T:! D)(x: T); +fn RequiresB(T:! B)(x: T); fn RequiresA(T:! A)(x: T) { + // ✅ Allowed: There is a blanket implementation + // of `B` for types implementing `A`. + RequiresB(x); + // ❌ Illegal: No implementation of `D` for type // `T` implementing `A` // RequiresD(x); @@ -4730,4 +4764,4 @@ be included in the declaration as well. - [#983: Generic details 7: final impls](https://github.com/carbon-language/carbon-lang/pull/983) - [#990: Generics details 8: interface default and final members](https://github.com/carbon-language/carbon-lang/pull/990) - [#1013: Generics: Set associated constants using where constraints](https://github.com/carbon-language/carbon-lang/pull/1013) -- [#1088: Generic details 10: interface implemented requirements](https://github.com/carbon-language/carbon-lang/pull/1088) +- [#1088: Generic details 10: interface-implemented requirements](https://github.com/carbon-language/carbon-lang/pull/1088) diff --git a/proposals/p1088.md b/proposals/p1088.md index e799169f90644..a3d9bc0ecb1e8 100644 --- a/proposals/p1088.md +++ b/proposals/p1088.md @@ -1,4 +1,4 @@ -# Generic details 10: interface implemented requirements +# Generic details 10: interface-implemented requirements @@ -44,9 +45,8 @@ this problem and your approach to solving it? } ``` - Difficulty of `where` clauses. -- Observe declarations for saying types implement interfaces, see - [discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) - and not just for interface-interface dependencies, but also blanket impls +- Observe declarations for saying types implement interfaces, and not just for + interface-interface dependencies, but also blanket impls TODO: Briefly and at a high level, how do you propose to solve the problem? Why will that in fact solve it? @@ -154,3 +154,21 @@ their parameterized implementations `final` in this situation anyway, even with This problem was discussed in [the #generics channel on Discord](https://discord.com/channels/655572317891461132/941071822756143115/941089885475962940). + +### Don't require `observe...is` declarations + +We could require the Carbon compiler to do a search to discover all interfaces +that are transitively implied from knowing that a type implements a set of +interfaces. However, we don't have a good way of bounding the depth of that +search. + +In fact, this search combined with conditional conformance makes the question +"is this interface implemented for this type" undecidable +[in Rust](https://sdleffler.github.io/RustTypeSystemTuringComplete/). Note: it +is possible that +[the acyclic rule](/docs/design/generics/details.md#acyclic-rule) would avoid +this problem in Carbon for blanket impls, but it doesn't apply to interface +requirements. + +This problem was observed in +[a discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848). From cd38ea6f47c6260e1abfd3bc6392ae53ad6e1277 Mon Sep 17 00:00:00 2001 From: Josh L Date: Mon, 7 Mar 2022 19:31:20 +0000 Subject: [PATCH 09/20] Observe blanket impls --- docs/design/generics/details.md | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 79f49b865897b..abc817b2a8ba6 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4591,12 +4591,12 @@ fn RequiresD[T:! D](x: T) { } ``` -FIXME: -[discussion in #typesystem on Discord](https://discord.com/channels/655572317891461132/708431657849585705/938167784565792848) - ### Observing blanket impls -FIXME: [Blanket impls](#blanket-impls) +An `observe...is` declaration can also be used to observe that a type implements +an interface because there is a [blanket impl](#blanket-impls) in terms of +requirements a type is already known to satisfy. Without an `observe` +declaration, Carbon will only use blanket impls that are directly satisfied. ``` interface A { } @@ -4634,6 +4634,10 @@ fn RequiresA(T:! A)(x: T) { } ``` +In the case of an error, a quality Carbon implementation will do a deeper search +for chains of requirements and blanket impls and suggest `observe` declarations +that would make the code compile if any solution is found. + ## Future work ### Dynamic types From 7aa3b0033e2272a8fe52465874eda459a6f48345 Mon Sep 17 00:00:00 2001 From: Josh L Date: Mon, 7 Mar 2022 20:09:32 +0000 Subject: [PATCH 10/20] Proposal text --- proposals/p1088.md | 69 ++++++++++++++++++++-------------------------- 1 file changed, 30 insertions(+), 39 deletions(-) diff --git a/proposals/p1088.md b/proposals/p1088.md index a3d9bc0ecb1e8..0931528f4e65c 100644 --- a/proposals/p1088.md +++ b/proposals/p1088.md @@ -15,7 +15,6 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Problem](#problem) - [Background](#background) - [Proposal](#proposal) -- [Details](#details) - [Rationale based on Carbon's goals](#rationale-based-on-carbons-goals) - [Alternatives considered](#alternatives-considered) - [Less strict about requirements with `where` clauses](#less-strict-about-requirements-with-where-clauses) @@ -25,56 +24,48 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception ## Problem -TODO: What problem are you trying to solve? How important is that problem? Who -is impacted by it? +This proposal is to add the capability for an interface to require other types +to be implemented, not just the `Self` type. The interface-implemented +requirement feature also has some concerns: + +- If the interface requirement has a `where` clause, there are + [concerns](#less-strict-about-requirements-with-where-clauses) about being + able to locally check whether impls satisfy that requirement. +- A function trying to make use of the fact that a type implements an + interface due to an interface requirement, or a blanket impl, may require + the compiler perform a search that we don't know will be bounded. ## Background -TODO: Is there any background that readers should consider to fully understand -this problem and your approach to solving it? +The first version of interface-implemented requirements for interfaces was +introduced in proposal +[#553: Generics details part 1](https://github.com/carbon-language/carbon-lang/pull/553). ## Proposal -- Requiring another type to implement an interface - ``` - interface IntLike { - impl i32 as As(Self); - } - interface CommonTypeWith(T:! Type) { - impl T as CommonTypeWith(Self); - } - ``` -- Difficulty of `where` clauses. -- Observe declarations for saying types implement interfaces, and not just for - interface-interface dependencies, but also blanket impls +This proposal adds two sections to the +[generics details design document](/docs/design/generics/details.md): -TODO: Briefly and at a high level, how do you propose to solve the problem? Why -will that in fact solve it? - -## Details - -TODO: Fully explain the details of the proposed solution. +- [Interface requiring other interfaces revisited](/docs/design/generics/details.md#interface-requiring-other-interfaces-revisited) +- [Observing a type implements an interface](/docs/design/generics/details.md#observing-a-type-implements-an-interface) ## Rationale based on Carbon's goals -TODO: How does this proposal effectively advance Carbon's goals? Rather than -re-stating the full motivation, this should connect that motivation back to -Carbon's stated goals for the project or language. This may evolve during -review. Use links to appropriate goals, for example: - -- [Community and culture](/docs/project/goals.md#community-and-culture) -- [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem) -- [Performance-critical software](/docs/project/goals.md#performance-critical-software) -- [Software and language evolution](/docs/project/goals.md#software-and-language-evolution) -- [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write) -- [Practical safety and testing mechanisms](/docs/project/goals.md#practical-safety-and-testing-mechanisms) -- [Fast and scalable development](/docs/project/goals.md#fast-and-scalable-development) -- [Modern OS platforms, hardware architectures, and environments](/docs/project/goals.md#modern-os-platforms-hardware-architectures-and-environments) -- [Interoperability with and migration from existing C++ code](/docs/project/goals.md#interoperability-with-and-migration-from-existing-c-code) +This proposal advances these goals of Carbon: -## Alternatives considered +- [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem): + The motivation for this expressive power of interface requirements comes + from discussions about how to achieve symmetric behavior with interfaces + like `CommonTypeWith` from + [proposal #911: Conditional expressions](https://github.com/carbon-language/carbon-lang/pull/911). +- [Fast and scalable development](/docs/project/goals.md#fast-and-scalable-development): + The requirement that the source provide the proof of any facts that would + require a recursive search using `observe` declarations means that the + expense of that search is avoided except in the case where there is a + compiler error. If the search is successful, the results of the search can + be copied into the source, and afterward the search need not be repeated. -TODO: What alternative solutions have you considered? +## Alternatives considered ### Less strict about requirements with `where` clauses From a0006c4a9a73052646752f9df2f607dd3c8a335a Mon Sep 17 00:00:00 2001 From: Josh L Date: Mon, 11 Apr 2022 18:45:01 +0000 Subject: [PATCH 11/20] Fix pre-commit --- executable_semantics/syntax/parser.ypp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/executable_semantics/syntax/parser.ypp b/executable_semantics/syntax/parser.ypp index 68af5085cf51d..c0a6c8d51d84e 100644 --- a/executable_semantics/syntax/parser.ypp +++ b/executable_semantics/syntax/parser.ypp @@ -903,9 +903,9 @@ declaration: } | INTERFACE identifier LEFT_CURLY_BRACE declaration_list RIGHT_CURLY_BRACE { - auto ty_ty = arena->New(context.source_loc()); + auto ty_ty = arena -> New(context.source_loc()); auto self = - arena->New(context.source_loc(), "Self", ty_ty); + arena -> New(context.source_loc(), "Self", ty_ty); $$ = arena->New(context.source_loc(), $2, self, $4); } | impl_kind IMPL expression AS expression LEFT_CURLY_BRACE declaration_list RIGHT_CURLY_BRACE From dc2fb2421b7061bbf8e8297263fdf54278d6ffe4 Mon Sep 17 00:00:00 2001 From: Josh L Date: Mon, 18 Apr 2022 23:20:15 +0000 Subject: [PATCH 12/20] Link now that #1084 merged --- docs/design/generics/details.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 7166a707d8cc5..36e81da86fe55 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4837,11 +4837,8 @@ When implementing an interface with an `impl as` requirement, that requirement must be satisfied either by an implementation in an imported library or an implementation somewhere in the same file. Implementing the requiring interface is a promise that the requirement will be implemented. This is like a - - - -forward declaration of an impl except that the definition can be broader instead -of being required to match exactly. +[forward declaration of an impl](#declaring-implementations) except that the +definition can be broader instead of being required to match exactly. ``` external impl Vector(i32) as Iterable { ... } From 620118954008b70f5d83d02441c926b2dc8d5b0c Mon Sep 17 00:00:00 2001 From: josh11b Date: Wed, 27 Apr 2022 14:25:31 -0700 Subject: [PATCH 13/20] Apply suggestions from code review Co-authored-by: Richard Smith --- docs/design/generics/details.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 36e81da86fe55..b9ba0fa1482ac 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4851,7 +4851,7 @@ fn ProcessVector(v: Vector(i32)) { } // Satisfies requirement that `Vector(i32)` must -// implement `Iterable` since `i32` is `Equatable`. +// implement `Equatable` since `i32` is `Equatable`. external impl Vector(T:! Equatable) as Equatable { ... } ``` @@ -4892,8 +4892,8 @@ different assignment. An [`observe` declaration](#observe-declarations) can be used to show that two types are equal so code can pass type checking without explicitly writing casts, without requiring the compiler to do a unbounded search that may not terminate. -The compiler may need another form of `observe` declaration to see that a type -implements an interface. +An `observe` declaration can also be used to show that a type implements an +interface, in cases where the compiler will not work this out for itself. ### Observing interface requirements From 7716e37787ea61752265f05cc0bcad8f2d9741c0 Mon Sep 17 00:00:00 2001 From: Josh L Date: Wed, 27 Apr 2022 21:28:03 +0000 Subject: [PATCH 14/20] Remove merge conflict marker --- docs/design/generics/details.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index b9ba0fa1482ac..bdb0f013bb51b 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -5325,8 +5325,6 @@ external impl [T:! IntLike] like T as MultipliableWith(like T) where .Result = T; ``` -> > > > > > > upstream/trunk - ## Future work ### Dynamic types From 46b634ed0123564f5682c52b51c7ae944bea90b8 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Apr 2022 21:32:03 +0000 Subject: [PATCH 15/20] `observe` only used during type checking --- docs/design/generics/details.md | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index bdb0f013bb51b..ea1e6f42edcc3 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4899,12 +4899,13 @@ interface, in cases where the compiler will not work this out for itself. One situation where this occurs is when there is a chain of [interfaces requiring other interfaces](#interface-requiring-other-interfaces-revisited). -Normally, Carbon will only consider the interfaces that are direct requirements -of the interfaces the type is known to implement. An `observe...is` declaration -can be used to add an interface that is a direct requirement to the set of -interfaces whose direct requirements will be considered for that type. This -allows a developer to provide a proof that there is a sequence of requirements -that demonstrate that a type implements an interface, as in this example: +During the 'impl' validation done during type checking, Carbon will only +consider the interfaces that are direct requirements of the interfaces the type +is known to implement. An `observe...is` declaration can be used to add an +interface that is a direct requirement to the set of interfaces whose direct +requirements will be considered for that type. This allows a developer to +provide a proof that there is a sequence of requirements that demonstrate that a +type implements an interface, as in this example: ``` interface A { } @@ -4935,6 +4936,12 @@ fn RequiresD[T:! D](x: T) { } ``` +Note that `observe` statements do not affect the selection of impls during code +generation. For coherence, the impl used for a type, interface pair must always +be the same, independent of context. The [termination rule](#termination-rule) +governs when compilation may fail when the compiler can't determine the impl to +select. + ### Observing blanket impls An `observe...is` declaration can also be used to observe that a type implements From e5670428a699ea726f94072f571066ac8b0f61d4 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Apr 2022 21:40:19 +0000 Subject: [PATCH 16/20] More comments in example --- docs/design/generics/details.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index ea1e6f42edcc3..4e47d9a2a1556 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4841,6 +4841,8 @@ is a promise that the requirement will be implemented. This is like a definition can be broader instead of being required to match exactly. ``` +// `Iterable` requires `Equatable`, so there must be some +// impl of `Equatable` for `Vector(i32)` in this file. external impl Vector(i32) as Iterable { ... } fn RequiresEquatable[T:! Equatable](x: T) { ... } @@ -4850,7 +4852,7 @@ fn ProcessVector(v: Vector(i32)) { RequiresEquatable(v); } -// Satisfies requirement that `Vector(i32)` must +// Satisfies the requirement that `Vector(i32)` must // implement `Equatable` since `i32` is `Equatable`. external impl Vector(T:! Equatable) as Equatable { ... } ``` From a5de77933ffce78ec9b1a9a5ddadc2316033f09b Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Apr 2022 21:52:59 +0000 Subject: [PATCH 17/20] Allow interface requirements to be satisfied by impl constraints --- docs/design/generics/details.md | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 4e47d9a2a1556..47a284695dc8b 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4834,9 +4834,10 @@ interface Iterable { ``` When implementing an interface with an `impl as` requirement, that requirement -must be satisfied either by an implementation in an imported library or an -implementation somewhere in the same file. Implementing the requiring interface -is a promise that the requirement will be implemented. This is like a +must be satisfied by an implementation in an imported library, an implementation +somewhere in the same file, or a constraint in the impl declaration. +Implementing the requiring interface is a promise that the requirement will be +implemented. This is like a [forward declaration of an impl](#declaring-implementations) except that the definition can be broader instead of being required to match exactly. @@ -4864,6 +4865,25 @@ implementation itself, as in: impl [T:! Type] T as CommonTypeWith(T) { ... } ``` +Here is an example where the requirement of interface `Iterable` that the type +implements interface `Equatable` is satisfied by a constraint in the `impl` +declaration: + +``` +class Foo(T:! Type) {} +// This is allowed because we know that an `impl Foo(T) as Equatable` +// will exist for all types `T` for which this impl is used, even +// though there's neither an imported impl nor an impl in this file. +external impl Foo(T:! Type where Foo(T) is Equatable) as Iterable {} +``` + +``` +class Bar {} +external impl Foo(Bar) as Equatable {} +// Gives `Foo(Bar) is Iterable` using the blanket impl of +// `Iterable` for `Foo(T)`. +``` + ### Requirements with `where` constraints An interface implementation requirement with a `where` clause is harder to From 8bdb39d76953abc4155dc75ddc16a616cac41fbd Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 28 Apr 2022 21:55:32 +0000 Subject: [PATCH 18/20] Connecting text --- docs/design/generics/details.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 47a284695dc8b..8692821d57d5b 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4877,6 +4877,9 @@ class Foo(T:! Type) {} external impl Foo(T:! Type where Foo(T) is Equatable) as Iterable {} ``` +This might be used to provide an implementation of `Equatable` for types that +already satisfy the requirement of implementing `Iterable`: + ``` class Bar {} external impl Foo(Bar) as Equatable {} From 929a80edefec5607d17a3a7b010e30380e9d24fd Mon Sep 17 00:00:00 2001 From: josh11b Date: Thu, 5 May 2022 15:21:03 -0700 Subject: [PATCH 19/20] Apply suggestions from code review Co-authored-by: Richard Smith --- docs/design/generics/details.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 0a6fdb4035724..ee472a59a2906 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4956,7 +4956,7 @@ interface, in cases where the compiler will not work this out for itself. One situation where this occurs is when there is a chain of [interfaces requiring other interfaces](#interface-requiring-other-interfaces-revisited). -During the 'impl' validation done during type checking, Carbon will only +During the `impl` validation done during type checking, Carbon will only consider the interfaces that are direct requirements of the interfaces the type is known to implement. An `observe...is` declaration can be used to add an interface that is a direct requirement to the set of interfaces whose direct @@ -4994,7 +4994,7 @@ fn RequiresD[T:! D](x: T) { ``` Note that `observe` statements do not affect the selection of impls during code -generation. For coherence, the impl used for a type, interface pair must always +generation. For coherence, the impl used for a (type, interface) pair must always be the same, independent of context. The [termination rule](#termination-rule) governs when compilation may fail when the compiler can't determine the impl to select. From 41d5e66f45914be5484e842a24bd791f748c8fc2 Mon Sep 17 00:00:00 2001 From: Josh L Date: Thu, 5 May 2022 22:21:47 +0000 Subject: [PATCH 20/20] Fix formatting --- docs/design/generics/details.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index ee472a59a2906..334d5faeddf71 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -4994,10 +4994,10 @@ fn RequiresD[T:! D](x: T) { ``` Note that `observe` statements do not affect the selection of impls during code -generation. For coherence, the impl used for a (type, interface) pair must always -be the same, independent of context. The [termination rule](#termination-rule) -governs when compilation may fail when the compiler can't determine the impl to -select. +generation. For coherence, the impl used for a (type, interface) pair must +always be the same, independent of context. The +[termination rule](#termination-rule) governs when compilation may fail when the +compiler can't determine the impl to select. ### Observing blanket impls