Uniformize extension binding/lookup

[kyouko-taiga]

The compiler currently handles extensions and conformances during name lookup in a rather unprincipled manner. It seems to me that a big part of the issue revolves around universally quantified extensions. I'll explain.

Note: For most intents and purposes, extensions and conformances work the same way. So for concision I'll just talk about extensions in the remainder.

Extension binding

One important prerequisite for name resolution is that we can identify the types extended by extension declarations. This information is easy to figure out when the extension relates to a concrete, non-generic type (let's ignore where clauses for the time being). For example, extension binding for the declaration below is completely obvious:

extension Int { public fun f() -> Int { copy() } }

Things get a little more complex when we're extending a generic type. For example:

extension Array { public fun f() -> Int { count() } }

What does it mean to extend Array? After all, Array isn't really a type. Rather, it is a function that returns one when we apply it. In literature we typically say that Array is a type constructor.

Extending a type constructor doesn't make much sense. It would be like extending a function. So when we're saying that we're extending Array, actually we're saying that we're extending all the types resulting from the application of Array. In other words, we're saying something like "for all types T, Array<T> is extended as follows ...". That's universal quantification.

Using some fictional syntax, we could make this universal quantification much more explicit:

extension<T> Array<T> { public fun f() -> Int { count() } }

Another way to introduce quantification implicitly is to extend a trait. When we write extension Collection, we're actually saying something like "for all types T such that T is a collection, T is extended as follows ...". Again, we could make this quantification explicit:

extension<T: Collection> T { ... }

Side note: It may be worth at some point to weigh the pros and cons of implicit quantification. On one hand, it save us a couple of angle brackets and let us avoid repeating generic parameters. On the other, it makes it adds a layer of indirection in the explanation of the system because, as mentioned, extending Array doesn't actually make any sense.

Extension lookup

Most of the complexity behind name resolution in Hylo is due to the fact that looking in the scope of a type starts a sort of global quest in the entire AST to find extensions of that type. Extensions of concrete, non-generic types are easy to handle. We can just build a table mapping a type to its extensions and we are done. Extensions of generic types require more care, again.

Say we have an Array<Bool> and we're looking for its extensions. We can't just check whether Array<Bool> is in the table. We wouldn't find what we're looking for because all extensions of Array are universally quantified. Instead, we have to find an extension of Array<T> for some T that can be unified with Bool, at least in principle.

The current implementation cheats in two different ways to deal with this problem.

• When we extend a type constructor, we register its head in the table, i.e., a type applications without any parameter. Then when we're looking for Array<Bool>'s extensions, we can actually look for the unapplied type instead (i.e., Array) and re-apply the type arguments later.
• When we extend a trait, we register its receiver parameter in the table, i.e., the implicit Self parameter that's declared in every trait. Then when we're looking for Collection's extensions, we can actually look for its corresponding receiver parameter.

Both of these tricks are a little "dirty". The first one ignores the distinction between types and type constructors, requiring special casing to strip type arguments or reapply them. The second ignores the theoretical scope in which universally quantified parameters are bound, requiring special casing to figure out the intended meaning of generic type parameters occurring in the signature of an extension.

Limits of current workarounds

In addition to "feel" unprincipled, the above-mentioned tricks actually break in the presence of structural types. Unlike Swift, Hylo lets us extend any type we want, including a structural one. A good justifying use case is Optional<T>, which is in fact an alias for Union<T, Some<T>> in the standard library. The ability to extend such a structural type lets us write, for example:

extension Optional {
  public static fun none() -> Self {
    None() as Optional
  }
}

But now the workarounds to circumvent universal quantification fail because we have no simple way to express unapplied constructors of arbitrary structural types. It kind of works for for optionals but only because of a mostly a happy coincidence: we consider Optional to be a type constructor and use the same trick as we do for Array. But then we can only find the extension if we're looking into a Optional<T>, not if we're looking into a Union<T, None<T>>.

public fun main() {
  let _: Optional<Int> = .none() // OK
  let _: Union<Int, None<Int>> = .none() // Error
}

That isn't intended behavior. typealias is not declaring a new type, merely an alias to some structural type. So Optional<Int> and Union<Int, None<Int>> should be interchangeable in any context.

Fixing the workarounds

Instead of using the above-mentioned workarounds, we should embrace the fact that extensions of generic types and traits are universally quantified, meaning that extension lookup should use unification rather than equality.