[Constraint solver] Introduce one-way binding constraints. #25983
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
xedin
reviewed
Jul 6, 2019
DougGregor
force-pushed
the
one-way-constraints
branch
from
1c27edc to
e48b471
Compare
DougGregor
force-pushed
the
one-way-constraints
branch
2 times, most recently
from
d39a964 to
8aab162
Compare
|
The changes to the connected-components algorithm are separated out into #26383. |
DougGregor
force-pushed
the
one-way-constraints
branch
2 times, most recently
from
c2296e5 to
07c8a64
Compare
|
@swift-ci please test source compatibility |
|
@swift-ci please smoke test |
|
@swift-ci please test compiler performance |
|
@swift-ci please test source compatibility |
|
@swift-ci please test compiler performance |
|
I'm staging in all of the pieces for this (e.g., #26530) and will rebase shortly. |
Introduce the notion of "one-way" binding constraints of the form $T0 one-way bind to $T1 which treats the type variables $T0 and $T1 as independent up until the point where $T1 simplifies down to a concrete type, at which point $T0 will be bound to that concrete type. $T0 won't be bound in any other way, so type information ends up being propagated right-to-left, only. This allows a constraint system to be broken up in more components that are solved independently. Specifically, the connected components algorithm now proceeds as follows: 1. Compute connected components, excluding one-way constraints from consideration. 2. Compute a directed graph amongst the components using only the one-way constraints, where an edge A -> B indicates that the type variables in component A need to be solved before those in component B. 3. Using the directed graph, compute the set of components that need to be solved before a given component. To utilize this, implement a new kind of solver step that handles the propagation of partial solutions across one-way constraints. This introduces a new kind of "split" within a connected component, where we collect each combination of partial solutions for the input components and (separately) try to solve the constraints in this component. Any correct solution from any of these attempts will then be recorded as a (partial) solution for this component. For example, consider: let _: Int8 = b ? Builtin.one_way(int8Or16(17)) : Builtin.one_way(int8Or16(42\ )) where int8Or16 is overloaded with types `(Int8) -> Int8` and `(Int16) -> Int16`. There are two one-way components (`int8Or16(17)`) and (`int8Or16(42)`), each of which can produce a value of type `Int8` or `Int16`. Those two components will be solved independently, and the partial solutions for each will be fed into the component that evaluates the ternary operator. There are four ways to attempt that evaluation: ``` [Int8, Int8] [Int8, Int16] [Int16, Int8] [Int16, Int16] To test this, introduce a new expression builtin `Builtin.one_way(x)` that introduces a one-way expression constraint binding the result of the expression 'x'. The builtin is meant to be used for testing purposes, and the one-way constraint expression itself can be synthesized by the type checker to introduce one-way constraints later on. Of these two, there are only two (partial) solutions that can work at all, because the types in the ternary operator need a common supertype: [Int8, Int8] [Int16, Int16] Therefore, these are the partial solutions that will be considered the results of the component containing the ternary expression. Note that only one of them meets the final constraint (convertibility to `Int8`), so the expression is well-formed. Part of rdar://problem/50150793.
…ilders When we transform each expression or statement in a function builder, introduce a one-way constraint so that type information does not flow backwards from the context into that statement or expression. This more closely mimics the behavior of normal code, where type inference is per-statement, flowing from top to bottom. This also allows us to isolate different expressions and statements within a closure that's passed into a function builder parameter, reducing the search space and (hopefully) improving compile times for large function builder closures. For now, put this functionality behind the compiler flag `-enable-function-builder-one-way-constraints` for testing purposes; we still have both optimization and correctness work to do to turn this on by default.
DougGregor
force-pushed
the
one-way-constraints
branch
from
d457f42 to
be73a9d
Compare
|
@swift-ci please smoke test |
|
@swift-ci please test source compatibility |
|
@swift-ci please test compiler performance |
|
This should be a no-op, because all of the one-way constraints code is behind a flag. Performance + compatibility testing is to ensure I didn't inadvertently break things in this refactoring. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Introduce the notion of "one-way" binding constraints of the form
which treats the type variables $T0 and $T1 as independent up until
the point where $T1 simplifies down to a concrete type, at which point
$T0 will be bound to that concrete type. $T0 won't be bound in any
other way, so type information ends up being propagated right-to-left,
only. This allows a constraint system to be broken up in more
components that are solved independently. Specifically, the connected
components algorithm now proceeds as follows:
consideration.
one-way constraints, where an edge A -> B indicates that the type
variables in component A need to be solved before those in component
B.
to be solved before a given component.
To utilize this, implement a new kind of solver step that handles the
propagation of partial solutions across one-way constraints. This
introduces a new kind of "split" within a connected component, where
we collect each combination of partial solutions for the input
components and (separately) try to solve the constraints in this
component. Any correct solution from any of these attempts will then
be recorded as a (partial) solution for this component.
For example, consider:
where int8Or16 is overloaded with types
(Int8) -> Int8and(Int16) -> Int16. There are two one-way components (int8Or16(17))and (
int8Or16(42)), each of which can produce a value of typeInt8or
Int16. Those two components will be solved independently, and thepartial solutions for each will be fed into the component that
evaluates the ternary operator. There are four ways to attempt that
evaluation:
To test this, introduce a new expression builtin
Builtin.one_way(x)thatintroduces a one-way expression constraint binding the result of the
expression 'x'. The builtin is meant to be used for testing purposes,
and the one-way constraint expression itself can be synthesized by the
type checker to introduce one-way constraints later on.
Of these two, there are only two (partial) solutions that can work at
all, because the types in the ternary operator need a common
supertype:
Therefore, these are the partial solutions that will be considered the
results of the component containing the ternary expression. Note that
only one of them meets the final constraint (convertibility to
Int8), so the expression is well-formed.Implements the core of rdar://problem/50150793.