Generic details 10: interface-implemented requirements
Table of contents
Problem
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 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
The first version of interface-implemented requirements for interfaces was introduced in proposal #553: Generics details part 1.
Proposal
This proposal adds two sections to the generics details design document:
Rationale based on Carbon’s goals
This proposal advances these goals of Carbon:
- 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. - 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.
Alternatives considered
Less strict about requirements with where
clauses
We could allow 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
andB
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
.
This problem was discussed in the #generics channel on Discord.
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. Note: it is possible that the 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.