You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
GSB: New algorithm for identifying redundant requirements
Generic signature minimization needs to diagnose and remove any
redundant requirements, that is, requirements that can be proven
from some subset of the remaining requirements.
For each requirement on an equivalence class, we record a set of
RequirementSources; a RequirementSource is a "proof" that the
equivalence class satisfies the requirement.
A RequirementSource is either "explicit" -- meaning it
corresponds to a generic requirement written by the user -- or it
is "derived", meaning it can be proven from some other explicit
requirement.
The most naive formulation of the minimization problem is that
we say that an explicit requirement is redundant if there is a
derived source for the same requirement. However, this is not
sufficient, for example:
protocol P {
associatedtype A : P where A.A == Self
}
In the signature <T where T : P>, the explicit requirement
T : P also has a derived source T.A.A : P. However, this source
is "self-derived", meaning that in order to obtain the
witness table for T.A.A : P, we first have to obtain the witness
table for T.A.
The GenericSignatureBuilder handled this kind of 'self-derived'
requirement correctly, by removing it from the list of sources.
This was implemented in the removeSelfDerived() function.
After removeSelfDerived() was called, any remaining derived
requirement sources were assumed to obsolete any explicit
source for the same requirement.
However, even this was not sufficient -- namely, it only handled
the case where a explicit requirement would imply a derived
source for itself, and not a cycle involving multiple explicit
sources that would imply each other.
For example, the following generic signature would be misdiagnosed
with *both* conformance requirements as redundant, resulting in
an invalid generic signature:
protocol P {
associatedtype T : P
}
func f<T : P, U : P>(_: T, _: U) where T.X == U, U.X == T {}
In the above example, T : P has an explicit requirement source,
as well as a derived source (U : P)(U.X : P). Similarly, U : P
has an explicit requirement source, as well as a derived source
(T : P)(T.X : P). Since neither of the derived sources were
"self-derived" according to our definition, we would diagnose
*both* explicit sources as redundant. But of course, after
dropping them, we are left with the following generic signature:
func f<T, U>(_: T, _: U) where T.X == U, U.X == T {}
This is no longer valid -- since neither T nor U have a conformance
requirement, the nested types T.X and U.X referenced from our
same-type requirements are no longer valid.
The new algorithm abandons the "self-derived" concept. Instead,
we build a directed graph where the vertices are explicit
requirements, and the edges are implications where one explicit
requirement implies another. In the above example, each of the
explicit conformance requirements implies the other. This means
a correct minimization must pick exactly one of the two -- not
zero, and not both.
The set of minimized requirements is formally defined as the
minimum set of requirements whose transitive closure is the
entire graph.
We compute this set by first building the graph of strongly
connected components using Tarjan's algorithm. The graph of SCCs
is a directed acyclic graph, which means we can compute the root
set of the DAG. Finally, we pick a suitable representative
requirement from each SCC in the root set, using the lexshort
order on subject types.
This commit implements the new algorithm, runs it on each generic
signature and asserts some properties about the results, but
doesn't actually use the algorithm for computing the minimized
signature or diagnosing redundancies; that will come in the next
commit.
0 commit comments