diff --git a/Analysis/include/Luau/ToString.h b/Analysis/include/Luau/ToString.h index efe82b12..a256e12f 100644 --- a/Analysis/include/Luau/ToString.h +++ b/Analysis/include/Luau/ToString.h @@ -11,6 +11,7 @@ LUAU_FASTINT(LuauTableTypeMaximumStringifierLength) LUAU_FASTINT(LuauTypeMaximumStringifierLength) +LUAU_FASTFLAG(LuauToStringSimpleCompositeTypesSingleLine) namespace Luau { @@ -39,6 +40,12 @@ struct ToStringNameMap struct ToStringOptions { + ToStringOptions(bool exhaustive = false) + : exhaustive(exhaustive) + , compositeTypesSingleLineLimit(FFlag::LuauToStringSimpleCompositeTypesSingleLine ? 5 : 0) + { + } + bool exhaustive = false; // If true, we produce complete output rather than comprehensible output bool useLineBreaks = false; // If true, we insert new lines to separate long results such as table entries/metatable. bool functionTypeArguments = false; // If true, output function type argument names when they are available @@ -47,6 +54,7 @@ struct ToStringOptions bool hideFunctionSelfArgument = false; // If true, `self: X` will be omitted from the function signature if the function has self size_t maxTableLength = size_t(FInt::LuauTableTypeMaximumStringifierLength); // Only applied to TableTypes size_t maxTypeLength = size_t(FInt::LuauTypeMaximumStringifierLength); + size_t compositeTypesSingleLineLimit = 5; // The number of type elements permitted on a single line when printing type unions/intersections ToStringNameMap nameMap; std::shared_ptr scope; // If present, module names will be added and types that are not available in scope will be marked as 'invalid' std::vector namedFunctionOverrideArgNames; // If present, named function argument names will be overridden diff --git a/Analysis/src/ToString.cpp b/Analysis/src/ToString.cpp index 10fe440e..8123e09f 100644 --- a/Analysis/src/ToString.cpp +++ b/Analysis/src/ToString.cpp @@ -17,6 +17,7 @@ LUAU_FASTFLAG(DebugLuauDeferredConstraintResolution) LUAU_FASTFLAGVARIABLE(LuauToStringPrettifyLocation, false) +LUAU_FASTFLAGVARIABLE(LuauToStringSimpleCompositeTypesSingleLine, false) /* * Enables increasing levels of verbosity for Luau type names when stringifying. @@ -878,11 +879,15 @@ struct TypeStringifier state.emit("("); bool first = true; + bool shouldPlaceOnNewlines = results.size() > state.opts.compositeTypesSingleLineLimit; for (std::string& ss : results) { if (!first) { - state.newline(); + if (shouldPlaceOnNewlines) + state.newline(); + else + state.emit(" "); state.emit("| "); } state.emit(ss); @@ -902,7 +907,7 @@ struct TypeStringifier } } - void operator()(TypeId, const IntersectionType& uv) + void operator()(TypeId ty, const IntersectionType& uv) { if (state.hasSeen(&uv)) { @@ -938,11 +943,15 @@ struct TypeStringifier std::sort(results.begin(), results.end()); bool first = true; + bool shouldPlaceOnNewlines = results.size() > state.opts.compositeTypesSingleLineLimit || isOverloadedFunction(ty); for (std::string& ss : results) { if (!first) { - state.newline(); + if (shouldPlaceOnNewlines) + state.newline(); + else + state.emit(" "); state.emit("& "); } state.emit(ss); diff --git a/CLI/FileUtils.cpp b/CLI/FileUtils.cpp index 71e536c7..4ca657a9 100644 --- a/CLI/FileUtils.cpp +++ b/CLI/FileUtils.cpp @@ -165,11 +165,14 @@ static bool traverseDirectoryRec(const std::string& path, const std::functionglobal->totalbytes : L->global->memcatbytes[category]; } + +lua_Alloc lua_getallocf(lua_State* L, void** ud) +{ + lua_Alloc f = L->global->frealloc; + if (ud) + *ud = L->global->ud; + return f; +} diff --git a/papers/incorrectness24/bibliography.bib b/papers/incorrectness24/bibliography.bib new file mode 100644 index 00000000..a5724f6b --- /dev/null +++ b/papers/incorrectness24/bibliography.bib @@ -0,0 +1,122 @@ +@InProceedings{BFJ21:GoalsLuau, + author = {L. Brown and A. Friesen and A. S. A. Jeffrey}, + 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}, +} + +@Misc{Roblox, + author = {Roblox}, + title = {Reimagining the way people come together}, + year = 2023, + url = {https://corp.roblox.com}, +} + +@Misc{Luau, + author = {Roblox}, + title = {The {Luau} Programming Language}, + year = 2023, + url = {https://luau-lang.org}, +} + +@Misc{Lua, + author = {Lua.org and {PUC}-Rio}, + title = {The {Lua} Programming Language}, + year = 2023, + url = {https://lua.org}, +} + +@Misc{Jef22:SemanticSubtyping, + author = {A. S. A. Jeffrey}, + title = {Semantic Subtyping in Luau}, + howpublished = {Roblox Technical Blog}, + year = {2022}, + url = {https://blog.roblox.com/2022/11/semantic-subtyping-luau/}, +} + +@InProceedings{GF05:GentleIntroduction, + author = {G. Castagna and A. Frisch}, + title = {A Gentle Introduction to Semantic Subtyping}, + booktitle = {Proc. Principles and Practice of Declarative Programming}, + year = {2005}, +} + +@InProceedings{ST07:GradualTyping, + author = {J. G. Siek and W. Taha}, + title = {Gradual Typing for Objects}, + booktitle = {Proc. European Conf Object-Oriented Programming}, + year = {2007}, + pages = {2-27}, +} + +@Misc{BJ23:agda-typeck, + author = {L. Brown and A. S. A. Jeffrey}, + title = {Luau Prototype Typechecker}, + year = {2023}, + OPTnote = {}, + url = {https://github.com/luau-lang/agda-typeck} +} + +@article{PT00:LocalTypeInference, +author = {Pierce, B. C. and Turner, D. N.}, +title = {Local Type Inference}, +year = {2000}, +volume = {22}, +number = {1}, +journal = {ACM Trans. Program. Lang. Syst.}, +pages = {1–44}, +} + +@inproceedings{SuccessTyping, + author = {Lindahl, T. and Sagonas, K.}, + title = {Practical Type Inference Based on Success Typings}, + year = {2006}, + booktitle = {Proc. Int. Conf. Principles and Practice of Declarative Programming}, + pages = {167–178}, +} + +@InProceedings{Dialyzer, +author="Lindahl, T. and Sagonas, K.", +title="Detecting Software Defects in Telecom Applications Through Lightweight Static Analysis: A War Story", +booktitle="Proc. Asian Symp. Programming Languages and Systems", +year="2004", +pages="91--106", +} + +@Misc{NewNonStrictRFC, + author = {A. S. A. Jeffrey}, + title = {{RFC} For New Non-strict Mode}, + howpublished = {Luau Request For Comment}, + year = {2023}, + note = {\url{https://github.com/Roblox/luau/pull/1037}}, +} + +@Inbook{Nielson1999, +author="Nielson, F. +and Nielson, H. R.", +title="Type and Effect Systems", +bookTitle="Correct System Design: Recent Insights and Advances", +year="1999", +publisher="Springer", +pages="114--136", +isbn="978-3-540-48092-1", +} + +@Misc{DesignElixir, + author = {G. Castagna and G. Duboc and J. Valim}, + title = {The Design Principles of the {Elixir} Type System}, + year = {2023}, + note = {\url{https://doi.org/10.48550/arXiv.2306.06391}}, +} + +@article{BidirectionalTyping, +author = {Dunfield, J. and Krishnaswami, N.}, +title = {Bidirectional Typing}, +year = {2022}, +volume = {54}, +number = {5}, +journal = {ACM Comput. Surv.}, +articleno = {98}, +numpages = {38}, +} \ No newline at end of file diff --git a/papers/incorrectness24/cc-by.png b/papers/incorrectness24/cc-by.png new file mode 100644 index 00000000..c8473a24 Binary files /dev/null and b/papers/incorrectness24/cc-by.png differ diff --git a/papers/incorrectness24/incorrectness24.pdf b/papers/incorrectness24/incorrectness24.pdf new file mode 100644 index 00000000..006496d1 Binary files /dev/null and b/papers/incorrectness24/incorrectness24.pdf differ diff --git a/papers/incorrectness24/incorrectness24.tex b/papers/incorrectness24/incorrectness24.tex new file mode 100644 index 00000000..ed154002 --- /dev/null +++ b/papers/incorrectness24/incorrectness24.tex @@ -0,0 +1,366 @@ +\documentclass[sigplan]{acmart} + +\setcopyright{rightsretained} +\copyrightyear{2024} +\acmYear{2024} +\acmConference[Incorrectness '24]{Formal Methods for Incorrectness}{January 2024}{London, UK} +\acmBooktitle{Incorrectness '24: Formal Methods for Incorrectness} +\acmDOI{} +\acmISBN{} +\expandafter\def\csname @copyrightpermission\endcsname{\raisebox{-2ex}{\includegraphics[width=.2\linewidth]{cc-by}} \parbox{.7\linewidth}{\raggedright This work is licensed under a Creative Commons Attribution 4.0 International License.}} +\expandafter\def\csname @copyrightowner\endcsname{Roblox.} +\newcommand{\infer}[2]{\frac{\displaystyle\begin{array}{@{}l@{}}#1\end{array}}{\displaystyle#2}} +\newcommand{\LOCAL}{\mathop{\mathsf{local}}} +\newcommand{\FUNCTION}{\mathop{\mathsf{function}}} +\newcommand{\IF}{\mathop{\mathsf{if}}} +\newcommand{\THEN}{\mathbin{\mathsf{then}}} +\newcommand{\ELSE}{\mathbin{\mathsf{else}}} +\newcommand{\END}{\mathop{\mathsf{end}}} +\newcommand{\NEVER}{\mathsf{never}} +\newcommand{\ERROR}{\mathsf{error}} +\newcommand{\UNKNOWN}{\mathsf{unknown}} +\newcommand{\STRING}{\mathsf{string}} +\newcommand{\NUMBER}{\mathsf{number}} +\newcommand{\MATH}{\mathsf{math}} +\newcommand{\ABS}{\mathsf{abs}} +\newcommand{\LOWER}{\mathsf{lower}} +\newcommand{\fun}{\mathbin{\rightarrow}} + +\begin{document} + +\title{Towards an Unsound But Complete Type System} +\subtitle{Work In Progress on New Non-Strict Mode for Luau} + +\author{Lily Brown} +\author{Andy Friesen} +\author{Alan Jeffrey} +\author{Vighnesh Vijay} +\affiliation{ + \institution{Roblox} + \city{San Mateo} + \state{CA} + \country{USA} +} + +\begin{abstract} +In HATRA 2021, we presented \emph{The Goals Of The Luau Type System}, +describing the human factors of a type system for a language with a +heterogeneous developer community. One of the goals was the design of +type system for bug detection, where we have high confidence that type +errors identify genuine software defects, and that false positives are +minimized. Such a type system is, by necessity, unsound, but we can ask +instead that it is complete. This paper presents a work-in-progress report +on the design and implementation of the new unsound type system for Luau. +\end{abstract} + +\maketitle + +\section{Introduction} + +Luau~\cite{Luau} is the scripting language used by the +Roblox~\cite{Roblox} platform for shared immersive experiences. Luau extends +the Lua~\cite{Lua} language, notably by providing type-driven tooling +such as autocomplete and API documentation (as well as traditional type +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 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 +communities: beginners are focused on immediate goals (``the stairs +should light up when a player walks on them'') and less on the code +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, which + minimizes 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, which + minimizes false negatives (that is, in strict mode, any program with a defect has a type error). +\end{itemize} +The focus of this extended abstract is the design of non-strict mode: what constitutes +a defect, and how can we design a complete type system for detecting them. +(The words ``sound'' and ``complete'' in this sense are far from ideal, +but ``sound type system'' has a well-established meaning, and ``complete'' +is well-established as the dual of ``sound'', so here we are.) + +The closest work to ours is success typing~\cite{SuccessTyping}, used +in Erlang Dialyzer~\cite{Dialyzer}. The new feature of our work is +that strict and non-strict mode have to interact, whereas Dialyzer only has +the equivalent of non-strict mode. + +New non-strict mode is specified in a Luau Request For +Comment~\cite{NewNonStrictRFC}, and is currently being implemented. +We expect it (and other new type checking features) to be available in +2024. This extended abstract is based on the RFC, but written in +``Greek letters and horizontal lines'' rather than ``monospaced text''. + +\section{Code defects} + +The main goal of non-strict mode is to identify defects, but this requires +deciding what a defect is. Run-time errors are an obvious defect: +\begin{verbatim} + local hi = "hi" + print(math.abs(hi)) +\end{verbatim} +but we also want to catch common mistakes such as mis-spelling a property name, +even though Luau returns \verb|nil| for missing property accesses. +For this reason, we consider a larger class of defects: +\begin{itemize} +\item run-time errors, +\item expressions guaranteed to be \verb|nil|, and +\item writing to a table property that is never read. +\end{itemize} + +\subsection{Run-time errors} + +Run-time errors occur due to run-time type mismatches (such as \verb|5("hi")|) +or incorrect built-in function calls (such as \verb|math.abs("hi")|). +Precisely identifying run-time errors is undecidable, for example: +\begin{verbatim} + if cond() then + math.abs(“hi”) + end +\end{verbatim} +We cannot be sure that this code produces a run-time +error, but we do know that if \verb|math.abs("hi")| is executed, it +will produce an error, so we consider this to be a defect. + +\subsection{Expressions guaranteed to be nil} + +Luau tables do not error when a missing property is accessed (though embeddings may). So +\begin{verbatim} + local t = { Foo = 5 } + local x = t.Fop +\end{verbatim} +does not produce a run-time error, but is more likely than not a +programmer error. If the programmer intended to +initialize \verb|x| as \verb|nil|, they could have written +\verb|x = nil|. For this reason, we consider it a code defect to use +an expression that the type system infers is of type \verb|nil|, other +than the \verb|nil| literal. + +\subsection{Writing properties that are never read} + +There is a matching problem with misspelling properties when writing. For example +\begin{verbatim} + function f() + local t = {} + t.Foo = 5 + t.Fop = 7 + print(t.Foo) + end +\end{verbatim} +does not produce a run-time error, but is more likely than not a +programmer error, since \verb|t.Fop| is written but never read. We can use +read-only and write-only table properties types for this, and consider it an +code defect to create a write-only property. + +We have to be careful about this though, because if \verb|f| ended +with \verb|return t|, then it would be a perfectly sensible function +with type \verb|() -> { Foo: number, Fop: number }|. The only way to detect +that \verb|Fop| was never read would be whole-program analysis, which is +prohibitively expensive. + +\section{New Non-strict error reporting} + +The difficult part of non-strict mode error-reporting is predicting +run-time errors. We do this using an error-reporting +pass that synthesizes a type context $\Delta$ such that if any of the $x : T$ in +$\Delta$ are satisfied, then the program will +produce a type error. For example in the program +\begin{verbatim} + function h(x, y) + math.abs(x) + string.lower(y) + end +\end{verbatim} +an error is reported when \verb|x| isn’t a \verb|number|, or \verb|y| isn’t a \verb|string|, so the synthesized context is +\begin{verbatim} + x : ~number, y : ~string +\end{verbatim} +(\verb|~T| is Luau's concrete syntax for type negation.) +In: +\begin{verbatim} + function f(x) + math.abs(x) + string.lower(x) + end +\end{verbatim} +an error is reported when \verb|x| isn’t a \verb|number| or isn’t a \verb|string|, so the context is +\begin{verbatim} + x : ~number | ~string +\end{verbatim} +(\verb"T | U" is Luau's concrete syntax for type union.) +Since the type \verb"~number | ~string" is equivalent to the type \verb|unknown| (which contains every value), +non-strict mode can report a warning, since calling the function is guaranteed to throw a run-time error. +In contrast: +\begin{verbatim} + function g(x) + if cond() then + math.abs(x) + else + string.lower(x) + end + end +\end{verbatim} +synthesizes context +\begin{verbatim} + x : ~number & ~string +\end{verbatim} +(\verb|T & U| is Luau's concrete syntax for type intersection.) +Since \verb|~number & ~string| is not equivalent to \verb|unknown|, non-strict mode reports no warning. + +\begin{figure*} + \[\begin{array}{c} + \infer{ + \Gamma \vdash M : \NEVER \dashv \Delta_1 \\ + \Gamma, x : T \vdash B \dashv \Delta_2, x : U \\ + \mbox{(warn if $\UNKNOWN <: U$)} + }{ + \Gamma \vdash (\LOCAL x : T = M; B) \dashv (\Delta_1 \cup \Delta_2) + } + \quad + \infer{ + \Gamma \vdash M : \NEVER \dashv \Delta_1 \\ + \Gamma \vdash B \dashv \Delta_2 \\ + \Gamma \vdash C \dashv \Delta_3 + }{ + \Gamma \vdash (\IF M \THEN B \ELSE C \END) \dashv (\Delta_1 \cup (\Delta_2 \cap \Delta_3)) + } + \\[\bigskipamount] + \infer{}{ + \Gamma \vdash x : T \dashv (x : T) + } + \quad + \infer{ + \mbox{(warn if $k:T$)} + }{ + \Gamma \vdash k : T \dashv \emptyset + } + \quad + \infer{ + \Gamma, x:S \vdash B \dashv \Delta, x:U \\ + \mbox{(warn if $\UNKNOWN <: U$)}\\ + \mbox{(warn if ${\FUNCTION} <: T$)} + }{ + \Gamma \vdash (\FUNCTION (x : S) B \END) : T \dashv \Delta + } + \quad + \infer{ + \Gamma \vdash M : (S \fun \ERROR) \\ + \Gamma \vdash M : \neg{\FUNCTION} \dashv \Delta_1 \\ + \Gamma \vdash N : S \dashv \Delta_2 \\ + \mbox{(warn if $\Gamma \vdash M : (\UNKNOWN \fun (T \cup \ERROR))$)} + }{ + \Gamma \vdash M(N) : T \dashv \Delta_1 \cup \Delta_2 + } + \end{array}\] + \caption{Type context synthesis for blocks ($\Gamma \vdash B \dashv \Delta$) and expressions ($\Gamma \vdash M:T \dashv \Delta$)} + \label{fig:ctxtgen} +\end{figure*} + +\begin{figure*} + \[ + \infer{ + \begin{array}[b]{c} + \infer{}{\Gamma \vdash \MATH.\ABS : (\neg\NUMBER \fun \ERROR)} \\[\bigskipamount] + \infer{}{\Gamma \vdash \MATH.\ABS : \neg{\FUNCTION} \dashv \emptyset} + \end{array} + \infer{ + \Gamma \vdash \STRING.\LOWER : (\neg\STRING \fun \ERROR) \\ + \Gamma \vdash \STRING.\LOWER : \neg{\FUNCTION} \dashv \emptyset \\ + \Gamma \vdash x : \neg{\STRING} \dashv (x : \neg\STRING) \\ + \mbox{(warn since $\Gamma \vdash \STRING.\LOWER : \UNKNOWN \fun (\neg\NUMBER \cup \ERROR)$)} + }{\Gamma \vdash \STRING.\LOWER(x) : \neg{\NUMBER} \dashv (x : \neg\STRING)} + }{\Gamma \vdash (\MATH.\ABS(\STRING.\LOWER(x)) : \NEVER \dashv (x : \neg\STRING)} + \] + \caption{Example warning} + \label{fig:example} +\end{figure*} + +In Figure~\ref{fig:ctxtgen} we provide some of the inference rules for +context synthesis, and the warnings that it +produces. These are run after type inference, so they can assume that +all code is fully typed. + +In the judgment $\Gamma \vdash M : T \dashv +\Delta$, the type context $\Gamma$ is the usual \emph{checked} type +context and $\Delta$ is the \emph{synthesized} context used to predict +run-time errors (following the terminology of bidirectional +typing~\cite{BidirectionalTyping}). + +\begin{conjecture}\label{conj:complete}% +If $\Gamma \vdash M : T \dashv \Delta, x:U$ and $\sigma$ is a closing +substitution where $\sigma(x) : U$ and $M[\sigma] \rightarrow^* v$, +then $v : T$. +\end{conjecture} + +\begin{corollary}\label{cor:complete}% +If $\Gamma \vdash M : \NEVER \dashv \Delta, x:\UNKNOWN$ and $\sigma$ is a closing +substitution, then $M[\sigma]$ does not terminate successfully. +\end{corollary} + +\section{Checked functions} + +The crucial aspect of this type system is that we have a type $\ERROR$ +inhabited by no values, and by expressions which may throw a run-time exception. +(This is essentially a very simple type and effect system~\cite{Nielson1999} +with one effect.) + +The rule for function application $M(N)$ +has two dependencies on the type for $M$: +\[\begin{array}{c} + \Gamma \vdash M : (S \fun \ERROR) + \\[\jot] + \Gamma \vdash M : (\UNKNOWN \fun (T \cup \ERROR)) +\end{array}\] +Since Luau is based on semantic subtyping~\cite{GF05:GentleIntroduction,Jef22:SemanticSubtyping} and supports +intersection types, this is equivalent to asking for $M$ to be an +overloaded function, where one overload has argument type $\UNKNOWN$, and +one has result type $\ERROR$. For example: +\[ + \MATH.\ABS : (\NUMBER \fun \NUMBER) \cap (\neg\NUMBER \fun \ERROR) +\] +and so (by subsumption): +\[\begin{array}{c} + \MATH.\ABS : (\neg\NUMBER \fun \ERROR) + \\[\jot] + \MATH.\ABS : (\UNKNOWN \fun (\NUMBER \cup \ERROR)) +\end{array}\] +This is a common enough idiom it is worth naming it: +we call any function of type +\[ + (S \fun T) \cap (\neg S \fun \ERROR) +\] +a \emph{checked} function, since it performs a run-time check +on its argument. They are called \emph{strong arrows} +in Elixir~\cite{DesignElixir}. + +Note that this type system has the usual subtyping rule for +functions: contravariant in their argument type, and +covariant in their result type. In contrast, checked functions +are invariant in their argument type, since one overload +$S \fun T$ is contravariant in $S$, and the other $\neg S \fun \ERROR$ +is covariant. + +This system is also different from success +typings~\cite{SuccessTyping}, which has functions +$(\neg S \fun \ERROR) \cap (\UNKNOWN \fun (T \cup \ERROR))$, +in our system, which are covariant in both $S$ and $T$. + +\section{Future work} + +This type system is still in the design phase~\cite{NewNonStrictRFC}, though we hope +the implementation will be ready by the end of 2023. This will include +testing the implementation on our unit tests, and on large code bases. + +There is an Agda development of a core of strict mode~\cite{BJ23:agda-typeck}. It +should extend to non-strict mode, at which point +Conjecture~\ref{conj:complete} (or something like it) +will be mechanically verified. + +\bibliographystyle{ACM-Reference-Format} \bibliography{bibliography} + +\end{document} diff --git a/rfcs/STATUS.md b/rfcs/STATUS.md index 41d69f01..653f168f 100644 --- a/rfcs/STATUS.md +++ b/rfcs/STATUS.md @@ -1,19 +1,5 @@ This document tracks unimplemented RFCs. -## Deprecate getfenv/setfenv - -[RFC: Deprecate getfenv/setfenv](https://github.com/Roblox/luau/blob/master/rfcs/deprecate-getfenv-setfenv.md) - -**Status**: Needs implementation. - -**Notes**: Implementing this RFC triggers warnings across the board in the apps ecosystem, in particular in testing libraries. Pending code changes / decisions. - -## Deprecate table.getn/foreach/foreachi - -[RFC: Deprecate table.getn/foreach/foreachi](https://github.com/Roblox/luau/blob/master/rfcs/deprecate-table-getn-foreach.md) - -**Status**: Needs implementation. - ## Read-only and write-only properties [RFC: Read-only properties](https://github.com/Roblox/luau/blob/master/rfcs/property-readonly.md) | diff --git a/rfcs/deprecate-getfenv-setfenv.md b/rfcs/deprecate-getfenv-setfenv.md index e5af1730..9e80f9c6 100644 --- a/rfcs/deprecate-getfenv-setfenv.md +++ b/rfcs/deprecate-getfenv-setfenv.md @@ -1,5 +1,7 @@ # Deprecate getfenv/setfenv +**Status**: Implemented + ## Summary Mark getfenv/setfenv as deprecated diff --git a/rfcs/deprecate-table-getn-foreach.md b/rfcs/deprecate-table-getn-foreach.md index c6c889dc..ea8e1e6b 100644 --- a/rfcs/deprecate-table-getn-foreach.md +++ b/rfcs/deprecate-table-getn-foreach.md @@ -1,5 +1,7 @@ # Deprecate table.getn/foreach/foreachi +**Status**: Implemented + ## Summary Mark table.getn/foreach/foreachi as deprecated diff --git a/rfcs/new-nonstrict.md b/rfcs/new-nonstrict.md new file mode 100644 index 00000000..42e9cc6f --- /dev/null +++ b/rfcs/new-nonstrict.md @@ -0,0 +1,340 @@ +# New non-strict mode + +## Summary + +Currently, strict mode and non-strict mode infer different types for +the same program. With this feature, strict and non-strict modes will +share the [local type inference](local-type-inference.md) +engine, and the only difference between the modes will be in which +errors are reported. + +## Motivation + +Having two different type inference engines is unnecessarily +confusing, and can result in unexpected behaviors such as changing the +mode of a module can cause errors in the users of that module. + +The current non-strict mode infers very coarse types (e.g. all local +variables have type `any`) and so is not appropriate for type-driven +tooling, which results in expensively and inconsistently using +different modes for different tools. + +## Design + +### Code defects + +The main goal of non-strict mode is to minimize false positives, that +is if non-strict mode reports an error, then we have high confidence +that there is a code defect. Example defects are: + +* Run-time errors +* Dead code +* Using an expression whose only possible value is `nil` +* Writing to a table property that is never read + +*Run-time errors*: this is an obvious defect. Examples include: + +* Built-in operators (`"hi" + 5`) +* Luau APIs (`math.abs("hi")`) +* Function calls from embeddings (`CFrame.new("hi")`) +* Missing properties from embeddings (`CFrame.new().nope`) + +Detecting run-time errors is undecidable, for example + +```lua +if cond() then + math.abs(“hi”) +end +``` + +It is undecidable whether this code produces a run-time error, but we +do know that if `math.abs("hi")` is executed, it will produce a +run-time error, and so report a type error in this case. + +*Expressions guaranteed to be `nil`*: Luau tables do not error when a +missing property is accessed (though embeddings may). So something +like + +```lua +local t = { Foo = 5 } +local x = t.Fop +``` + +won’t produce a run-time error, but is more likely than not a +programmer error. In this case, if the programmer intent was to +initialize `x` as `nil`, they could have written + +```lua +local t = { Foo = 5 } +local x = nil +``` + +For this reason, we consider it a code defect to use a value that the +type system guarantees is of type `nil`. + +*Writing properties that are never read*: There is a matching problem +with misspelling properties when writing. For example + +```lua +function f() + local t = {} + t.Foo = 5 + t.Fop = 7 + print(t.Foo) +end +``` + +won’t produce a run-time error, but is more likely than not a +programmer error, since `t.Fop` is written but never read. We can use +read-only and write-only table properties for this, and make it an +error to create a write-only property. + +We have to be careful about this though, because if `f` ended with +`return t`, then it would be a perfectly sensible function with type +`() -> { Foo: number, Fop: number }`. The only way to detect that `Fop` +was never read would be whole-program analysis, which is prohibitively +expensive. + +*Implicit coercions*: Luau supports various implicit coercions, such +as allowing `math.abs("-12")`. These should be reported as defects. + +### New Non-strict error reporting + +The difficult part of non-strict mode error-reporting is detecting +guaranteed run-time errors. We can do this using an error-reporting +pass that generates a type context such that if any of the `x : T` in +the type context are satisfied, then the program is guaranteed to +produce a type error. + +For example in the program + +```lua +function h(x, y) + math.abs(x) + string.lower(y) +end +``` + +an error is reported when `x` isn’t a `number`, or `y` isn’t a `string`, so the generated context is + +``` +x : ~number +y : ~string +``` + +In the function: + +```lua +function f(x) + math.abs(x) + string.lower(x) +end +``` + +an error is reported when x isn’t a number or isn’t a string, so the constraint set is + +``` +x : ~number | ~string +``` + +Since `~number | ~string` is equivalent to `unknown`, non-strict mode +can report a warning, since calling the function is guaranteed to +throw a run-time error. In contrast: + +```lua +function g(x) + if cond() then + math.abs(x) + else + string.lower(x) + end +end +``` + +generates context + +``` +x : ~number & ~string +``` + +Since `~number & ~string` is not equivalent to `unknown`, non-strict mode reports no warning. + +* The disjunction of contexts `C1` and `C2` contains `x : T1|T2`, + where `x : T1` is in `C1` and `x : T2` is in `C2`. +* The conjunction of contexts `C1` and `C2` contains `x : T1&T2`, + where `x : T1` is in `C1` and `x : T2` is in `C2`. + +The context generated by a block is: + +* `x = E` generates the context of `E : never`. +* `B1; B2` generates the disjunction of the context of `B1` and the + context of `B2`. +* `if C then B1 else B2` end generates the conjunction of the context + of `B1` and the context of `B2`. +* `local x; B` generates the context of `B`, removing the constraint + `x : T`. If the type inferred for `x` is a subtype of `T`, then + issue a warning. +* `function f(x1,...,xN) B end` generates the context for `B`, + removing `x1 : T1, ..., xN : TN`. If any of the `Ti` are equivalent to + `unknown`, then issue a warning. + +The constraint set generated by a typed expression is: + +* The context generated by `x : T` is `x : T`. +* The context generated by `s : T` (where `s` is a scalar) is + trivial. Issue a warning if `s` has type `T`. +* The context generated by `F(M1, ..., MN) : T` is the disjunction of + the contexts generated by `F : ~function`, and by + `M1 : T1`, ...,`MN : TN` where for each `i`, `F` has an overload + `(unknown^(i-1),Ti,unknown^(N-i)) -> error`. (Pick `Ti` to be + `never` if no such overload exists). Issue a warning if `F` has an + overload `(unknown^N) -> S` where `S <: (T | error)`. +* The context generated by `M.p` is the context generated by `M : ~table`. +* The context generated by `M[N]` is the disjunction of the contexts + generated by `M : ~table` and `N : never`. + +For example: + +* The context generated by `math.abs("hi") : never` is + * the context generated by `"hi" : ~number`, since `math.abs` has an + overload `(~number) -> error`, which is trivial. + * A warning is issued since `"hi"` has type `~number`. +* The context generated by `function f(x) math.abs(x); string.lower(x) end` is + * the context generated by `math.abs(x); string.lower(x)` which is the disjunction of + * the context generated by `math.abs(x)`, which is + * the context `x : ~number`, since `math.abs` has an overload `(~number)->error` + * the context generated by `string.lower(x)`, which is + * the context `x : ~string`, since `string.lower` has an overload `(~string)->error` + * remove the binding `x : (~number | ~string)` + * A warning is issued since `(~number | ~string)` is equivalent to `unknown`. +* The context generated by `math.abs(string.lower(x))` is + * the context generated by `string.lower(x) : ~number`, since `math.abs` has an overload `(~number)->error`, which is + * the text`x : ~string`, since `string.lower` has an overload `(~string)->error`. + * An warning is issued, since `string.lower` has an overload `(unknown) -> (string | error)` and `(string | error) <: (~number | error)`. + +### Ergonomics + +*Error reporting*. A straightforward implementation of this design +issues warnings at the point that data flows into a place +guaranteed to later produce a run-time error, which may not be perfect +ergonomics. For example, in the program: + +```lua +local x +if cond() then + x = 5 +else + x = nil +end +string.lower(x) +``` + +the type inferred for `x` is `number?` and the context generated is `x +: ~string`. Since `number? <: ~string`, a warning is issued at the +declaration `local x`. For ergonomics, we might want to identify +either `string.lower(x)` or `x = 5` (or both!) in the error report. + +*Stringifying checked functions*. This design depends on functions +having overloads with `error` return type. This integrates with +[type error suppression](type-error-suppression.md), but would not be +a perfect way to present types to users. A common case is that the +checked type is the negation of the function type, for example the +type of `math.abs`: + +``` +(number) -> number & (~number) -> error +``` + +This might be better presented as an annotation on the argument type, something like: + +``` +@checked (number) -> number +``` + +The type + +``` + @checked (S1,...,SN) -> T +``` + +is equivalent to + + +``` + (S1,...,SN) -> T + & (~S1, unknown^N-1) -> error + & (unknown, ~S2, unknown^N-2) -> error + ... + & (unknown^N-1, SN) -> error +``` + +As a further extension, we might allow users to explicitly provide `@checked` type annotations. + +Checked functions are known as strong functions in Elixir. + +## Drawbacks + +This is a breaking change, since it results in more errors being issued. + +Strict mode infers more precise (and hence more complex) types than +current non-strict mode, which are presented by type error messages +and tools such as type hover. + +## Alternatives + +Success typing (used in Erlang Dialyzer) is the nearest existing +solution. It is similar to this design, except that it only works in +(the equivalent of) non-strict mode. The success typing function type +`(S)->T` is the equivalent of our +`(~S)->error & (unknown)->(T|error)`. + +We could put the `@checked` annotation on individual function argments +rather than the function type. + +We could use this design to infer checked functions. In function +`f(x1, ..., xN) B end`, we could generate the context +`(x1 : T1, ..., xN : TN)` for `B`, and add an overload +`(unknown^(i-1),Ti,unknown^(N-i))->error` to the inferred type of `f`. For +example, for the function + +```lua +function h(x, y) + math.abs(x) + string.lower(y) +end +``` + +We would infer type + +``` + (number, string) -> () +& (~number, unknown) -> error +& (unknown, ~string) -> error +``` + +which is the same as + +``` + @checked (number, string) -> () +``` + +The problem with doing this is what to do about recursive functions. + +## References + +Lily Brown, Andy Friesen and Alan Jeffrey +*Position Paper: Goals of the Luau Type System*, +in HATRA '21: Human Aspects of Types and Reasoning Assistants, +2021. +https://doi.org/10.48550/arXiv.2109.11397 + +Giuseppe Castagna, Guillaume Duboc, José Valim +*The Design Principles of the Elixir Type System*, +2023. +https://doi.org/10.48550/arXiv.2306.06391 + +Tobias Lindahl and Konstantinos Sagonas, +*Practical Type Inference Based on Success Typings*, +in PPDP '06: Principles and Practice of Declarative Programming, +pp. 167–178, 2006. +https://doi.org/10.1145/1140335.1140356 diff --git a/rfcs/syntax-string-interpolation.md b/rfcs/syntax-string-interpolation.md index 2fbb04b0..b2b9b0ea 100644 --- a/rfcs/syntax-string-interpolation.md +++ b/rfcs/syntax-string-interpolation.md @@ -1,5 +1,7 @@ # String interpolation +**Status**: Implemented + ## Summary New string interpolation syntax. diff --git a/tests/Conformance.test.cpp b/tests/Conformance.test.cpp index 1e520100..a023840b 100644 --- a/tests/Conformance.test.cpp +++ b/tests/Conformance.test.cpp @@ -1163,6 +1163,18 @@ TEST_CASE("ApiType") CHECK(lua_type(L, -1) == LUA_TUSERDATA); } +TEST_CASE("AllocApi") +{ + int ud = 0; + StateRef globalState(lua_newstate(limitedRealloc, &ud), lua_close); + lua_State* L = globalState.get(); + + void* udCheck = nullptr; + bool allocfIsSet = lua_getallocf(L, &udCheck) == limitedRealloc; + CHECK(allocfIsSet); + CHECK(udCheck == &ud); +} + #if !LUA_USE_LONGJMP TEST_CASE("ExceptionObject") { diff --git a/tests/ToString.test.cpp b/tests/ToString.test.cpp index 06fc1b8f..32e10709 100644 --- a/tests/ToString.test.cpp +++ b/tests/ToString.test.cpp @@ -234,8 +234,41 @@ TEST_CASE_FIXTURE(Fixture, "functions_are_always_parenthesized_in_unions_or_inte CHECK_EQ(toString(&itv), "((number, string) -> (string, number)) & ((string, number) -> (number, string))"); } -TEST_CASE_FIXTURE(Fixture, "intersections_respects_use_line_breaks") +TEST_CASE_FIXTURE(Fixture, "simple_intersections_printed_on_one_line") { + ScopedFastFlag sff{"LuauToStringSimpleCompositeTypesSingleLine", true}; + CheckResult result = check(R"( + local a: string & number + )"); + + ToStringOptions opts; + opts.useLineBreaks = true; + + CHECK_EQ("number & string", toString(requireType("a"), opts)); +} + +TEST_CASE_FIXTURE(Fixture, "complex_intersections_printed_on_multiple_lines") +{ + ScopedFastFlag sff{"LuauToStringSimpleCompositeTypesSingleLine", true}; + CheckResult result = check(R"( + local a: string & number & boolean + )"); + + ToStringOptions opts; + opts.useLineBreaks = true; + opts.compositeTypesSingleLineLimit = 2; + + //clang-format off + CHECK_EQ("boolean\n" + "& number\n" + "& string", + toString(requireType("a"), opts)); + //clang-format on +} + +TEST_CASE_FIXTURE(Fixture, "overloaded_functions_always_printed_on_multiple_lines") +{ + ScopedFastFlag sff{"LuauToStringSimpleCompositeTypesSingleLine", true}; CheckResult result = check(R"( local a: ((string) -> string) & ((number) -> number) )"); @@ -250,13 +283,28 @@ TEST_CASE_FIXTURE(Fixture, "intersections_respects_use_line_breaks") //clang-format on } -TEST_CASE_FIXTURE(Fixture, "unions_respects_use_line_breaks") +TEST_CASE_FIXTURE(Fixture, "simple_unions_printed_on_one_line") { + ScopedFastFlag sff{"LuauToStringSimpleCompositeTypesSingleLine", true}; + CheckResult result = check(R"( + local a: number | boolean + )"); + + ToStringOptions opts; + opts.useLineBreaks = true; + + CHECK_EQ("boolean | number", toString(requireType("a"), opts)); +} + +TEST_CASE_FIXTURE(Fixture, "complex_unions_printed_on_multiple_lines") +{ + ScopedFastFlag sff{"LuauToStringSimpleCompositeTypesSingleLine", true}; CheckResult result = check(R"( local a: string | number | boolean )"); ToStringOptions opts; + opts.compositeTypesSingleLineLimit = 2; opts.useLineBreaks = true; //clang-format off