mirrors/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2024-11-15 14:25:44 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge branch 'master' into merge

Browse Source
This commit is contained in:
Vyacheslav Egorov 2023-08-25 18:45:50 +03:00
commit 263c282635
5 changed files with 230 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/_pages/performance.md
View File

@ -88,7 +88,7 @@ For this mechanism to work, function call must be "obvious" to the compiler - it
The mechanism works by directly invoking a highly specialized and optimized implementation of a builtin function from the interpreter core loop without setting up a stack frame and omitting other work; additionally, some fastcall specializations are partial in that they don't support all types of arguments, for example all `math` library builtins are only specialized for numeric arguments, so calling `math.abs` with a string argument will fall back to the slower implementation that will do string->number coercion.
As a result, builtin calls are very fast in Luau - they are still slightly slower than core instructions such as arithmetic operations, but only slightly so. The set of fastcall builtins is slowly expanding over time and as of this writing contains `assert`, `type`, `typeof`, `rawget`/`rawset`/`rawequal`, `getmetatable`/`setmetatable`, all functions from `math` and `bit32`, and some functions from `string` and `table` library.
As a result, builtin calls are very fast in Luau - they are still slightly slower than core instructions such as arithmetic operations, but only slightly so. The set of fastcall builtins is slowly expanding over time and as of this writing contains `assert`, `type`, `typeof`, `rawget`/`rawset`/`rawequal`, `getmetatable`/`setmetatable`, `tonumber`/`tostring`, all functions from `math` (except `noise` and `random`/`randomseed`) and `bit32`, and some functions from `string` and `table` library.
Some builtin functions have partial specializations that reduce the cost of the common case further. Notably:
@ -98,7 +98,7 @@ Some builtin functions have partial specializations that reduce the cost of the
Some functions from `math` library like `math.floor` can additionally take advantage of advanced SIMD instruction sets like SSE4.1 when available.
In addition to runtime optimizations for builtin calls, many builtin calls can also be constant-folded by the bytecode compiler when using aggressive optimizations (level 2); this currently applies to most builtin calls with constant arguments and a single return value. For builtin calls that can not be constant folded, compiler assumes knowledge of argument/return count (level 2) to produce more efficient bytecode instructions.
In addition to runtime optimizations for builtin calls, many builtin calls, as well as constants like `math.pi`/`math.huge`, can also be constant-folded by the bytecode compiler when using aggressive optimizations (level 2); this currently applies to most builtin calls with constant arguments and a single return value. For builtin calls that can not be constant folded, compiler assumes knowledge of argument/return count (level 2) to produce more efficient bytecode instructions.
## Optimized table iteration

2
papers/hatra23/bibliography.bib
View File

