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 definitions from covcon-again

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-04-06 14:12:21 -05:00
parent 2fb0ef80ad
commit 8c522788bd
1 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -63,19 +63,28 @@ The algorithm for function overload resolution is now trivial: the type of `f(x)
The extra work is now in type normalization, which removes uses of `src` and `tgt` during quantification.
First, we normalize `F & function`, resulting in a type `(S1 -> T1) & ... & (SN -> TN)`. During normalization, we *saturate* the type:
First, we normalize `F & function`, resulting in a type `(S1 -> T1) & ... & (SN -> TN)`. During normalization, we ensure the type is *unambiguous* (defn 2.2 of https://www.irif.fr/~gc/papers/covcon-again.pdf):
* 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 any `i` and `j`, either `Si & Sj` is empty, or there is a unique least `Sk` such that `Si & Sj <: Sk`
*specialization sound* (defn 2.3 of https://www.irif.fr/~gc/papers/covcon-again.pdf)
* for any `i` and `j`, if `Si <: Sj` then `Ti <: Tj`.
and *union-saturated*
* for any `i` and `j`, there is an `Sk` such that `Si|Sj <: Sk` and `Tk <: Ti|Tj`
(union-saturation means the definition of `tgt` is the same as the algorithm in 4.4.3 of https://www.irif.fr/~gc/papers/covcon-again.pdf)
Then:
* `src F` is (S1 | ... | SN)`
* `tgt F(X)` is the most precise `Ti` such that `X <: Si`.
* `tgt F(X)` is the least `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.
If normalized 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:
For example normalizing `(number? -> string?) & (string? -> number?)` gives `(nil -> nil) & (number? -> string?) & (string? -> number?) & ((number | string)? -> (number | string)?)` so:
```
src((number? -> string?) & (string? -> number?)) is (number | string)?
@ -84,8 +93,6 @@ For example saturating `(number? -> string?) & (string? -> number?)` gives `(nil
tgt((number? -> string?) & (string? -> number?)) (nil) is nil
```
(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