From 8845d33e4d92ecf44f7eb5e8b925d9ab9c3ebf93 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 5 Apr 2022 17:01:37 -0500 Subject: [PATCH] Added saturation to the algorithm --- rfcs/function-overload-resolution.md | 84 ++++++++++++++++++++-------- 1 file changed, 62 insertions(+), 22 deletions(-) diff --git a/rfcs/function-overload-resolution.md b/rfcs/function-overload-resolution.md index 7f26e318..2e6b2e4a 100644 --- a/rfcs/function-overload-resolution.md +++ b/rfcs/function-overload-resolution.md @@ -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`.