@ -1,6 +1,6 @@
@InProceedings{BFJ21:GoalsLuau,
author = {L. Brown and A. Friesen and A. S. A. Jeffrey},
title = {Goals of the Luau Type System},
title = {Position Paper: Goals of the Luau Type System},
booktitle = {Proc. Human Aspects of Types and Reasoning Assistants},
year = {2021},
url = {https://asaj.org/papers/hatra21.pdf},

BIN
papers/hatra23/hatra23.pdf
View File

Binary file not shown.

56
papers/hatra23/hatra23.tex
View File

@ -12,6 +12,7 @@
\newcommand{\ANY}{\mathtt{any}}
\newcommand{\ERROR}{\mathtt{error}}
\newcommand{\NUMBER}{\mathtt{number}}
\begin{document}
@ -48,7 +49,7 @@ error reporting). Roblox has hundreds of millions of users, and
millions of creators, ranging from children learning to program for
the first time to professional development studios.
In HATRA 2021, we presented \emph{The Goals Of The Luau Type
In HATRA 2021, we presented a position paper on the \emph{Goals Of The Luau Type
System}~\cite{BFJ21:GoalsLuau}, describing the human factors issues
with designing a type system for a language with a heterogeneous
developer community. The design flows from the needs of the different
@ -58,9 +59,9 @@ quality concerns of more experienced developers; for all users
type-driven tooling is important for productivity. These needs result in a design with two modes:
\begin{itemize}
\item \emph{non-strict mode}, aimed at non-professionals, focused on
minimizing false positives, and
minimizing false positives (that is, in non-strict mode, any program with a type error has a defect), and
\item \emph{strict mode}, aimed at professionals, focused on
minimizing false negatives (i.e.~type soundness).
minimizing false negatives (that is, in strict mode, any program with a defect has a type error).
\end{itemize}
%% For both communities, type-driven tooling is important, so we
%% provide \emph{infallible type inference}, which infers types
@ -81,21 +82,58 @@ inclusion~\cite{GF05:GentleIntroduction}. This is aligned with the
\emph{minimize false positives} goal of Luau non-strict mode, since
semantic subtyping only reports a failure of subtyping when there is a
value which inhabits the candidate subtype, but not the candidate
supertype. This has the added benefit of improving error reporting in
the prototype implementation: since the prototype is constructive, the
witness for the failure of subtyping can help drive error reports.
supertype.
For example, the program:
\begin{verbatim}
local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then y = CFrame.new() else y = Vector3.new() end
local z : Vector3 | CFrame = x * y
\end{verbatim}
cannot produce a run-time error, since multiplication of \verb|CFrame|s is overloaded:
\begin{verbatim}
((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)
\end{verbatim}
In order to typecheck this program, we check that that type is a subtype of:
\begin{verbatim}
(CFrame, Vector3 | CFrame) -> (Vector3 | CFrame)
\end{verbatim}
In the previous, syntax-driven, implementation of subtyping, this subtype check would fail, resulting in a false positive.
We have now released an implementation of semantic subtyping, which does not suffer from this defect.
See our technical blog for more details~\cite{Jef22:SemanticSubtyping}.
Rather than the gradual typing approach
of~\cite{ST07:GradualTyping}, which uses \emph{consistent
of Siek and Taha~\cite{ST07:GradualTyping}, which uses \emph{consistent
subtyping} where $\ANY \lesssim T \lesssim \ANY$ for any type $T$, we
adopt an approach based on \emph{error suppression}, where $\ANY$ is
an error-suppressing type, and any failures of subtyping involving
error-suppressing types are not reported. Users can explicitly
suppress type errors by declaring variables with type $\ANY$, and
since an expression with a type error has an error-suppressing type we
avoid cascading errors. Error suppression is in production Luau, and is
mechanically verified~\cite{BJ23:agda-typeck}.
avoid cascading errors.
We do this by defining a \emph{infallible} typing judgment $\Gamma \vdash M : T$
such that for any $\Gamma$ and $M$, there is a $T$ such that $\Gamma \vdash M : T$.
For example the rule for addition (ignoring overloads for simplicity) is:
\[
\frac{\Gamma \vdash M : T \quad \Gamma \vdash M : U}{\Gamma \vdash M+N : \NUMBER}
\]
We define which judgments produce warnings, for example that rule produces a warning
when
\begin{itemize}
\item either $T \not<: \NUMBER$ and $T$ is not error-suppressing,
\item or $U \not<: \NUMBER$ and $U$ is not error-suppressing.
\end{itemize}
To retain type soundness (in the absence of user-supplied error-suppressing types)
we show that
if $\Gamma \vdash M : T$ and $T$ is error-suppressing, then either
\begin{itemize}
\item $\Gamma$ or $M$ contains an error-suppressing type, or
\item $\Gamma \vdash M : T$ produces a warning.
\end{itemize}
From this it is straightforward to show the usual ``well typed
programs don't go wrong'' type soundness result for programs without explicit
error-suppressing types~\cite{BJ23:agda-typeck}.
\section{Further work}

180
rfcs/local-type-inference.md Normal file
View File

@ -0,0 +1,180 @@
# Local Type Inference
## Summary
We are going to supplant the current type solver with one based on Benjamin Pierce's Local Type Inference algorithm:
https://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf
## Motivation
Luau's type inference algorithm is used for much more than typechecking scripts. It is also the backbone of an autocomplete algorithm which has to work even for people who don't know what types or type systems are.
We originally implemented nonstrict mode by making some tactical adjustments to the type inference algorithm. This was great for reducing false positives in untyped code, but carried with it the drawback that the inference result was usually not good enough for the autocomplete system. In order to offer a high quality experience, we've found ourselves to run type inference on nonstrict scripts twice: once for error feedback, and once again to populate the autocomplete database.
Separately, we would also like more accurate type inference in general. Our current type solver jumps to conclusions a little bit too quickly. For example, it cannot infer an accurate type for an ordinary search function:
```lua
function index_of(tbl, el)
for i = 0, #tbl do
if tbl[i] == el then
return i
end
end
return nil
end
```
Our solver sees two `return` statements and assumes that, because the first statement yields a `number`, so too must the second.
To fix this, we are going to move to an architecture where type inference and type checking are two separate steps. Whatever mode the user is programming with, we will run an accurate type inference pass over their code and then run one of two typechecking passes over it.
## Notation
We'll use the standard notation `A <: B` to indicate that `A` is a subtype of `B`.
## Design
At a very high level, local type inference is built around the idea that we track the lower bounds and their upper bounds. The lower bounds of a binding is the set of values that it might conceivably receive. If a binding receives a value outside of its upper bounds, the program will fail.
At the implementation level, we reencode free types as the space between these bounds.
Upper bounds arise only from type annotations and certain builtin operations whereas lower bounds arise from assignments, return statements, and uses.
Free types all start out with bounds `never <: 't <: unknown`. Intuitively, we say that `'t` represents some set of values whose domain is at least `never` and at most `unknown`. This naturally could be any value at all.
When dispatching a constraint `T <: 't`, we replace the lower bounds of `'t` by the union of its old lower bounds and `T`. When dispatching a constraint `'t <: T`, we replace the upper bounds by its upper bound intersected with `T`. In other words, lower bounds grow from nothing as we see the value used whereas the upper bound initially encompasses everything and shrinks as we constrain it.
### Constraint Generation Rules
A return statement expands the lower bounds of the enclosing function's return type.
```lua
function f(): R
local x: X
return x
-- X <: R
end
```
An assignment adds to the lower bounds of the assignee.
```lua
local a: A
local b: B
a = b
-- B <: A
```
A function call adds to the upper bounds of the function being called.
Equivalently, passing a value to a function adds to the upper bounds of that value and to the lower bounds of its return value.
```lua
local g
local h: H
local j = g(h)
-- G <: (H) -> I...
-- I... <: J
```
Property access is a constraint on a value's upper bounds.
```lua
local a: A
a.b = 2
-- A <: {b: number}
a[1] = 3
-- A <: {number}
```
### Generalization
Generalization is the process by which we infer that a function argument is generic. Broadly speaking, we solve constraints that arise from the function interior, we scan the signature of the function for types that are unconstrained, and we replace those types with generics. This much is all unchanged from the old solver.
Unlike with the old solver, we never bind free types when dispatching a subtype constraint under local type inference. We only bind free types during generalization.
If a type only appears in covariant positions in the function's signature, we can replace it by its lower bound. If it only appears in contravariant positions, we replace it by its upper bound. If it appears in both, we'll need to implement bounded generics to get it right. This is beyond the scope of this RFC.
If a free type has neither upper nor lower bounds, we replace it with a generic.
Some simple examples:
```lua
function print_number(n: number) print(n) end
function f(n)
print_number(n)
end
```
We arrive at the solution `never <: 'n <: number`. When we generalize, we can replace `'n` by its upper bound, namely `number`. We infer `f : (number) -> ()`.
Next example:
```lua
function index_of(tbl, el) -- index_of : ('a, 'b) -> 'r
for i = 0, #tbl do -- i : number
if tbl[i] == el then -- 'a <: {'c}
return i -- number <: 'r
end
end
return nil -- nil <: 'r
end
```
When typechecking this function, we have two constraints on `'r`, the return type. We can combine these constraints by taking the union of the lower bounds, leading us to `number | nil <: 'r <: unknown`. The type `'r` only appears in the return type of the function. The return type of this function is `number | nil`.
At runtime, Luau allows any two values to be compared. Comparisons of values of mismatched types always return `false`. We therefore cannot produce any interesting constraints about `'b` or `'c`.
We end up with these bounds:
```
never <: 'a <: {'c}
never <: 'b <: unknown
never <: 'c <: unknown
number | nil <: 'r <: unknown
```
`'a` appears in the argument position, so we replace it with its upper bound `{'c}`. `'b` and `'c` have no constraints at all so they are replaced by generics `B` and `C`. `'r` appears only in the return position and so is replaced by its lower bound `number | nil`.
The final inferred type of `index_of` is `<B, C>({C}, B) -> number | nil`.
## Drawbacks
This algorithm requires that we create a lot of union and intersection types. We need to be able to consistently pare down degenerate unions like `number | number`.
Local type inference is also more permissive than what we have been doing up until now. For instance, the following is perfectly fine:
```lua
local x = nil
if something then
x = 41
else
x = "fourty one"
end
```
We'll infer `x : number | string | nil`. If the user wishes to constrain a value more tightly, they will have to write an annotation.
## Alternatives
### What TypeScript does
TypeScript very clearly makes it work in what we would call a strict mode context, but we need more in order to offer a high quality nonstrict mode. For instance, TypeScript's autocomplete is completely helpless in the face of this code fragment:
```ts
let x = null;
x = {a: "a", b: "pickles"};
x.
```
TypeScript will complain that the assignment to `x` is illegal because `x` has type `null`. It will further offer no autocomplete suggestions at all when the user types the final `.`.
It's not viable for us to require users to write type annotations. Many of our users do not yet know what types are but we are nevertheless committed to providing them a tool that is helpful to them.
### Success Typing
Success typing is the algorithm used by the Dialyzer inference engine for Erlang. Instead of attempting to prove that values always flow in sensible ways, it tries to prove that values _could_ flow in sensible ways.
Success typing is quite nice in that it's very forgiving and can draw surprisingly useful information from untyped code, but that forgiving nature works against us in the case of strict mode.