luau/papers/hatra23/hatra23.tex

\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}}
\newcommand{\NUMBER}{\mathtt{number}}

\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 of a type system for a
language with a heterogeneous developer community. In this extended
abstract we provide a progress report, focusing on
the unexpected aspects: semantic subtyping and type error
suppression.
\end{abstract}

\maketitle

\section{Recap}

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, focused on
  minimizing false positives (that is, in non-strict mode, any program with a type error has a defect), and
\item \emph{strict mode}, aimed at professionals, focused on
  minimizing false negatives (that is, in strict mode, any program with a defect has a type error).
\end{itemize}
%% For both communities, type-driven tooling is important, so we
%% provide \emph{infallible type inference}, which infers types
%% even for ill-typed or syntactically invalid programs.

\section{Progress}

In the two years since the position paper, we have been making changes
to the Luau type system to achieve the goals we set out. Most of the
changes were straightforward, but two were large changes in how we
thought about the design of the type system: replacing the existing
syntactic subtyping algorithm by \emph{semantic subtyping}, and
treating gradual typing as \emph{type error suppression}.

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.
For example, the program:
\begin{verbatim}
  local x : CFrame = CFrame.new()
  local y : Vector3 | CFrame
  if math.random() < 0.5 then y = CFrame.new() else y = Vector3.new() end
  local z : Vector3 | CFrame = x * y
\end{verbatim}
cannot produce a run-time error, since multiplication of \verb|CFrame|s is overloaded:
\begin{verbatim}
  ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)
\end{verbatim}
In order to typecheck this program, we check that that type is a subtype of:
\begin{verbatim}
  (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame)
\end{verbatim}
In the previous, syntax-driven, implementation of subtyping, this subtype check  would fail, resulting in a false positive.
We have now released an implementation of semantic subtyping, which does not suffer from this defect.
See our technical blog for more details~\cite{Jef22:SemanticSubtyping}.

Rather than the gradual typing approach
of Siek and Taha~\cite{ST07:GradualTyping}, which uses \emph{consistent
subtyping} where $\ANY \lesssim T \lesssim \ANY$ for any type $T$, we
adopt an approach based on \emph{error suppression}, where $\ANY$ is
an error-suppressing type, and any failures of subtyping involving
error-suppressing types are not reported. Users can explicitly
suppress type errors by declaring variables with type $\ANY$, and
since an expression with a type error has an error-suppressing type we
avoid cascading errors.

We do this by defining a \emph{infallible} typing judgment $\Gamma \vdash M : T$
such that for any $\Gamma$ and $M$, there is a $T$ such that $\Gamma \vdash M : T$.
For example the rule for addition (ignoring overloads for simplicity) is:
\[
  \frac{\Gamma \vdash M : T \quad \Gamma \vdash M : U}{\Gamma \vdash M+N : \NUMBER} 
\]
We define which judgments produce warnings, for example that rule produces a warning
when
\begin{itemize}
  \item either $T \not<: \NUMBER$ and $T$ is not error-suppressing,
  \item or $U \not<: \NUMBER$ and $U$ is not error-suppressing.
\end{itemize}
To retain type soundness (in the absence of user-supplied error-suppressing types)
we  show that
if $\Gamma \vdash M : T$ and $T$ is error-suppressing, then either
\begin{itemize}
  \item $\Gamma$ or $M$ contains an error-suppressing type, or
  \item $\Gamma \vdash M : T$ produces a warning.
\end{itemize}
From this it is straightforward to show the usual ``well typed
programs don't go wrong'' type soundness result for programs without explicit
error-suppressing types~\cite{BJ23:agda-typeck}.

\section{Further work}

Currently the type inference system uses greedy inference, which is
very sensitive to order of declarations, and can easily result in
false positives. We plan to replace this 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. Local type inference will infer more
precise union types, and hence better type-driven tooling.

At some point, we hope that error suppression will be the only difference
between strict mode and non-strict mode.

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

\end{document}