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
This kind of data structure first appeared in the early history of compilers in the implementation of ``\texttt{EQUIV} statements'' for declaring that two symbols ought to share a storage location. These statements thus define an equivalence relation on symbols, and the performance gains from a careful implementation were noted in~\cite{improvedequivalence}. A survey of later techniques appears in~\cite{unionfindsurvey}.
680
680
681
681
\paragraph{Lazy expansion.}
682
-
From a theoretical point of view, the archetype builder's approach amounts to exhausive enumeration of all \index{derived requiremen!enumerationt}derived requirements and \index{valid type parameter!enumeration}valid type parameters of a generic signature, made slightly more efficient by the choice of data structure (the asymmetry in the handling of member types in \AlgRef{archetypebuildermerge} means we skip parts of the search space that would yield nothing new).
682
+
From a theoretical point of view, the archetype builder's approach amounts to exhaustive enumeration of all \index{derived requirement!enumeration}derived requirements and \index{valid type parameter!enumeration}valid type parameters of a generic signature, made slightly more efficient by the choice of data structure (the asymmetry in the handling of member types in \AlgRef{archetypebuildermerge} means we skip parts of the search space that would yield nothing new).
683
683
684
684
The eager expansion model survived the introduction of protocol \texttt{where} clauses in Swift~4 \cite{se0142}, and thus associated requirements, with only relatively minor changes. The introduction of recursive conformances in Swift~4.1~\cite{se0157} necessitated a larger overhaul. Once the type parameter graph becomes infinite, the eager conformance requirement expansion of \AlgRef{archetypebuilderexpand} no longer makes sense. The \texttt{ArchetypeBuilder} was renamed to the \IndexDefinition{GenericSignatureBuilder@\texttt{GenericSignatureBuilder}}\texttt{GenericSignatureBuilder} as part of a re-design where the recursive expansion was now performed as needed, within the lookup of \AlgRef{archetypebuilderlookup} itself \cite{implrecursive}.
We now state the general result. We need this for the proof of \ThmRef{validtheorem}, and also later in \SecRef{conformancepathsexist}, when we show that every derived conformance requirement has a derivation of a certrain form.
771
+
We now state the general result. We need this for the proof of \ThmRef{validtheorem}, and also later in \SecRef{conformancepathsexist}, when we show that every derived conformance requirement has a derivation of a certain form.
Let $G$ be an arbitrary generic signature. Suppose that $G\vdash\tT$ and $G\vdash\TP$ for some type parameter \tT\ and protocol \tP. Then if we take a valid type parameter or derived requirement of~$\GP$ and replace \tSelf\ with \tT\ throughout, we get a valid type parameter or derived requirement of~$G$, just rooted in \tT. That is:
Let $G$ be a \index{well-formed generic signature}well-formed generic signature. If $G$ has a pair of \index{derived requirement!conflicts}derived requirements $R_1$~and~$R_2$ where $R_1\otimes\Sigma$ and $R_2\otimes\Sigma$ cannot both be \index{satisfied requirement!conflicts}satisfied by the same substitution map~$\Sigma$, then $R_1$~and~$R_2$ define a pair of \IndexDefinition{conflicting requirement}\emph{confliciting requirements}. A generic signature $G$ is \emph{conflict-free} if it does not have any pairs of conflicting requirements. The pairs of derived requirements that can lead to conflicts are enumerated below:
1315
+
Let $G$ be a \index{well-formed generic signature}well-formed generic signature. If $G$ has a pair of \index{derived requirement!conflicts}derived requirements $R_1$~and~$R_2$ where $R_1\otimes\Sigma$ and $R_2\otimes\Sigma$ cannot both be \index{satisfied requirement!conflicts}satisfied by the same substitution map~$\Sigma$, then $R_1$~and~$R_2$ define a pair of \IndexDefinition{conflicting requirement}\emph{conflicting requirements}. A generic signature $G$ is \emph{conflict-free} if it does not have any pairs of conflicting requirements. The pairs of derived requirements that can lead to conflicts are enumerated below:
1316
1316
\begin{enumerate}
1317
1317
\item For two concrete \index{same-type requirement!conflicts}same-type requirements $\SameReq{T}{$\tX_1$}$ and $\SameReq{T}{$\tX_2$}$, we desugar the ``combined'' requirement $\SameReq{$\tX_1$}{$\tX_2$}$, as we already saw. Here and every remaining case below, desugaring will either detect a conflict, or produce a simpler list of requirements that can replace one of the two original requirements.
1318
1318
\item For a concrete same-type requirement $\TX$ and superclass requirement $\TC$, we desugar $\ConfReq{X}{C}$, which can be satisfied only if~\tX\ is a class type that is also a subclass of~\tC.
We can now describe the main loop of the Knuth-Bendix completion procedure, which repeatedly finds and resolves critical pairs until no more non-trivial critical pairs remain. This process might not terminate, and we might find ourselves discovering new critical pairs and adding new rules to resolve them, forever. To prevent an infinite loop in the case of failure, we implement a termination check; if we think we've done too much work already, we give up on constructing a covergent rewriting system. We already mentioned the \textbf{left-simplified}, \textbf{right-simplified}, and \textbf{substitution-simplified} flags a few times; they are set by the rule simplification passes, with the first two described in \SecRef{rulereduction} and the third one in \SecRef{substsimplification}. These passes are invoked at appropriate times in the main loop below.
390
+
We can now describe the main loop of the Knuth-Bendix completion procedure, which repeatedly finds and resolves critical pairs until no more non-trivial critical pairs remain. This process might not terminate, and we might find ourselves discovering new critical pairs and adding new rules to resolve them, forever. To prevent an infinite loop in the case of failure, we implement a termination check; if we think we've done too much work already, we give up on constructing a convergent rewriting system. We already mentioned the \textbf{left-simplified}, \textbf{right-simplified}, and \textbf{substitution-simplified} flags a few times; they are set by the rule simplification passes, with the first two described in \SecRef{rulereduction} and the third one in \SecRef{substsimplification}. These passes are invoked at appropriate times in the main loop below.
391
391
392
392
\begin{algorithm}[Knuth-Bendix completion procedure]\label{knuthbendix} Takes a list of rewrite rules as input. Records new rewrite rules, as well as rewrite loops, and returns success or failure. On success, the rewrite rules define a convergent rewriting system. Failure indicates we got a non-orientable rewrite rule, or we triggered the termination check.
If the identity conformance rule had not been part of that initial set, this last critical pair would \emph{define} the identity conformance rule, and we would obtain the same rewrite system in the end. We don't need to explicitly add the identity conformance rule, after all. There is a practical consideration though. By making this rule part of the initial set, and cruicially, marking it \index{permanent rule}\textbf{permanent}, we remove it from consideration in the rewrite system minimization algorithm. This cuts out a lot of unnecessary work.
1236
+
If the identity conformance rule had not been part of that initial set, this last critical pair would \emph{define} the identity conformance rule, and we would obtain the same rewrite system in the end. We don't need to explicitly add the identity conformance rule, after all. There is a practical consideration though. By making this rule part of the initial set, and crucially, marking it \index{permanent rule}\textbf{permanent}, we remove it from consideration in the rewrite system minimization algorithm. This cuts out a lot of unnecessary work.
\ListingRef{rewritesystemq} shows the convegent rewrite system for \tQ, which imports rules from protocol~\texttt{N}. Completion discovers the following critical pairs; we will be content to just summarize because they are similar to previous examples:
1526
+
\ListingRef{rewritesystemq} shows the convergent rewrite system for \tQ, which imports rules from protocol~\texttt{N}. Completion discovers the following critical pairs; we will be content to just summarize because they are similar to previous examples:
1527
1527
\begin{itemize}
1528
1528
\item Rule (6) overlaps with (7) on $\pQ\cdot\pQ\cdot\nA$. We define rule (\CRule{10}) (this general principle was established in \ExRef{protoassocrule}).
1529
1529
\item Rule (8) overlaps with (2) on $\pQ\cdot\protosym{N}\cdot\nA$. We define rule (\CRule{11}) (\ExRef{protocolinheritancecompletionexample}).
However, we wish to recover $\SubstringSequence$ from $\Sigma$ alone, without resorting to a \index{global conformance lookup}\emph{global} conformance lookup, as we did in the above calculation. We don't have a lot of options. In fact, pretty much the \emph{only} thing local confomance lookup can do is take one of the \index{root conformance}root conformances stored in the substitution map, and proceed to apply \index{associated conformance projection}associated conformance projection operations.
146
+
However, we wish to recover $\SubstringSequence$ from $\Sigma$ alone, without resorting to a \index{global conformance lookup}\emph{global} conformance lookup, as we did in the above calculation. We don't have a lot of options. In fact, pretty much the \emph{only} thing local conformance lookup can do is take one of the \index{root conformance}root conformances stored in the substitution map, and proceed to apply \index{associated conformance projection}associated conformance projection operations.
147
147
148
148
Our generic signature $G$ only has one explicit conformance requirement, so we start with the lone root conformance of $\Sigma$:
We denote this inherited conformance by $\ConfReq{Square}{Shape}$. It behaves identically to the superclass conformance $\ConfReq{Polygon}{Shape}$, except if ask for its \index{conforming type!inherited conformance}conforming type, we get back \texttt{Square} instead of \texttt{Polygon}. In \ExRef{inheritedspecializedconf}, we will see that more complex behavors can manifest when the superclass declaration has generic parameters.
67
+
We denote this inherited conformance by $\ConfReq{Square}{Shape}$. It behaves identically to the superclass conformance $\ConfReq{Polygon}{Shape}$, except if ask for its \index{conforming type!inherited conformance}conforming type, we get back \texttt{Square} instead of \texttt{Polygon}. In \ExRef{inheritedspecializedconf}, we will see that more complex behaviors can manifest when the superclass declaration has generic parameters.
Associated type inference \index{synthesized declaration}synthesizes a type alias member for each inferred associated type, so we can refer to \texttt{Cat.Toy} elsewhere in the program, as if we explictly declared the type alias \texttt{Toy} as a member of \texttt{Cat}. Now, consider \texttt{Dog}, which witnesses \texttt{Pet}'s associated type with a generic parameter named \texttt{Toy}. This is Case~3:
323
+
Associated type inference \index{synthesized declaration}synthesizes a type alias member for each inferred associated type, so we can refer to \texttt{Cat.Toy} elsewhere in the program, as if we explicitly declared the type alias \texttt{Toy} as a member of \texttt{Cat}. Now, consider \texttt{Dog}, which witnesses \texttt{Pet}'s associated type with a generic parameter named \texttt{Toy}. This is Case~3:
0 commit comments