diff --git a/rfcs/generic-function-subtyping.md b/rfcs/generic-function-subtyping.md new file mode 100644 index 000000000..b9c0c430b --- /dev/null +++ b/rfcs/generic-function-subtyping.md @@ -0,0 +1,211 @@ +# Expanded Subtyping for Generic Function Types + +## Summary + +Extend the subtyping relation for function types to relate generic function +types with compatible instantiated function types. + +## Motivation + +As Luau does not have an explicit syntax for instantiation, there are a number +of places where the typechecker will automatically perform instantiation with +the goal of permitting more programs. These instances of instantiation are +ad-hoc and strategic, but useful in practice for permitting programs such as: + +```lua +function id(x: T): T + return x +end + +local idNum : (number) -> number +idNum = id -- ok +``` + +However, they have also been a source of some typechecking bugs because of how +they actually make a determination as to whether the instantation should happen, +and they currently open up some potential soundness holes when instantiating +functions in table types since properties of tables are mutable and thus need to +be invariant (which the automatic-instantiation potentially masks). + +## Design + +The goal then is to rework subtyping to support the relationship we want in the +first place: allowing polymorphic functions to be used where instantiated +functions are expected. In particular, this means adding instantiation itself to +the subtyping relation. Formally, that'd look something like: + +``` +instantiate((T1) -> T2) = (T1') -> T2' +(T1') -> T2' <: (T3) -> T4 +-------------------------------------------- +(T1) -> T2 <: (T3) -> T4) +``` + +Or informally, we'd say that a generic function type is a subtype of another +function type if we can instantiate it and show that instantiated function type +to be a subtype of the original function type. Implementation-wise, this loose +formal rule suggests a strategy of when we'll want to apply instantiation. +Namely, whenever the subtype and supertype are both functions with the potential +subtype having some generic parameters and the supertype having none. So, if we +look once again at our simple example from motivation, we can walk through how +we expect it to type check: + +```lua +function id(x: T): T + return x +end + +local idNum : (number) -> number +idNum = id -- ok +``` + +First, `id` is given the type `(T) -> T` and `idNum` is given the type +`(number) -> number`. When we actually perform the assignment, we must show that +the type of the right-hand side is compatible with the type of the left-hand +side according to subtyping. That is, we'll ask if `(T) -> T` is a subtype of +`(number) -> number` which matches the rule to apply instantiation since the +would-be subtype has a generic parameter while the would-be supertype has no +generic parameters. This contrasts with the current implementation which, before +asking the subtyping question, checks if the type of the right-hand side +contains any generics at any point and if the type of the left-hand side cannot +_possibly_ contain generics and instantiates the right-hand side if so. + +Adding instantiation to subtyping does pose some additional questions still +about when exactly to instantiate. Namely, we need to consider cases like +function application. We can see why by looking at some examples: + +```lua +function rank2(f: (a) -> a): (number) -> number + return f +end +``` + +In this case, we expect to allow the instantiation of `f` from `(a) -> a` to +`(number) -> number`. After all, we can consider other cases like where the body +instead applies `f` to some particular value, e.g. `f(42)`, and we'd want the +instantiation to be allowed there. However, this means we'd potentially run into +issues if we allowed call sites to `rank2` to pass in non-polymorphic functions. +A naive approach to implementing this proposal would do exactly that because we +currently treat contravariant subtyping positions (i.e. for the arguments of +functions) as being the same as our normal (i.e. covariant) subtyping relation +but with the arguments reversed. So, to type check an application like +`rank2(function(str: string) return str + "s" end)` (where the function argument +is of type `(string) -> string`), we would ask if `(a) -> a` is a subtype of +`(string) -> string`. This is precisely the question we asked in the original +example, but in the contravariant context, this is actually unsound since +`rank2` would then function as a general coercion from, e.g., +`(string) -> string` to `(number) -> number`. + +This sort of behavior does come up in other languages that mix polymorphism and +subtyping. If we consider the same example in F#, we can compare its behavior: + +```fsharp +let ranktwo (f : 'a -> 'a) : int -> int = f +let pluralize (s : string) : string = s + "s" +let x = ranktwo pluralize +``` + +For this example, F# produces one warning and one error. The warning is applied +to the function definition of `ranktwo` itself (coded `FS0064`), and says "This +construct causes code to be less generic than indicated by the type annotations. +The type variable 'a has been constrained to be type 'int'." This warning +highlights the actual difference between our example in Luau and the F# +translation. In F#, `'a` is really a free type variable, rather than a generic +type parameter of the function `ranktwo`, as such, this code actually +constrains the type of `ranktwo` to be `(int -> int) -> (int -> int)`. As such, +the application on line 3 errors because our `(string -> string)` function is +simply not compatible with that type. With higher-rank polymorphic function +parameters, it doesn't make sense to warn on their instantiation (as illustrated +by the example of actually applying `f` to some particular data in the +definition of `rank2`), but it's still just as problematic if we were to accept +instantiated functions at polymorphic types. Thus, it's important that we +actually ensure that we only instantiate in covariant contexts. So, we must +ensure that subtyping only instantiates in covariant contexts. + +It may also be helpful to consider an example of rank-1 polymorphism to +understand the full scope of the behavior. So, we can look at what happens if we +simply move the type parameter out in our working example: + +```lua +function rank1(f: (a) -> a): (number) -> number + return f +end +``` + +In this case, we expect an error to occur because the type of `f` depends on +what we instantiate `rank1` with. If we allowed this, it would naturally be +unsound because we could again provide a `(string) -> string` argument (by +instantiating `a` with `string`). This reinforces the idea that the presence of +the generic type parameter is likely to be a good option for determining +instantiation (at least when compared to the presence of free type variables). + +## Drawbacks + +One of the aims of this proposal is to provide a clear and predictable mental +model of when instantiation will take place in Luau. The author feels this +proposal is step forward compared to the existing ad-hoc usage of instantiation +in the typechecker, but it's possible that programmers are already comfortable +with the mental model they have built for the existing implementation. +Hopefully, this is mitigated by the fact that the new setup should allow all of +the _sound_ uses of instantiation permitted by the existing system. Notably, +however, programmers may be surprised by the added restriction when it comes to +properties in tables. In particular, we can consider a small variation of our +original example with identity functions: + +```lua +function id(x: T): T + return x +end + +local poly : { id : (a) -> a } = { id = id } + +local mono : { id : (number) -> number } +mono = poly -- error! +mono.id = id -- also an error! +``` + +In this case, the fact that we're dealing with a _property_ of a table type +means that we're in a context that needs to be invariant (i.e. not allow +subtyping) to avoid unsoundness caused by interactions between mutable +references and polymorphism (see things like the [value +restriction in OCaml][value-restriction] to understand why). In most cases, we +believe programmers will be using functions in tables as an implementation of +methods for objects, so we don't anticipate that they'll actually _want_ to do +the unsound thing here. The accepted RFC for [read-only +properties][read-only-props] gives us a technically-precise solution since +read-only properties would be free to be typechecked as a covariant context +(since they disallow mutation), and thus if the property `id` was marked +read-only, we'd be able to do both of the assignments in the above example. + +## Alternatives + +The main alternatives would likely be keeping the existing solution (and +likely having to tactically fix future bugs where instantiation either happens +too much or not enough), or removing automatic instantiation altogether in favor +of manual instantiation syntax. The former solution (changing nothing) is cheap +now (both in terms of runtime performance and also development cost), but the +existing implementation involves extra walks of both types to make a decision +about whether or not to perform instantiation. To minimize the performance +impact, the functions that perform these questions (`isGeneric` and +`maybeGeneric`) actually do not perform a full walk, and instead try to +strategically look at only enough to make the decision. We already found and +fixed one bug that was caused by these functions being too imprecise against +their spec, but fleshing them out entirely could potentially be a noticeable +performance regression since the decision to potentially instantiate is one that +comes up often. + +Removing automatic instantiation altogether, by contrast, will definitely be +"correct" in that we'll never instantiate in the wrong spot and programmers will +always have the ability to instantiate, but it would be a marked regression on +developer experience since it would increase the annotation burden considerably +and generally runs counter to the overall design strategy of Luau (which focuses +heavily on type inference). It would also require us to actually pick a syntax +for manual instantiation (which we are still open to do in the future if we +maintain an automatic instantiation solution) which is frought with parser +ambiguity issues or requires the introduction of a sigil like Rust's turbofish +for instantiation. Discussion of that syntax is present in the [generic +functions][generic-functions] RFC. + +[value-restriction]: https://stackoverflow.com/questions/22507448/the-value-restriction#22507665 +[read-only-props]: https://github.com/Roblox/luau/blob/master/rfcs/property-readonly.md +[generic-functions]: https://github.com/Roblox/luau/blob/master/rfcs/generic-functions.md