mirror of
https://github.com/luau-lang/luau.git
synced 2025-03-03 18:51:42 +00:00
Merge remote-tracking branch 'origin/master' into merge
This commit is contained in:
Lily Brown
commit
4d2be9727e
16 changed files with 936 additions and 26 deletions
|
|
@ -11,6 +11,7 @@
|
||||||
|
|
||||||
LUAU_FASTINT(LuauTableTypeMaximumStringifierLength)
|
LUAU_FASTINT(LuauTableTypeMaximumStringifierLength)
|
||||||
LUAU_FASTINT(LuauTypeMaximumStringifierLength)
|
LUAU_FASTINT(LuauTypeMaximumStringifierLength)
|
||||||
|
LUAU_FASTFLAG(LuauToStringSimpleCompositeTypesSingleLine)
|
||||||
|
|
||||||
namespace Luau
|
namespace Luau
|
||||||
{
|
{
|
||||||
|
|
@ -39,6 +40,12 @@ struct ToStringNameMap
|
||||||
|
|
||||||
struct ToStringOptions
|
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 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 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
|
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
|
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 maxTableLength = size_t(FInt::LuauTableTypeMaximumStringifierLength); // Only applied to TableTypes
|
||||||
size_t maxTypeLength = size_t(FInt::LuauTypeMaximumStringifierLength);
|
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;
|
ToStringNameMap nameMap;
|
||||||
std::shared_ptr<Scope> scope; // If present, module names will be added and types that are not available in scope will be marked as 'invalid'
|
std::shared_ptr<Scope> scope; // If present, module names will be added and types that are not available in scope will be marked as 'invalid'
|
||||||
std::vector<std::string> namedFunctionOverrideArgNames; // If present, named function argument names will be overridden
|
std::vector<std::string> namedFunctionOverrideArgNames; // If present, named function argument names will be overridden
|
||||||
|
|
|
||||||
|
|
@ -17,6 +17,7 @@
|
||||||
|
|
||||||
LUAU_FASTFLAG(DebugLuauDeferredConstraintResolution)
|
LUAU_FASTFLAG(DebugLuauDeferredConstraintResolution)
|
||||||
LUAU_FASTFLAGVARIABLE(LuauToStringPrettifyLocation, false)
|
LUAU_FASTFLAGVARIABLE(LuauToStringPrettifyLocation, false)
|
||||||
|
LUAU_FASTFLAGVARIABLE(LuauToStringSimpleCompositeTypesSingleLine, false)
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* Enables increasing levels of verbosity for Luau type names when stringifying.
|
* Enables increasing levels of verbosity for Luau type names when stringifying.
|
||||||
|
|
@ -878,11 +879,15 @@ struct TypeStringifier
|
||||||
state.emit("(");
|
state.emit("(");
|
||||||
|
|
||||||
bool first = true;
|
bool first = true;
|
||||||
|
bool shouldPlaceOnNewlines = results.size() > state.opts.compositeTypesSingleLineLimit;
|
||||||
for (std::string& ss : results)
|
for (std::string& ss : results)
|
||||||
{
|
{
|
||||||
if (!first)
|
if (!first)
|
||||||
{
|
{
|
||||||
|
if (shouldPlaceOnNewlines)
|
||||||
state.newline();
|
state.newline();
|
||||||
|
else
|
||||||
|
state.emit(" ");
|
||||||
state.emit("| ");
|
state.emit("| ");
|
||||||
}
|
}
|
||||||
state.emit(ss);
|
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))
|
if (state.hasSeen(&uv))
|
||||||
{
|
{
|
||||||
|
|
@ -938,11 +943,15 @@ struct TypeStringifier
|
||||||
std::sort(results.begin(), results.end());
|
std::sort(results.begin(), results.end());
|
||||||
|
|
||||||
bool first = true;
|
bool first = true;
|
||||||
|
bool shouldPlaceOnNewlines = results.size() > state.opts.compositeTypesSingleLineLimit || isOverloadedFunction(ty);
|
||||||
for (std::string& ss : results)
|
for (std::string& ss : results)
|
||||||
{
|
{
|
||||||
if (!first)
|
if (!first)
|
||||||
{
|
{
|
||||||
|
if (shouldPlaceOnNewlines)
|
||||||
state.newline();
|
state.newline();
|
||||||
|
else
|
||||||
|
state.emit(" ");
|
||||||
state.emit("& ");
|
state.emit("& ");
|
||||||
}
|
}
|
||||||
state.emit(ss);
|
state.emit(ss);
|
||||||
|
|
|
||||||
|
|
@ -165,11 +165,14 @@ static bool traverseDirectoryRec(const std::string& path, const std::function<vo
|
||||||
{
|
{
|
||||||
joinPaths(buf, path.c_str(), data.d_name);
|
joinPaths(buf, path.c_str(), data.d_name);
|
||||||
|
|
||||||
int type = data.d_type;
|
#if defined(DTTOIF)
|
||||||
int mode = -1;
|
mode_t mode = DTTOIF(data.d_type);
|
||||||
|
#else
|
||||||
|
mode_t mode = 0;
|
||||||
|
#endif
|
||||||
|
|
||||||
// we need to stat DT_UNKNOWN to be able to tell the type
|
// we need to stat an UNKNOWN to be able to tell the type
|
||||||
if (type == DT_UNKNOWN)
|
if ((mode & S_IFMT) == 0)
|
||||||
{
|
{
|
||||||
struct stat st = {};
|
struct stat st = {};
|
||||||
#ifdef _ATFILE_SOURCE
|
#ifdef _ATFILE_SOURCE
|
||||||
|
|
@ -181,15 +184,15 @@ static bool traverseDirectoryRec(const std::string& path, const std::function<vo
|
||||||
mode = st.st_mode;
|
mode = st.st_mode;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (type == DT_DIR || mode == S_IFDIR)
|
if (mode == S_IFDIR)
|
||||||
{
|
{
|
||||||
traverseDirectoryRec(buf, callback);
|
traverseDirectoryRec(buf, callback);
|
||||||
}
|
}
|
||||||
else if (type == DT_REG || mode == S_IFREG)
|
else if (mode == S_IFREG)
|
||||||
{
|
{
|
||||||
callback(buf);
|
callback(buf);
|
||||||
}
|
}
|
||||||
else if (type == DT_LNK || mode == S_IFLNK)
|
else if (mode == S_IFLNK)
|
||||||
{
|
{
|
||||||
// Skip symbolic links to avoid handling cycles
|
// Skip symbolic links to avoid handling cycles
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -323,6 +323,8 @@ LUA_API void lua_clonefunction(lua_State* L, int idx);
|
||||||
|
|
||||||
LUA_API void lua_cleartable(lua_State* L, int idx);
|
LUA_API void lua_cleartable(lua_State* L, int idx);
|
||||||
|
|
||||||
|
LUA_API lua_Alloc lua_getallocf(lua_State* L, void** ud);
|
||||||
|
|
||||||
/*
|
/*
|
||||||
** reference system, can be used to pin objects
|
** reference system, can be used to pin objects
|
||||||
*/
|
*/
|
||||||
|
|
|
||||||
|
|
@ -1432,3 +1432,11 @@ size_t lua_totalbytes(lua_State* L, int category)
|
||||||
api_check(L, category < LUA_MEMORY_CATEGORIES);
|
api_check(L, category < LUA_MEMORY_CATEGORIES);
|
||||||
return category < 0 ? L->global->totalbytes : L->global->memcatbytes[category];
|
return category < 0 ? L->global->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;
|
||||||
|
}
|
||||||
|
|
|
||||||
122
papers/incorrectness24/bibliography.bib
Normal file
122
papers/incorrectness24/bibliography.bib
Normal file
|
|
@ -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},
|
||||||
|
}
|
||||||
BIN
papers/incorrectness24/cc-by.png
Normal file
BIN
papers/incorrectness24/cc-by.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 12 KiB |
BIN
papers/incorrectness24/incorrectness24.pdf
Normal file
BIN
papers/incorrectness24/incorrectness24.pdf
Normal file
Binary file not shown.
366
papers/incorrectness24/incorrectness24.tex
Normal file
366
papers/incorrectness24/incorrectness24.tex
Normal file
|
|
@ -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}
|
||||||
|
|
@ -1,19 +1,5 @@
|
||||||
This document tracks unimplemented RFCs.
|
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
|
## Read-only and write-only properties
|
||||||
|
|
||||||
[RFC: Read-only properties](https://github.com/Roblox/luau/blob/master/rfcs/property-readonly.md) |
|
[RFC: Read-only properties](https://github.com/Roblox/luau/blob/master/rfcs/property-readonly.md) |
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,7 @@
|
||||||
# Deprecate getfenv/setfenv
|
# Deprecate getfenv/setfenv
|
||||||
|
|
||||||
|
**Status**: Implemented
|
||||||
|
|
||||||
## Summary
|
## Summary
|
||||||
|
|
||||||
Mark getfenv/setfenv as deprecated
|
Mark getfenv/setfenv as deprecated
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,7 @@
|
||||||
# Deprecate table.getn/foreach/foreachi
|
# Deprecate table.getn/foreach/foreachi
|
||||||
|
|
||||||
|
**Status**: Implemented
|
||||||
|
|
||||||
## Summary
|
## Summary
|
||||||
|
|
||||||
Mark table.getn/foreach/foreachi as deprecated
|
Mark table.getn/foreach/foreachi as deprecated
|
||||||
|
|
|
||||||
340
rfcs/new-nonstrict.md
Normal file
340
rfcs/new-nonstrict.md
Normal file
|
|
@ -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
|
||||||
|
|
@ -1,5 +1,7 @@
|
||||||
# String interpolation
|
# String interpolation
|
||||||
|
|
||||||
|
**Status**: Implemented
|
||||||
|
|
||||||
## Summary
|
## Summary
|
||||||
|
|
||||||
New string interpolation syntax.
|
New string interpolation syntax.
|
||||||
|
|
|
||||||
|
|
@ -1163,6 +1163,18 @@ TEST_CASE("ApiType")
|
||||||
CHECK(lua_type(L, -1) == LUA_TUSERDATA);
|
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
|
#if !LUA_USE_LONGJMP
|
||||||
TEST_CASE("ExceptionObject")
|
TEST_CASE("ExceptionObject")
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -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))");
|
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"(
|
CheckResult result = check(R"(
|
||||||
local a: ((string) -> string) & ((number) -> number)
|
local a: ((string) -> string) & ((number) -> number)
|
||||||
)");
|
)");
|
||||||
|
|
@ -250,13 +283,28 @@ TEST_CASE_FIXTURE(Fixture, "intersections_respects_use_line_breaks")
|
||||||
//clang-format on
|
//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"(
|
CheckResult result = check(R"(
|
||||||
local a: string | number | boolean
|
local a: string | number | boolean
|
||||||
)");
|
)");
|
||||||
|
|
||||||
ToStringOptions opts;
|
ToStringOptions opts;
|
||||||
|
opts.compositeTypesSingleLineLimit = 2;
|
||||||
opts.useLineBreaks = true;
|
opts.useLineBreaks = true;
|
||||||
|
|
||||||
//clang-format off
|
//clang-format off
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue