[swift-evolution] [Pitch] Remove type inference for associated types

[Douglas Gregor]

> On Jun 25, 2016, at 12:51 AM, Dmitri Gribenko via swift-evolution <swift-evolution at swift.org> wrote:
> 
> On Fri, Jun 24, 2016 at 10:50 PM, Austin Zheng via swift-evolution
> <swift-evolution at swift.org> wrote:
>> Hello all,
>> 
>> Per Chris Lattner's list of open Swift 3 design topics
>> (http://article.gmane.org/gmane.comp.lang.swift.evolution/21369), I've put
>> together a proposal for removing type inference for associated types.
> 
> Hi Austin,
> 
> Thank you for starting this discussion!  There's one other alternative
> that I mentioned in one of the previous threads on this subject.  The
> idea is to limit the inference so that the sizes and the complexity of
> the problems that the type checker has to solve become tractable with
> a simple algorithm, not a full constrain solver.
> 
> Currently, as far as I understand, the type checker solves for all
> associated types for a protocol conformance in a single giant step,
> during which every decision can affect every other decision.  

That’s correct. It’s limiting that inference to a single conformance, but solving for all of the associated type witnesses simultaneously, using educated guesses as to which value witnesses will eventually be used (this is unchecked and seriously buggy). The fact that it’s only solving for a single conformance—e.g., “X : Collection” helps restrict the inference, but it’s also somewhat incorrect: why shouldn’t implementing a requirement from MutableCollection allow one to infer some associated type witness—say, the Index type—for a Collection? IIRC, we have some requirements duplicated in the standard library’s protocols simply to push the associated type inference into handling these cases.


> My
> suggestion is that we keep associated type inference for the simple
> cases where it is obvious what the user meant.  The author of the
> protocol would be able to identify these simple cases and define how
> exactly the inference should happen.  For example:
> 
> protocol Collection {
>  associatedtype Index
> 
>  @infers(Index)
>  var startIndex: Index
> 
>  // Does not affect associated type inference, types have to match
> with decisions made by other declarations.
>  var endIndex: Index
> 
>  // Does not affect associated type inference.
>  subscript(i: Index) -> Iterator.Element
> 
>  associatedtype Iterator
> 
>  @infers(Iterator)
>  func iterator() -> Iterator
> }
> 
> Under the current system, every declaration in a conforming type that
> matches a requirement that mentions 'Index' can affect the inference.
> That is, 'Index' is inferred from all declarations in the conforming
> type.   But there is no reason to make it that general -- the protocol
> author knows that 'var startIndex' in the conforming type has be of
> the right type, and there is no reason for other declaration to affect
> the decision about what 'Index' is resolved to.  Under the proposed
> rule, there is at most one declaration that the protocol author is
> allowed to designate with @infers, that is allowed to affect the
> inference.  If there is no @infers for a certain associated type, then
> it is never inferred and should always be specified explicitly.

Pragmatically, this approach can reduce associated type inference and its associated problems. It might even provide a way for us to stage in the removal of type inference for associated types from the language, by removing it from the “user-facing” language but leaving it enabled in key standard library protocols so we don’t regress too badly, giving us more time to sort out how defaulted associated types and type aliases in protocol extensions can fill the gap.

However, this doesn’t actually achieve the simplification in the type checker that is intended. We would still need to maintain the existing global inference algorithm, and while it would (overall) reduce the number of requirements we need to consider when inferring associated type witnesses, it’s still a global problem because you can still have several possible “startIndex” or “iterator()” potential witnesses to consider (e.g., in the type, protocol extensions, constrained protocol extensions, and so on; and it gets more interesting with conditional conformances). And as soon as you mark that subscript with @infers(Index), all of the complexity becomes apparent again.

That brings me to the other point about this: it’s changing the default, but nothing would prevent a user from simply marking every requirement with @infers(each-associated-type-listed), in which case we’ve not actually fixed the problem. 

> 
> This is the basic idea, I'm sure there are corner cases I haven't
> thought about (e.g., how does this interact with constrained
> extension, can we still solve everything with a simple algorithm?)
> But the reason why I'm suggesting this alternative is that I'm
> concerned that in simple cases like inferring the 'Index' and
> 'Iterator' typealiases having to specify them manually is just
> boilerplate, that does not add to clarity, and, I believe, can be
> inferred by the type checker without involving a heavy constrain
> solver.


The solver for associated type witnesses is not simple, despite my assertions in that amusing commit message. It’s just simpler than going through the (expression) constraint solver, which we had before. It has to track multiple solutions from different possible requirement/witness pairings, rank the results, etc. Nothing in this proposal simplifies any of that… it just tries to give that solver smaller problems to work with.

	- Doug