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
\item If a conformance requirement is made redundant by a same-type requirement that fixes a type parameter to a concrete type (such as $\SameReq{T}{S}$ and $\ConfReq{T}{P}$ where \texttt{S} is a concrete type and $\ConfReq{S}{P}$ is a concrete conformance), the rewrite system cannot be reused for technical reasons; we will talk about this in \ChapRef{concreteconformances}.
137
137
\end{enumerate}
138
138
139
-
The first three only occur with invalid code, and are accompanied by diagnostics. The fourth is not an error, just a rare edge case where our optimization cannot be performed. All conditions are checked for during minimization, and recorded in the form of a flags field. We cannot install the minimization machine if any of these flags are set; doing so would associate a generic signature with a minimization machine that contains rewrite rules not explained by the generic signature itself. This would confuse subsequent generic signature queries. In the event that the above does not cover some other unforseen scenario where equivalence fails to hold, the \IndexFlag{disable-requirement-machine-reuse}\texttt{-disable-requirement-machine-reuse} frontend flag forces minimization machines to be discarded immediately after use, instead of being installed.
139
+
The first three only occur with invalid code, and are accompanied by diagnostics. The fourth is not an error, just a rare edge case where our optimization cannot be performed. All conditions are checked for during minimization, and recorded in the form of a flags field. We cannot install the minimization machine if any of these flags are set; doing so would associate a generic signature with a minimization machine that contains rewrite rules not explained by the generic signature itself. This would confuse subsequent generic signature queries. In the event that the above does not cover some other unforeseen scenario where equivalence fails to hold, the \IndexFlag{disable-requirement-machine-reuse}\texttt{-disable-requirement-machine-reuse} frontend flag forces minimization machines to be discarded immediately after use, instead of being installed.
140
140
141
141
\begin{example}
142
142
The compiler builds several requirement machines while type checking the code below:
Note that this was an overlap of the first kind, so rule (7) is now marked \index{left-simplified rule}\textbf{left-simplified}. Thus, rule (*8) completely supercedes rule (7). Rule (*8) survives minimization and maps to the requirement $\ConfReq{\ttgp{0}{0}.[P]A.[Q]B}{R}$, which appears in the generic signature that we output for this protocol extension:
745
+
Note that this was an overlap of the first kind, so rule (7) is now marked \index{left-simplified rule}\textbf{left-simplified}. Thus, rule (*8) completely supersedes rule (7). Rule (*8) survives minimization and maps to the requirement $\ConfReq{\ttgp{0}{0}.[P]A.[Q]B}{R}$, which appears in the generic signature that we output for this protocol extension:
We see that applying $\Sigma_{\ConfReq{X}{S}}$ to \texttt{\ttgp{0}{0}.[S]A} and \texttt{\ttgp{0}{0}.[S]C.[S]B} also outputs identical types: $\AssocType{[S]A}\otimes\ConfReq{X}{S}=\AssocType{[S]B}\otimes\ConfReq{Y}{S}=\texttt{Int}$. Is this the case for \emph{every} conformance to \texttt{S}? That is, is it true that $G_\texttt{S}\vDash\SameReq{\texttt{\ttgp{0}{0}.A}}{\texttt{\ttgp{0}{0}.C.B}}$?
1077
1077
1078
-
We will see the answer is ``yes,'' proving that our function \texttt{f()} type checks. For a visual perspective, we turn to the \index{type parameter graph}type parameter graph\footnote{In our previous formulation, the type parameter graph has a distinguished root node, with every generic parameter as a child of this root. Now, our generic signature only has one generic parameter, so a root node would be superflous; we omit it in what follows.} for $G_\texttt{S}$. \FigRef{protocolsfig} constructs this graph in three steps. Between each step, we have a \index{graph homomorphism}graph homomorphism---in fact, a \index{covering map}covering map, in the sense of \SecRef{protocolcomponent}---transforming one graph into the other:
1078
+
We will see the answer is ``yes,'' proving that our function \texttt{f()} type checks. For a visual perspective, we turn to the \index{type parameter graph}type parameter graph\footnote{In our previous formulation, the type parameter graph has a distinguished root node, with every generic parameter as a child of this root. Now, our generic signature only has one generic parameter, so a root node would be superfluous; we omit it in what follows.} for $G_\texttt{S}$. \FigRef{protocolsfig} constructs this graph in three steps. Between each step, we have a \index{graph homomorphism}graph homomorphism---in fact, a \index{covering map}covering map, in the sense of \SecRef{protocolcomponent}---transforming one graph into the other:
1079
1079
\begin{enumerate}
1080
1080
\item The first step shows the graph as it would be without the protocol stating any same-type requirements; we get an infinite tree where each interior node is the parent of one other interior node, and two leaf nodes.
Completion suceeds on $M_3$ using a reduction order where $c<b<a$ and $p<n$, and we get a finite convergent rewrite system. We've already listed the numerous rules once, so we won't do it again. Let's call this finite convergent presentation $M_2^\prime$:
1684
+
Completion succeeds on $M_3$ using a reduction order where $c<b<a$ and $p<n$, and we get a finite convergent rewrite system. We've already listed the numerous rules once, so we won't do it again. Let's call this finite convergent presentation $M_2^\prime$:
For $(1)\Rightarrow(2)$, note that the set of generic parameter types is always finite, so it suffices to only consider reduced \index{dependent member type}dependent member types. Suppose we're given an infinite set of reduced dependent member types; we must produce an infinite set of abstract conformances. Each dependent member type \texttt{T.[P]A} is equivalent to an ordered pair consisting of a type witness projection $\AssocType{[P]A}$ and an abstract conformance $\ConfReq{T}{P}$; the first element of the pair is drawn from a finite set, so a counting argument shows that the mapping that takes the second element of each pair must give us an infinite set of abstract conformances.
568
568
569
-
Furthermore, these abstract conformances must be reduced, meaning their subject types are reduced. To see why, note that whenever \texttt{T.[P]A} is a reduced dependent member type, its base type \texttt{T} must be reduced as well (otherwise, if $G\vDash\SameReq{$\texttt{T}^\prime$}{T}$ with $\texttt{T}^\prime<\texttt{T}$, we could construct from this a derivation of $\SameReq{$\texttt{T}^\prime$.[P]A}{T.[P]A}$ with $\texttt{$\texttt{T}^\prime$.[P]A} < \texttt{T.[P]A}$, contradicting the asumption that \texttt{T.[P]A} is reduced).
569
+
Furthermore, these abstract conformances must be reduced, meaning their subject types are reduced. To see why, note that whenever \texttt{T.[P]A} is a reduced dependent member type, its base type \texttt{T} must be reduced as well (otherwise, if $G\vDash\SameReq{$\texttt{T}^\prime$}{T}$ with $\texttt{T}^\prime<\texttt{T}$, we could construct from this a derivation of $\SameReq{$\texttt{T}^\prime$.[P]A}{T.[P]A}$ with $\texttt{$\texttt{T}^\prime$.[P]A} < \texttt{T.[P]A}$, contradicting the assumption that \texttt{T.[P]A} is reduced).
570
570
571
571
A similar argument establishes $(2)\Rightarrow(1)$. We're given an infinite set of reduced abstract conformances, and we must produce an infinite set of reduced type parameters. Each abstract conformance $\ConfReq{T}{P}$ uniquely determines an ordered pair, consisting of a \index{protocol declaration}protocol declaration $\protosym{P}$ and a type parameter \texttt{T}. The set of protocol declarations is finite, so again, taking the second element of each pair gives us an infinite set of reduced type parameters.
An unqualified reference to a member of an outer nominal type can only be made if the member is static, because there is no ``outer \texttt{self} value'' to invoke the method with; a \emph{value} of the nested type does not contain a \emph{value} of its parent type.
570
570
571
-
For the same reason, methods inside \index{local type declaration}local types cannot refer to local variables declared outside of the local type. (Constrast this with \index{Java}Java inner classes for example, which can be declared as \texttt{static} or instance members of their outer class; a non-\texttt{static} inner class captures a ``\texttt{this}'' reference from the outer class. Inner classes nested in methods can also capture local variables in Java.)
571
+
For the same reason, methods inside \index{local type declaration}local types cannot refer to local variables declared outside of the local type. (Contrast this with \index{Java}Java inner classes for example, which can be declared as \texttt{static} or instance members of their outer class; a non-\texttt{static} inner class captures a ``\texttt{this}'' reference from the outer class. Inner classes nested in methods can also capture local variables in Java.)
572
572
573
573
\paragraph{Constructor declarations.}
574
574
\IndexDefinition{constructor declaration}Constructor declarations are introduced with the \texttt{init} keyword. The parent context of a constructor must be a nominal type or extension.
\item\texttt{isGenericContext()} answers true if either this generic context or one of its parents has a generic parameter list.
1032
1032
\item\texttt{isInnermostContextGeneric()} answers if this declaration context itself has a generic parameter list. Compare with \texttt{isGenericContext()}.
Every nominal type declaration has an associated \IndexDefinition{member lookup table}\emph{member lookup table}, which is used for direct lookup. This table maps each identifier to a list of value declarations with that name (multiple value declarations can share a name because Swift allows type-based overloading). The declarations in a member lookup table are understood to be members of one or more iterable declaration contexts, which are exactly the type declaration itself and all of its extensions. These iterable declaration contexts might originate from a mix of different module kinds. For example, the nominal type itself might be an \index{Objective-C}Objective-C class from an imported Objective-C module, with one extension declared in a binary Swift module, and another extension defined in the main module, parsed from source.
253
253
254
-
The lookup table is populated lazily, in a manner resembling a state machine. Say we're asked to perform a direct lookup for some given name. If this is the first direct lookup, we populate the member lookup table with \emph{all} members from any \emph{parsed} iterable declaration contexts, which might trigger delayed parsing. Each entry in the member lookup table stores a ``complete'' bit. The ``complete'' bit of these initially-populated entries is \emph{not} set, meaning that the entry only contains those members that were parsed from source. If any iterable declaration contexts originate from binary and imported modules, direct lookup then asks each lazy member loader to selectively load only those members with the given name. (Parsed declaration contexts do not offer this level of lazyness, because there is no way to parse a subset of the members only.) After the lazy member loaders do their work, the lookup table entry for this name is now complete, and the ``complete'' bit is set. Later when direct lookup finds a member lookup table entry with the ``complete'' bit set, it knows this entry is fully populated, and the stored list of declarations is returned immediately without querying the lazy member loaders.
254
+
The lookup table is populated lazily, in a manner resembling a state machine. Say we're asked to perform a direct lookup for some given name. If this is the first direct lookup, we populate the member lookup table with \emph{all} members from any \emph{parsed} iterable declaration contexts, which might trigger delayed parsing. Each entry in the member lookup table stores a ``complete'' bit. The ``complete'' bit of these initially-populated entries is \emph{not} set, meaning that the entry only contains those members that were parsed from source. If any iterable declaration contexts originate from binary and imported modules, direct lookup then asks each lazy member loader to selectively load only those members with the given name. (Parsed declaration contexts do not offer this level of laziness, because there is no way to parse a subset of the members only.) After the lazy member loaders do their work, the lookup table entry for this name is now complete, and the ``complete'' bit is set. Later when direct lookup finds a member lookup table entry with the ``complete'' bit set, it knows this entry is fully populated, and the stored list of declarations is returned immediately without querying the lazy member loaders.
255
255
256
256
This \emph{lazy member loading} mechanism ensures that only those members which are actually referenced in a compilation session are loaded from serialized and imported iterable declaration contexts.
The \texttt{CanGenericSignature} class wraps a \texttt{GenericSignatureImpl *} pointer which is known to be canonical. The pointer can be recovered with the \texttt{getPointer()} method. There is an implicit conversion from \texttt{CanGenenericSiganture} to \texttt{GenericSignature}. The \texttt{operator->} forwards method calls to the underlying \texttt{GenericSignatureImpl}.
1380
+
The \texttt{CanGenericSignature} class wraps a \texttt{GenericSignatureImpl *} pointer which is known to be canonical. The pointer can be recovered with the \texttt{getPointer()} method. There is an implicit conversion from \texttt{CanGenericSignature} to \texttt{GenericSignature}. The \texttt{operator->} forwards method calls to the underlying \texttt{GenericSignatureImpl}.
1381
1381
1382
1382
The \texttt{operator==} and \texttt{operator!=} operators are used to test \texttt{CanGenericSignature} for pointer equality. The \texttt{isEqual()} method of \texttt{GenericSignatureImpl} implements canonical equality on arbitrary generic signatures by first canonicalizing both sides, then checking the resulting canonical signatures for pointer equality. Therefore, the following are equivalent:
\item For every pair of distinct prime numbers $p$ and $q$, we have $p\cdot q\sim q\cdot p$, so our binary operation is commutative.
361
361
\item For every prime number $p$, we have $0\cdot p\sim0$ and $p\cdot0\sim0$, so that zero behaves like the \index{zero element}zero element.
362
362
\end{itemize}
363
-
In fact, no ``smaller'' presentation exists. It is perhaps surprising to constrast this with $(\mathbb{N},+,0)$, which just the free monoid with one generator.
363
+
In fact, no ``smaller'' presentation exists. It is perhaps surprising to contrast this with $(\mathbb{N},+,0)$, which just the free monoid with one generator.
0 commit comments