\documentclass[acmsmall]{acmart}

\setcopyright{rightsretained}
\copyrightyear{2023}
\acmYear{2023}
\acmConference[HATRA '23]{Human Aspects of Types and Reasoning Assistants}{October 2023}{Portugal, Spain}
\acmBooktitle{HATRA '23: Human Aspects of Types and Reasoning Assistants}
\acmDOI{}
\acmISBN{}
\expandafter\def\csname @copyrightpermission\endcsname{\raisebox{-1ex}{\includegraphics[height=3.5ex]{cc-by}} This work is licensed under a Creative Commons Attribution 4.0 International License.}
\expandafter\def\csname @copyrightowner\endcsname{Roblox.}

\newcommand{\ANY}{\mathtt{any}}
\newcommand{\ERROR}{\mathtt{error}}

\begin{document}

\title{Goals of the Luau Type System, Two Years On}

\author{Lily Brown}
\author{Andy Friesen}
\author{Alan Jeffrey}
\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 issues with designing a type system for a
language with a heterogeneous developer community. In this extended
abstract we provide a progress report on how the design is being
delivered.
\end{abstract}

\maketitle

\section{Recap}

Luau~\cite{Luau} is the scripting language used by the
Roblox~\cite{Roblox} platform for shared 3D 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 \emph{The 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, focused on
  minimizing false positives, and
\item \emph{strict mode}, aimed at professionals, focused on
  minimizing false negatives (i.e.~type soundness).
\end{itemize}
For both communities, type-driven tooling is important, so we
provide \emph{infallible type inference}, which infers types no matter 
the inputs.

\section{New stuff}

The main improvement is that Luau now has support for \emph{semantic
subtyping}~\cite{Jef22:SemanticSubtyping}. Semantic subtyping
interprets types as sets of values, and subtyping as set
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.

The other big improvement is how we view gradual typing, Rather than
the approach of~\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}.

\section{Further work}

Currently the type inference system uses greedy inference, which is
very sensitive to order of declarations, and can easily result in
false positives. This needs replaced by some form of local type
inference~\cite{PT00:LocalTypeInference}.

Currently, non-strict mode operates in the style of gradual type
systems by inferring $\ANY$ as the type for local variables. This does
not play well with type-directed tooling, for example $\ANY$ cannot
provide autocomplete suggestions. We plan to improve non-strict mode's
type inference and interaction with error-suppression.

\bibliographystyle{ACM-Reference-Format} \bibliography{bibliography}

\end{document}