luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

Added saturation to the algorithm

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-04-05 17:01:37 -05:00
parent d31a28a08c
commit 8845d33e4d
1 changed files with 62 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
rfcs/function-overload-resolution.md
View file

@ -59,26 +59,23 @@ We do this by introducing types `src F` and `tgt F(X)` (syntax to be bikeshedded
hopefully it will never be seen by creators!), standing for the parameter and
result types of applying a function of type `F` to an argument of type `X`.
The algorithm for function overload resolution is now trivial: the type of `f(x)` is just `tgt F(X)`, and this introduces a constraint `X <: src(F)`.
The algorithm for function overload resolution is now trivial: the type of `f(x)` is just `tgt F(X & src F)`, and this introduces a constraint `X <: src(F)`.
The extra work is now in type normalization, which removes uses of `src` and `tgt` during quantification:
The extra work is now in type normalization, which removes uses of `src` and `tgt` during quantification.
```
src (T -> U) is T
src (T & U) is src T | src U
src (T | U) is src T & src U
src T is src F when T is a table with a metatable with a __call__ property of type F
src T is none in any other case
First, we normalize `F & function`, resulting in a type `(S1 -> T1) & ... & (SN -> TN)`. During normalization, we *saturate* the type:
tgt (T -> U) (V) is U when (T&V) is inhabited
tgt (T & U) (V) is tgt T(V) & tgt U(V)
tgt (T | U) (V) is tgt T(V) | tgt U(V)
tgt T (V) is tgt F(V) when T is a table with a metatable with a __call__ property of type F
tgt top (T) is top
tgt T (V) is none in any other case
```
* for any `(Si -> Ti)` and `(Sj -> Tj)` in the saturation, `((Si|Sj) -> (Ti|Tj))` is in the saturation, and
* for any `(Si -> Ti)` and `(Sj -> Tj)` in the saturation, `((Si&Sj) -> (Ti&Tj))` is in the saturation.
For example:
Then:
* `src F` is (S1 | ... | SN)`
* `tgt F(X)` is the most precise `Ti` such that `X <: Si`.
If saturated types are ordered by subtyping order, this is the same as the current algorithm for function overload resolution.
For example saturating `(number? -> string?) & (string? -> number?)` gives `(nil -> nil) & (number? -> string?) & (string? -> number?) & ((number | string)? -> (number | string)?)` so:
```
src((number? -> string?) & (string? -> number?)) is (number | string)?
@ -87,26 +84,69 @@ For example:
tgt((number? -> string?) & (string? -> number?)) (nil) is nil
```
(This is a variant of the algorithm used in the Luau prototype.)
(This is a variant of the algorithm given in https://www.irif.fr/~gc/papers/covcon-again.pdf)
The real thing would need scaled up to type packs and generic functions.
As an optimization, saturation can merge functions with the same
return types (since `(S1 -> T) & (S2 -> T)` is equivalent to `(S1 |
S2) -> T`). For example, the
unsaturated type for `CFrame.new` is
```
(() -> CFrame)
& ((Vector3, Vector3) -> CFrame)
& ((number, number, number) -> CFrame)
& ((number, number, number, number, number, number) -> CFrame)
& ((number, number, number, number, number, number, number, number, number, number, number, number) -> CFrame)
```
saturating this would result in 32 overloads, but this can be optimized to one:
```
( ()
| (Vector3, Vector3)
| (number, number, number)
| (number, number, number, number, number, number)
| (number, number, number, number, number, number, number, number, number, number, number, number)
) -> CFrame
```
Hopefully this is a common case, since Roblox API function overloads all share a return type,
and we don't infer overloaded functions.
This does depend on having unions of type packs.
## Drawbacks
Anything we do about this will be a breaking change.
Scaling this up to type packs probably involves intersection and union on packs.
There may be other devils in the details.
Scaling this up to type packs involves intersection and union on packs.
We need to ensure `src` and `tgt` do not leak.
We need to make sure that normalization doesn't lose valuable autocomplete information.
We need an algorithm for "is a type inhabited".
In this proposal, the type of `f(x)` can depend on the type of `x`, which may cause complexity in type inference.
There may be other devils in the details.
## Alternatives
We could try applying fixes to the current algorithm, and live with constraint order mattering.
We could adopt the Flow solution, which adds "if this then that" constraints, but that makes it very likely we will need to introduce additional backtracking.
We could adopt the TypeScript or Flow solution, which adds "if this then that" constraints, but that makes it very likely we will need to introduce additional backtracking.
We could normalize all types to have the same return type, by equating `(S1 -> T1) & (S2 -> T2)` with `((S1 | S2) -> (T1 & T2))`. This is a breaking change, though in a corner case I doubt has had much use. It does mean that `&` and `|` aren't just intersection and union any more, for example `(string -> number) & (number -> string)` contains
```lua
function(x)
if type(x) == "string" then
return 1
else
return "hi"
end
end
```
which is not in `(string | number) -> never`.