mirror of
https://github.com/luau-lang/luau.git
synced 2024-11-15 14:25:44 +08:00
Delete papers directory
The directory was moved to https://github.com/luau-lang/research See https://github.com/Roblox/luau/issues/1074 for context
This commit is contained in:
Arseny Kapoulkine
GitHub
parent
d70a02a2d0
commit
13e3af2724
12
papers/.gitignore
vendored
12
papers/.gitignore
vendored
@ -1,12 +0,0 @@
|
|||||||
*.aux
|
|
||||||
*.bbl
|
|
||||||
*.blg
|
|
||||||
*.dvi
|
|
||||||
*.fdb_latexmk
|
|
||||||
*.fls
|
|
||||||
*.log
|
|
||||||
*.out
|
|
||||||
*.xcp
|
|
||||||
*.nav
|
|
||||||
*.snm
|
|
||||||
*.toc
|
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 69 KiB |
@ -1,45 +0,0 @@
|
|||||||
# HATRA 21 position paper
|
|
||||||
|
|
||||||
A position paper on Luau for [Human Aspects of Types and Reasoning Assistants](https://2021.splashcon.org/home/hatra-2021) (HATRA) 2021.
|
|
||||||
|
|
||||||
## Installing latexmk
|
|
||||||
|
|
||||||
First install basictex
|
|
||||||
```
|
|
||||||
sudo brew install basictex
|
|
||||||
```
|
|
||||||
|
|
||||||
Then install the dependencies for the paper (sigh, by hand):
|
|
||||||
|
|
||||||
```
|
|
||||||
sudo tlmgr update --all
|
|
||||||
sudo tlmgr install acmart
|
|
||||||
sudo tlmgr install iftex
|
|
||||||
sudo tlmgr install xstring
|
|
||||||
sudo tlmgr install environ
|
|
||||||
sudo tlmgr install totpages
|
|
||||||
sudo tlmgr install trimspaces
|
|
||||||
sudo tlmgr install manyfoot
|
|
||||||
sudo tlmgr install ncctools
|
|
||||||
sudo tlmgr install comment
|
|
||||||
sudo tlmgr install balance
|
|
||||||
sudo tlmgr install preprint
|
|
||||||
sudo tlmgr install libertine
|
|
||||||
sudo tlmgr install inconsolata
|
|
||||||
sudo tlmgr install newtx
|
|
||||||
sudo tlmgr install latexmk
|
|
||||||
sudo tlmgr install montserrat
|
|
||||||
sudo tlmgr install ly1
|
|
||||||
```
|
|
||||||
|
|
||||||
## Building the paper
|
|
||||||
|
|
||||||
To build the paper:
|
|
||||||
```
|
|
||||||
latexmk --pdf hatra21
|
|
||||||
```
|
|
||||||
|
|
||||||
To run latexmk in watching mode (where it rebuilds the PDF on each change):
|
|
||||||
```
|
|
||||||
latexmk --pdf --pvc hatra21
|
|
||||||
```
|
|
||||||
@ -1,177 +0,0 @@
|
|||||||
@Misc{Roblox,
|
|
||||||
author = {Roblox},
|
|
||||||
title = {What is {Roblox}},
|
|
||||||
year = 2021,
|
|
||||||
url = {https://corp.roblox.com},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Misc{Luau,
|
|
||||||
author = {Roblox},
|
|
||||||
title = {The {Luau} Programming Language},
|
|
||||||
year = 2021,
|
|
||||||
url = {https://luau-lang.org},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Misc{Lua,
|
|
||||||
author = {Lua.org and {PUC}-Rio},
|
|
||||||
title = {The {Lua} Programming Language},
|
|
||||||
year = 2021,
|
|
||||||
url = {https://lua.org},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Misc{AllEducators,
|
|
||||||
author = {Roblox},
|
|
||||||
title = {Roblox Education: All Educators},
|
|
||||||
year = {2021},
|
|
||||||
url = {https://education.roblox.com/en-us/educators},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Misc{RobloxDevelopers,
|
|
||||||
author = {Roblox},
|
|
||||||
title = {Roblox Developers Expected to Earn Over \$250 Million in 2020; Platform Now Has Over 150 Million Monthly Active Users
|
|
||||||
},
|
|
||||||
year = {2020},
|
|
||||||
url = {https://corp.roblox.com/2020/07/roblox-developers-expected-earn-250-million-2020-platform-now-150-million-monthly-active-users/},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Book{TAPL,
|
|
||||||
author = {Benjamin C. Pierce},
|
|
||||||
title = {Types and Programming Languages},
|
|
||||||
publisher = {{MIT} Press},
|
|
||||||
year = {2002},
|
|
||||||
isbn = {0-262-16209-1},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Book{TDDIdris,
|
|
||||||
author = {Edwin Brady},
|
|
||||||
title = {Type-Driven Development with {Idris}},
|
|
||||||
publisher = {Manning},
|
|
||||||
year = {2017},
|
|
||||||
isbn = {9781617293023},
|
|
||||||
}
|
|
||||||
|
|
||||||
@PhdThesis{TopQuality,
|
|
||||||
author = {Bastiaan J. Heeren},
|
|
||||||
title = {Top Quality Type Error Messages},
|
|
||||||
school = {U. Utrecht},
|
|
||||||
year = {2005},
|
|
||||||
}
|
|
||||||
|
|
||||||
@PhdThesis{RepairingTypeErrors,
|
|
||||||
author = {Bruce J. McAdam},
|
|
||||||
title = {Repairing Type Errors in Functional Programs},
|
|
||||||
school = {U. Edinburgh},
|
|
||||||
year = {2002},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{GradualTyping,
|
|
||||||
author = {Jeremy G. Siek and Walid Taha},
|
|
||||||
title = {Gradual Typing for Functional Languages},
|
|
||||||
booktitle = {Proc. Scheme and Functional Programming Workshop},
|
|
||||||
year = {2006},
|
|
||||||
pages = {81-92},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{WellTyped,
|
|
||||||
author = {Philip Wadler and Robert B. Findler},
|
|
||||||
title = {Well-typed Programs Can’t be Blamed},
|
|
||||||
booktitle = {Proc. European Symp. Programming},
|
|
||||||
year = {2009},
|
|
||||||
pages = {1-16},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{Contracts,
|
|
||||||
author = {Robert B. Findler and Matthias Felleisen},
|
|
||||||
title = {Contracts for Higher-order Functions},
|
|
||||||
booktitle = {Proc. Int. Conf. Functional Programming},
|
|
||||||
year = {2002},
|
|
||||||
pages = {48-59},
|
|
||||||
}
|
|
||||||
|
|
||||||
@inproceedings{SuccessTyping,
|
|
||||||
author = {Lindahl, Tobias and Sagonas, Konstantinos},
|
|
||||||
title = {Practical Type Inference Based on Success Typings},
|
|
||||||
year = {2006},
|
|
||||||
booktitle = {Proc. Int. Conf. Principles and Practice of Declarative Programming},
|
|
||||||
pages = {167–178},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{IncorrectnessLogic,
|
|
||||||
author = {O'Hearn, Peter W.},
|
|
||||||
title = {Incorrectness Logic},
|
|
||||||
year = {2020},
|
|
||||||
booktitle = {Proc. Symp. Principles of Programming Languages},
|
|
||||||
articleno = {10},
|
|
||||||
pages = {1-32},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Misc{HowToDrawAnOwl,
|
|
||||||
author = {Know Your Meme},
|
|
||||||
title = {How To Draw An Owl},
|
|
||||||
year = {2010},
|
|
||||||
url = {https://knowyourmeme.com/memes/how-to-draw-an-owl},
|
|
||||||
}
|
|
||||||
|
|
||||||
@Misc{RustBook,
|
|
||||||
author = {Klabnik, Steve and Nichols, Carol and the Rust Community},
|
|
||||||
title = {The Rust Programming Language},
|
|
||||||
year = {2021},
|
|
||||||
url = {https://doc.rust-lang.org/book/},
|
|
||||||
}
|
|
||||||
|
|
||||||
@article{TypeClasses,
|
|
||||||
author = {Hall, Cordelia V. and Hammond, Kevin and Peyton Jones, Simon L. and Wadler, Philip L.},
|
|
||||||
title = {Type Classes in Haskell},
|
|
||||||
year = {1996},
|
|
||||||
volume = {18},
|
|
||||||
number = {2},
|
|
||||||
journal = {ACM Trans. Program. Lang. Syst.},
|
|
||||||
pages = {109–138},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{Hazel,
|
|
||||||
author = {Cyrus Omar and Ian Voysey and Ravi Chugh and Matthew Hammer},
|
|
||||||
title = {Live Functional Programming with Typed Holes},
|
|
||||||
booktitle = {Proc. Symp. Principles of Programming Languages},
|
|
||||||
year = {2019},
|
|
||||||
pages = {14:1-14:28},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{MigratoryTyping,
|
|
||||||
author = {Sam Tobin-Hochstadt and Matthias Felleisen and Robert Bruce Findler and Matthew Flatt and Ben Greenman and Andrew M. Kent and Vincent St-Amour and T. Stephen Strickland and Asumu Takikawa},
|
|
||||||
title = {Migratory Typing: Ten Years Later},
|
|
||||||
booktitle = {Proc. Summit on Advances in Programming Languages},
|
|
||||||
year = {2017},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{LinkingTypes,
|
|
||||||
author = {Daniel Patterson and Amal Ahmed},
|
|
||||||
title = {Linking Types for Multi-Language Software: Have Your Cake and Eat It Too},
|
|
||||||
booktitle = {Proc. Summit on Advances in Programming Languages},
|
|
||||||
year = {2017},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{QuickLook,
|
|
||||||
author = {Serrano, Alejandro and Hage, Jurriaan and Peyton Jones, Simon and Vytiniotis, Dimitrios},
|
|
||||||
title = {A quick look at impredicativity},
|
|
||||||
booktitle = {Proc. Int. Conf. Functional Programming},
|
|
||||||
year = {2020},
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{Boehm85,
|
|
||||||
author = {Partial polymorphic type inference is undecidable},
|
|
||||||
title = {Hans-J. Boehm},
|
|
||||||
booktitle = {Proc. Symp. Foundations of Computer Science},
|
|
||||||
year = {1985},
|
|
||||||
pages = {339-345},
|
|
||||||
}
|
|
||||||
|
|
||||||
@article{LocalTypeInference,
|
|
||||||
author = {Pierce, Benjamin C. and Turner, David N.},
|
|
||||||
title = {Local Type Inference},
|
|
||||||
year = {2000},
|
|
||||||
volume = {22},
|
|
||||||
number = {1},
|
|
||||||
journal = {ACM Trans. Program. Lang. Syst.},
|
|
||||||
pages = {1–44},
|
|
||||||
}
|
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 12 KiB |
Binary file not shown.
@ -1,446 +0,0 @@
|
|||||||
\documentclass[acmsmall]{acmart}
|
|
||||||
|
|
||||||
\setcopyright{rightsretained}
|
|
||||||
\copyrightyear{2021}
|
|
||||||
\acmYear{2021}
|
|
||||||
\acmConference[HATRA '21]{Human Aspects of Types and Reasoning Assistants}{October 2021}{Chicago, IL}
|
|
||||||
\acmBooktitle{HATRA '21: 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{\squnder}[1]{\color{red}\underline{{\color{black}#1}}\color{black}}
|
|
||||||
\newcommand{\infer}[2]{\frac{\textstyle#1}{\textstyle#2}}
|
|
||||||
\newcommand{\erase}{\mathrm{erase}}
|
|
||||||
\newcommand{\evCtx}{\mathcal{E}}
|
|
||||||
\newcommand{\NIL}{\mathsf{nil}}
|
|
||||||
\newcommand{\ANY}{\mathsf{any}}
|
|
||||||
\newcommand{\TRUE}{\mathsf{true}}
|
|
||||||
\newcommand{\FALSE}{\mathsf{false}}
|
|
||||||
\newcommand{\NUMBER}{\mathsf{number}}
|
|
||||||
\newcommand{\STRING}{\mathsf{string}}
|
|
||||||
\newcommand{\ERROR}{\mathsf{error}}
|
|
||||||
\newcommand{\IF}{\mathsf{if}\,}
|
|
||||||
\newcommand{\LOCAL}{\mathsf{local}\,}
|
|
||||||
\newcommand{\THEN}{\,\mathsf{then}\,}
|
|
||||||
\newcommand{\ELSE}{\,\mathsf{else}\,}
|
|
||||||
\newcommand{\END}{\,\mathsf{end}}
|
|
||||||
\newcommand{\FUNCTION}{\mathsf{function}\,}
|
|
||||||
\newcommand{\RETURN}{\mathsf{return}\,}
|
|
||||||
\newcommand{\FIND}{\mathsf{find}}
|
|
||||||
\newcommand{\PRINT}{\mathsf{print}}
|
|
||||||
\newcommand{\strlit}[1]{\mbox{``#1''}}
|
|
||||||
|
|
||||||
\begin{document}
|
|
||||||
|
|
||||||
\title{Position Paper: Goals of the Luau Type System}
|
|
||||||
|
|
||||||
\author{Lily Brown}
|
|
||||||
\author{Andy Friesen}
|
|
||||||
\author{Alan Jeffrey}
|
|
||||||
\affiliation{
|
|
||||||
\institution{Roblox}
|
|
||||||
\city{San Mateo}
|
|
||||||
\state{CA}
|
|
||||||
\country{USA}
|
|
||||||
}
|
|
||||||
|
|
||||||
\begin{abstract}
|
|
||||||
Luau is the scripting language that powers user-generated experiences on the
|
|
||||||
Roblox platform. It is a statically-typed language, based on the
|
|
||||||
dynamically-typed Lua language, with type inference. These types are used for providing
|
|
||||||
editor assistance in Roblox Studio, the IDE for authoring Roblox experiences.
|
|
||||||
Due to Roblox's uniquely heterogeneous developer community, Luau must operate
|
|
||||||
in a somewhat different fashion than a traditional statically-typed language.
|
|
||||||
In this paper, we describe some of the goals of the Luau type system,
|
|
||||||
focusing on where the goals differ from those of other type systems.
|
|
||||||
\end{abstract}
|
|
||||||
|
|
||||||
\maketitle
|
|
||||||
|
|
||||||
\section{Introduction}
|
|
||||||
|
|
||||||
The Roblox platform allows anyone to create shared,
|
|
||||||
immersive, 3D experiences. As of July 2021, there are
|
|
||||||
approximately 20~million experiences available on Roblox, created
|
|
||||||
by 8~million developers~\cite{Roblox}. Roblox creators are often young: there are
|
|
||||||
over 200~Roblox kids' coding camps in 65~countries
|
|
||||||
listed by the company as education resources~\cite{AllEducators}.
|
|
||||||
The Luau programming language~\cite{Luau} is the scripting language
|
|
||||||
used by creators of Roblox experiences. Luau is derived from the Lua
|
|
||||||
programming language~\cite{Lua}, with additional capabilities,
|
|
||||||
including a type inference engine.
|
|
||||||
|
|
||||||
This paper will discuss some of the goals of the Luau type system, such
|
|
||||||
as supporting goal-driven learning, non-strict typing semantics, and
|
|
||||||
mixing strict and non-strict types. Particular focus is placed on how
|
|
||||||
these goals differ from traditional type systems' goals.
|
|
||||||
|
|
||||||
\section{Needs of the Roblox platform}
|
|
||||||
\subsection{Heterogeneous developer community}
|
|
||||||
|
|
||||||
Need: \emph{a language that is powerful enough to support professional users, yet accessible to beginners}
|
|
||||||
|
|
||||||
Quoting a Roblox 2020 report \cite{RobloxDevelopers}:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \emph{Adopt Me!} now has over 10 billion plays and surpassed 1.6 million concurrent users earlier this year.
|
|
||||||
\item \emph{Piggy}, launched in January 2020, has close to 5 billion visits in just over six months.
|
|
||||||
\item There are now 345,000 developers on the platform who are monetizing their games.
|
|
||||||
\end{itemize}
|
|
||||||
This demonstrates the heterogeneity of the Roblox developer community:
|
|
||||||
developers of experiences with billions of plays are on the same
|
|
||||||
platform as children first learning to code. Both of these groups are important to
|
|
||||||
support: the professional development studios bring high-quality experiences to the
|
|
||||||
platform, and the beginning creators contribute to the energetic creative community,
|
|
||||||
forming the next generation of developers.
|
|
||||||
|
|
||||||
\subsection{Goal-driven learning}
|
|
||||||
|
|
||||||
Need: \emph{organic learning for achieving specific goals}
|
|
||||||
|
|
||||||
All developers are goal-driven, but this is especially true for
|
|
||||||
learners. A learner will download Roblox Studio
|
|
||||||
(the creation environment for the Roblox platform) with an
|
|
||||||
experience in mind, such as designing an obstacle course
|
|
||||||
to play in with their friends.
|
|
||||||
|
|
||||||
The user experience of developing a Roblox experience is primarily a
|
|
||||||
3D interactive one, seen in Fig.~\ref{fig:studio}(a). The user designs
|
|
||||||
and deploys 3D assets such as terrain, parts and joints, providing
|
|
||||||
them with physics attributes such as mass and orientation. The user
|
|
||||||
can interact with the experience in Studio, and deploy it to a Roblox
|
|
||||||
server so anyone with the Roblox app can play it. Physics, rendering
|
|
||||||
and multiplayer are all immediately accessible to creators.
|
|
||||||
|
|
||||||
\begin{figure}
|
|
||||||
\includegraphics[width=0.48\textwidth]{studio-mow.png}
|
|
||||||
\includegraphics[width=0.48\textwidth]{studio-script-editor.png}
|
|
||||||
\caption{Roblox Studio's 3D environment editor (a), and script editor (b)}
|
|
||||||
\label{fig:studio}
|
|
||||||
\end{figure}
|
|
||||||
|
|
||||||
At some point during experience design, the experience creator has a need
|
|
||||||
that can't be met by the game engine alone, such as ``the stairs should
|
|
||||||
light up when a player walks on them'' or ``a firework is set off
|
|
||||||
every few seconds''. At this point, they will discover the script
|
|
||||||
editor, seen in Fig.~\ref{fig:studio}(b).
|
|
||||||
|
|
||||||
This onboarding experience is different from many initial exposures to
|
|
||||||
programming, in that by the time the user first opens the script
|
|
||||||
editor, they have already built much of their creation, and have a
|
|
||||||
very specific concrete aim. As such, Luau must allow users to perform a
|
|
||||||
specific task with as much help as possible from tools.
|
|
||||||
|
|
||||||
A common workflow for getting started is to Google the task, then
|
|
||||||
cut-and-paste the resulting code, adapting it as needed. Since this
|
|
||||||
is so common, backward compatibility of Luau with existing code is
|
|
||||||
important, even for learners who do not have an existing code base to
|
|
||||||
maintain.
|
|
||||||
|
|
||||||
Type-driven tools are useful to all creators, in as much as they help
|
|
||||||
them achieve their current goals. For example type-driven
|
|
||||||
autocomplete, or type-driven API documentation, are of immediate
|
|
||||||
benefit. Traditional typechecking can be useful, for example for
|
|
||||||
catching spelling mistakes, but for most goal-driven developers, the
|
|
||||||
type system should help or get out of the way.
|
|
||||||
|
|
||||||
\subsection{Type-driven development}
|
|
||||||
|
|
||||||
Need: \emph{a language that supports large-scale codebases and defect detection}
|
|
||||||
|
|
||||||
Professional development studios are also goal-directed (though the
|
|
||||||
goals may be more abstract, such as ``decrease user churn'' or
|
|
||||||
``improve frame rate'') but have additional needs:
|
|
||||||
\begin{itemize}
|
|
||||||
|
|
||||||
\item \emph{Code planning}:
|
|
||||||
code spends much of its time in an incomplete state, with holes
|
|
||||||
that will be filled in later.
|
|
||||||
|
|
||||||
\item \emph{Code refactoring}:
|
|
||||||
code evolves over time, and it is easy for changes to
|
|
||||||
break previously-held invariants.
|
|
||||||
|
|
||||||
\item \emph{Defect detection}:
|
|
||||||
code has errors, and detecting these at runtime (for example by crash telemetry)
|
|
||||||
can be expensive and recovery can be time-consuming.
|
|
||||||
|
|
||||||
\end{itemize}
|
|
||||||
Detecting defects ahead-of-time is a traditional goal of type systems,
|
|
||||||
resulting in an array of techniques for establishing safety results,
|
|
||||||
surveyed for example in~\cite{TAPL}. Supporting code planning and
|
|
||||||
refactoring are some of the goals of \emph{type-driven
|
|
||||||
development}~\cite{TDDIdris} under the slogan ``type, define,
|
|
||||||
refine''. A common use of type-driven development is renaming a
|
|
||||||
property, which is achieved by changing the name in one place,
|
|
||||||
and then fixing the resulting type errors---once the type system stops
|
|
||||||
reporting errors, the refactoring is complete.
|
|
||||||
|
|
||||||
To help support the transition from novice to experienced developer,
|
|
||||||
types are introduced gradually, through API documentation and type discovery.
|
|
||||||
Type inference provides many of the benefits of type-driven development
|
|
||||||
even to creators who are not explicitly providing types.
|
|
||||||
|
|
||||||
\section{Goals of the type system}
|
|
||||||
\subsection{Infallible types}
|
|
||||||
|
|
||||||
Goal: \emph{provide type information even for ill-typed or syntactically invalid programs.}
|
|
||||||
|
|
||||||
Programs spend much of their time under development in an ill-typed or incomplete state, even if the
|
|
||||||
final artifact is well-typed. If tools such as autocomplete and API documentation are type-driven,
|
|
||||||
this means that tooling needs to rely on type information even for ill-typed
|
|
||||||
or syntactically invalid programs. An analogy is infallible parsers, which perform error recovery and
|
|
||||||
provide an AST for all input texts, even if they don't adhere to the parser's syntax.
|
|
||||||
|
|
||||||
Program analysis can still flag type errors, which may be presented
|
|
||||||
to the user with red squiggly underlining. Formalizing this, rather
|
|
||||||
than a judgment
|
|
||||||
$\Gamma\vdash M:T$, for an input term $M$, there is a judgment
|
|
||||||
$\Gamma \vdash M \Rightarrow N : T$ where $N$ is an output term
|
|
||||||
where some subterms are \emph{flagged} as having type errors, written $\squnder{N}$. Write $\erase(N)$
|
|
||||||
for the result of erasing flaggings: $\erase(\squnder{N}) = \erase(N)$.
|
|
||||||
|
|
||||||
For example, in Lua, the $\STRING.\FIND$ function expects two strings, and returns the
|
|
||||||
offsets for that string:
|
|
||||||
\[
|
|
||||||
\STRING.\FIND(\strlit{hello}, \strlit{ell}) \rightarrow (2, 4)
|
|
||||||
\qquad
|
|
||||||
\STRING.\FIND(\strlit{world}, \strlit{ell}) \rightarrow (\NIL, \NIL)
|
|
||||||
\]
|
|
||||||
and in Luau it has the type:
|
|
||||||
\[
|
|
||||||
\STRING.\FIND : (\STRING, \STRING) \rightarrow (\NUMBER?, \NUMBER?)
|
|
||||||
\]
|
|
||||||
In a conventional type system, there is no judgment for ill-typed terms
|
|
||||||
such as $\STRING.\FIND(\strlit{hello}, 37)$ but in an infallible system we flag the error
|
|
||||||
and approximate the type, for example:
|
|
||||||
\[
|
|
||||||
{} \vdash
|
|
||||||
\STRING.\FIND(\strlit{hello}, 37)
|
|
||||||
\Rightarrow
|
|
||||||
\squnder{\STRING.\FIND(\strlit{hello}, 37)}
|
|
||||||
:
|
|
||||||
(\NUMBER?, \NUMBER?)
|
|
||||||
\]
|
|
||||||
The goal of infallible types is that every term has a typing judgment
|
|
||||||
given by flagging ill-typed subterms:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \emph{Typability}: for every $M$ and $\Gamma$,
|
|
||||||
there are $N$ and $T$ such that $\Gamma \vdash M \Rightarrow N : T$.
|
|
||||||
\item \emph{Erasure}: if $\Gamma \vdash M \Rightarrow N : T$
|
|
||||||
then $\erase(M) = \erase(N)$
|
|
||||||
\end{itemize}
|
|
||||||
Some issues raised by infallible types:
|
|
||||||
\begin{itemize}
|
|
||||||
\item Which heuristics should be used to provide types for flagged programs? For example, could one
|
|
||||||
use minimal edit distance to correct for spelling mistakes in field names?
|
|
||||||
\item How can we avoid cascading type errors, where a developer is
|
|
||||||
faced with type errors that are artifacts of the heuristics, rather
|
|
||||||
than genuine errors?
|
|
||||||
\item How can the goals of an infallible type system be formalized?
|
|
||||||
\end{itemize}
|
|
||||||
\emph{Related work}:
|
|
||||||
there is a large body of work on type error reporting
|
|
||||||
(see, for example, the survey in~\cite[Ch.~3]{TopQuality})
|
|
||||||
and on type-directed program repair
|
|
||||||
(see, for example, the survey in~\cite[Ch.~3]{RepairingTypeErrors}),
|
|
||||||
but less on type repair.
|
|
||||||
The closest work is Hazel's~\cite{Hazel} \emph{typed holes}
|
|
||||||
where $\squnder{N}$ is treated as a partially-filled hole in the program,
|
|
||||||
though in that work partially-filled holes are not erased at run-time.
|
|
||||||
Many compilers perform
|
|
||||||
error recovery during typechecking, but do not provide a semantics
|
|
||||||
for programs with type errors.
|
|
||||||
|
|
||||||
\subsection{Strict types}
|
|
||||||
|
|
||||||
Goal: \emph{no false negatives.}
|
|
||||||
|
|
||||||
For developers who are interested in defect detection, Luau provides a \emph{strict mode},
|
|
||||||
which acts much like a traditional, sound, type system. This has the goal of ``no false negatives''
|
|
||||||
where any possible run-time error is flagged. This is formalized using:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \emph{Operational semantics}: a reduction judgment $M \rightarrow N$ on terms.
|
|
||||||
\item \emph{Values}: a subset of terms representing a successfully completed evaluation.
|
|
||||||
\end{itemize}
|
|
||||||
Error states at runtime are represented as stuck states (terms that are not
|
|
||||||
values but cannot reduce), and showing that no well-typed program is
|
|
||||||
stuck. This is not true if typing is infallible, but can fairly
|
|
||||||
straightforwardly be adapted. We extend the operational semantics to flagged terms,
|
|
||||||
where $M \rightarrow M'$ implies $\squnder{M} \rightarrow \squnder{M'}$, and
|
|
||||||
for any value $V$ we have $\squnder{V} \rightarrow V$, then show:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \emph{Progress}: if ${} \vdash M \Rightarrow N : T$, then either $N \rightarrow N'$ or $N$ is a value or $N$ has a flagged subterm.
|
|
||||||
\item \emph{Preservation}: if ${} \vdash M \Rightarrow N : T$ and $N \rightarrow N'$ then $M \rightarrow^*M'$ and ${} \vdash M' \Rightarrow N' : T$.
|
|
||||||
\end{itemize}
|
|
||||||
For example in typechecking the program:
|
|
||||||
\[
|
|
||||||
\LOCAL (i,j) = \STRING.\FIND(x, y);
|
|
||||||
\IF i \THEN \PRINT(j-i) \END
|
|
||||||
\]
|
|
||||||
the interesting case is $i-j$ in a context where $i$ has type
|
|
||||||
$\NUMBER$ (since it is guarded by the $\IF$) but $j$ has type
|
|
||||||
$\NUMBER?$. Since subtraction has type $(\NUMBER, \NUMBER) \rightarrow \NUMBER$,
|
|
||||||
this is a type error, so the relevant typing judgment is:
|
|
||||||
\[\begin{array}{r@{}l}
|
|
||||||
x: \STRING, y: \STRING \vdash {}&
|
|
||||||
(\LOCAL (i,j) = \STRING.\FIND(x, y);
|
|
||||||
\IF i \THEN \PRINT(j-i) \END) \\
|
|
||||||
\Rightarrow {}&
|
|
||||||
(\LOCAL (i,j) = \STRING.\FIND(x, y);
|
|
||||||
\IF i \THEN \PRINT(\squnder{j-i}) \END)
|
|
||||||
\end{array}\]
|
|
||||||
Some issues raised by soundness for infallible types:
|
|
||||||
\begin{itemize}
|
|
||||||
\item How should the judgments and their metatheory be set up?
|
|
||||||
\item How should type inference and generic functions be handled?
|
|
||||||
\item Is the operational semantics of flagged values
|
|
||||||
($\squnder{V} \rightarrow V$) the right one?
|
|
||||||
\end{itemize}
|
|
||||||
\emph{Related work}: gradual typing and blame analysis, e.g.~\cite{GradualTyping,WellTyped,Contracts}.
|
|
||||||
The main difference between this approach and that of migratory typing~\cite{MigratoryTyping}
|
|
||||||
is that (due to backward compatibility with existing Lua) we cannot introduce
|
|
||||||
extra code during migration.
|
|
||||||
|
|
||||||
\subsection{Nonstrict types}
|
|
||||||
|
|
||||||
Goal: \emph{no false positives.}
|
|
||||||
|
|
||||||
For developers who are not interested in defect detection, type-driven
|
|
||||||
tools and techniques such as autocomplete, API documentation
|
|
||||||
and type-driven refactoring are still useful.
|
|
||||||
For such developers, Luau provides a
|
|
||||||
\emph{nonstrict mode}, which we hope will eventually be useful for all
|
|
||||||
developers. This non-strict typing mode is particularly useful when
|
|
||||||
adopting Luau types in pre-existing code that was not authored with
|
|
||||||
the type system in mind. Non-strict mode does \emph{not} aim for
|
|
||||||
soundness, but instead has the goal of ``no false positives``, in the
|
|
||||||
sense that any flagged code is guaranteed to produce a runtime error
|
|
||||||
when executed.
|
|
||||||
|
|
||||||
Our previous example was, in fact, a false positive since a programmer
|
|
||||||
can make use of the fact that $\STRING.\FIND(x, y)$ is either $\NIL$
|
|
||||||
in both results or neither, so if $i$ is non-$\NIL$ then so is $j$.
|
|
||||||
This is discussed in the English-language documentation but not reflected
|
|
||||||
in the type. So flagging $(i - j)$ is a false positive.
|
|
||||||
|
|
||||||
On the face of it, detecting all errors without false positives is undecidable, since a program such as
|
|
||||||
$(\IF f() \THEN \ERROR \END)$ will produce a runtime error when $f()$ is
|
|
||||||
$\TRUE$. Instead we can aim for a weaker property: that all flagged code
|
|
||||||
is either dead code or will produce an error. Either of these is a
|
|
||||||
defect, so deserves flagging, even if the tool does not know
|
|
||||||
which reason applies.
|
|
||||||
|
|
||||||
We can formalize this by defining an \emph{evaluation context}
|
|
||||||
$\evCtx[\bullet]$, and saying $M$ is \emph{incorrectly flagged}
|
|
||||||
if it is of the form $\evCtx[\squnder{V}]$. We can then define:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \emph{Correct flagging}: if ${} \vdash M \Rightarrow N : T$
|
|
||||||
then $N$ is correctly flagged.
|
|
||||||
\end{itemize}
|
|
||||||
Some issues raised by nonstrict types:
|
|
||||||
\begin{itemize}
|
|
||||||
|
|
||||||
\item Will nonstrict types result in errors being flagged in function call sites
|
|
||||||
rather than definitions?
|
|
||||||
|
|
||||||
\item In Luau, ill-typed property update of most tables succeeds
|
|
||||||
(the property is inserted if it did not exist), and so functions which
|
|
||||||
update properties cannot be flagged. Can we still provide meaningful
|
|
||||||
error messages in such cases?
|
|
||||||
|
|
||||||
\item Does nonstrict typing require whole program analysis,
|
|
||||||
to find all the possible types a property might be updated with?
|
|
||||||
|
|
||||||
\item The natural formulation of function types in a nonstrict setting
|
|
||||||
is that of~\cite{SuccessTyping}: if $f: T \rightarrow U$ and $f(V) \rightarrow^* W$
|
|
||||||
then $V:T$ and $W:U$. This formulation is \emph{covariant} in $T$,
|
|
||||||
not \emph{contravariant}; what impact does this have?
|
|
||||||
|
|
||||||
\end{itemize}
|
|
||||||
\emph{Related work}: success types~\cite{SuccessTyping} and incorrectness logic~\cite{IncorrectnessLogic}.
|
|
||||||
|
|
||||||
\subsection{Mixing types}
|
|
||||||
|
|
||||||
Goal: \emph{support mixed strict/nonstrict development}.
|
|
||||||
|
|
||||||
Like every active software community, Roblox developers share code
|
|
||||||
with one another constantly. First- and third-party developers alike
|
|
||||||
frequently share entire software packages written in Luau. To add to
|
|
||||||
this, many Roblox experiences are authored by a team. It is therefore
|
|
||||||
crucial that we offer first-class support for mixing code written in
|
|
||||||
strict and nonstrict modes.
|
|
||||||
|
|
||||||
Some questions raised by mixed-mode types:
|
|
||||||
\begin{itemize}
|
|
||||||
|
|
||||||
\item How much feedback can we offer for a nonstrict script that is
|
|
||||||
importing strict-mode code?
|
|
||||||
|
|
||||||
\item In strict mode, how do we talk about values and types that are
|
|
||||||
drawn from nonstrict code?
|
|
||||||
|
|
||||||
\item How can we combine the goals of strict and nonstrict types?
|
|
||||||
|
|
||||||
\item Can we have strict and non-strict mode infer the same types,
|
|
||||||
only with different flagging?
|
|
||||||
|
|
||||||
\item Is strict-mode code sound when it relies on non-strict code,
|
|
||||||
which has weaker invariants?
|
|
||||||
|
|
||||||
\item How can we avoid introducing function wrappers in higher-order code
|
|
||||||
at the strict/nonstrict boundary?
|
|
||||||
|
|
||||||
\end{itemize}
|
|
||||||
\emph{Related work}: there has been work on interoperability between different type systems,
|
|
||||||
notably~\cite{LinkingTypes}, but there the overall goals of the systems were similar safety properties.
|
|
||||||
In our case, the two type systems have different goals.
|
|
||||||
|
|
||||||
\subsection{Type inference}
|
|
||||||
|
|
||||||
Goal: \emph{infer types to allow gradual adoption of type annotations.}
|
|
||||||
|
|
||||||
Since backward compatibility with existing code is important, we have
|
|
||||||
to provide types for code without explicit annotations. Moreover, we
|
|
||||||
want to make use of type-directed tools such as autocomplete, so we
|
|
||||||
cannot adopt the common strategy of treating all untyped variables as
|
|
||||||
having type $\ANY$. This leads us to type inference.
|
|
||||||
|
|
||||||
To make use of type-driven technologies for programs
|
|
||||||
without explicit type annotations, we use a type inference algorithm.
|
|
||||||
Since Luau includes System~F, type inference is undecidable~\cite{Boehm85},
|
|
||||||
but we can still make use of heuristics such as local type inference~\cite{LocalTypeInference}.
|
|
||||||
|
|
||||||
It remains to be seen if type inference can satisfy the goals of
|
|
||||||
strict and non-strict types. The current Luau system
|
|
||||||
infers different types in the two modes, which is unsatisfactory as it
|
|
||||||
makes changing mode a non-local breaking change. In addition,
|
|
||||||
non-strict inference is currently too imprecise to support
|
|
||||||
type-directed tools such as autocomplete.
|
|
||||||
|
|
||||||
Some questions raised by type inference:
|
|
||||||
\begin{itemize}
|
|
||||||
|
|
||||||
\item How many cases in strict mode cannot be inferred by the type inference system? Minimizing
|
|
||||||
this kind of error is desirable, to make the type system as unobtrusive as possible.
|
|
||||||
\item Can something like the Rust traits system~\cite{RustBook} or Haskell classes~\cite{TypeClasses} be used to provide types for overloaded operators, without hopelessly confusing learners?
|
|
||||||
\item Type inference currently infers monotypes for unannotated
|
|
||||||
functions, in contrast to QuickLook~\cite{QuickLook}, which can infer generic types.
|
|
||||||
Will this be good enough for idiomatic Luau scripts?
|
|
||||||
\item Can type inference be used to infer the same types in strict and nonstrict mode, to ease migrating between modes, with the only difference being error reporting?
|
|
||||||
\end{itemize}
|
|
||||||
\emph{Related work}: there is a large body of work on type inference, largely summarized in~\cite{TAPL}.
|
|
||||||
|
|
||||||
\section{Conclusions}
|
|
||||||
|
|
||||||
In this paper, we have presented some of the goals of the Luau type
|
|
||||||
system, and how they map to the needs of the Roblox creator
|
|
||||||
community. We have also explored how these goals differ from traditional
|
|
||||||
type systems, where it is necessary to accommodate the unique needs of
|
|
||||||
the Roblox platform. We have sketched what a solution might look like;
|
|
||||||
all that remains is to draw the owl~\cite{HowToDrawAnOwl}.
|
|
||||||
|
|
||||||
\bibliographystyle{ACM-Reference-Format} \bibliography{bibliography}
|
|
||||||
|
|
||||||
\end{document}
|
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 589 KiB |
Binary file not shown.
|
Before Width: | Height: | Size: 294 KiB |
Binary file not shown.
@ -1,203 +0,0 @@
|
|||||||
\documentclass[aspectratio=169]{beamer}
|
|
||||||
|
|
||||||
\usecolortheme{whale}
|
|
||||||
\setbeamertemplate{navigation symbols}{}
|
|
||||||
\definecolor{background}{rgb}{0.945,0.941,0.96}
|
|
||||||
\definecolor{bluish}{rgb}{0.188,0.455,0.863}
|
|
||||||
\usepackage{montserrat}
|
|
||||||
\setbeamerfont{frametitle}{size=\Large,series=\bfseries}
|
|
||||||
\setbeamerfont{title}{size=\Huge,series=\bfseries}
|
|
||||||
\setbeamerfont{date}{shape=\itshape}
|
|
||||||
\setbeamercolor{title}{bg=bluish}
|
|
||||||
\setbeamercolor{frametitle}{bg=bluish}
|
|
||||||
\setbeamercolor{background canvas}{bg=background}
|
|
||||||
\setbeamercolor{itemize item}{fg=bluish}
|
|
||||||
\setbeamercolor{part name}{fg=background}
|
|
||||||
\setbeamercolor{part title}{bg=bluish}
|
|
||||||
\setbeamertemplate{footline}[text line]{\hfill\raisebox{5ex}{\insertshorttitle~~~~\insertframenumber/\inserttotalframenumber~~~~\includegraphics[width=5em]{Logo-Roblox-Black-Full.png}}}
|
|
||||||
\AtBeginPart{{\setbeamertemplate{footline}{}\frame{\partpage}}}
|
|
||||||
|
|
||||||
\newcommand{\erase}{\mathsf{erase}}
|
|
||||||
|
|
||||||
\title{Goals of the Luau~Type~System}
|
|
||||||
\author{Lily Brown \and Andy Friesen \and Alan Jeffrey}
|
|
||||||
\institute[Roblox]{\includegraphics[width=15em]{Logo-Roblox-Black-Full.png}}
|
|
||||||
\date[HATRA '21]{\textit{Human Aspects of Types and Reasoning Assistants} 2021}
|
|
||||||
|
|
||||||
\begin{document}
|
|
||||||
|
|
||||||
{\setbeamertemplate{footline}{}\frame{\titlepage}}
|
|
||||||
|
|
||||||
\part{Creator Goals}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Roblox}
|
|
||||||
|
|
||||||
A platform for creating shared immersive 3D experiences:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Many}: 20 million experiences, 8 million creators.
|
|
||||||
\item \textbf{At scale}: e.g.~\emph{Adopt Me!} has 10 billion plays.
|
|
||||||
\item \textbf{Learners}: e.g.~200+ kids' coding camps in 65+ countries.
|
|
||||||
\item \textbf{Professional}: 345k creators monetizing experiences.
|
|
||||||
\end{itemize}
|
|
||||||
A very heterogeneous community.
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Roblox developer community}
|
|
||||||
|
|
||||||
All developers are important:
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Learners}: energetic creative community.
|
|
||||||
\item \textbf{Professionals}: high-quality experiences.
|
|
||||||
\item \textbf{Everyone inbetween}: some learners become professionals!
|
|
||||||
\end{itemize}
|
|
||||||
Satisfying everyone is sometimes challenging.
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Roblox Studio}
|
|
||||||
|
|
||||||
Demo time!
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Learners have immediate goals}
|
|
||||||
|
|
||||||
E.g. ``when a player steps on the button, advance the slide''.
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{3D scene editor} meets most goals, e.g.~model parts.
|
|
||||||
\item \textbf{Programming} is needed for reacting to events, e.g.~collisions.
|
|
||||||
\item \textbf{Onboarding} is very different from ``let's learn to program''.
|
|
||||||
\item \textbf{Google Stack Overflow} is a common workflow.
|
|
||||||
\item \textbf{Type-driven tools} are useful, e.g.~autocomplete or API help.
|
|
||||||
\item \textbf{Type errors} may be useful (e.g.~catching typos) but some are not.
|
|
||||||
\end{itemize}
|
|
||||||
Type systems should help or get out of the way.
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Professionals have long-term goals}
|
|
||||||
|
|
||||||
E.g. ``decrease user churn'' or ``improve frame rate''.
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Code planning}: programs are incomplete.
|
|
||||||
\item \textbf{Code refactoring}: programs change.
|
|
||||||
\item \textbf{Defect detection}: programs have bugs.
|
|
||||||
\end{itemize}
|
|
||||||
Type-driven development is a useful technique!
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\part{Luau Type System}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Infallible types}
|
|
||||||
|
|
||||||
Goal: \emph{support type-driven tools (e.g. autocomplete) for all programs.}
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Traditional typing judgment} says nothing about ill-typed terms.
|
|
||||||
\item \textbf{Infallible judgment}: every term gets a type.
|
|
||||||
\item \textbf{Flag type errors}: elaboration introduces \emph{flagged} subterms.
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\emph{Related work}:
|
|
||||||
\begin{itemize}
|
|
||||||
\item Type error reporting, program repair.
|
|
||||||
\item Typed holes (e.g. in Hazel).
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Strict types}
|
|
||||||
|
|
||||||
Goal: \emph{no false negatives}.
|
|
||||||
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Strict mode} enabled by developers who want defect detection.
|
|
||||||
\item \textbf{Business as usual} soundness via progress + preservation.
|
|
||||||
\item \textbf{Gradual types} for programs with flagged type errors.
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\emph{Related work}:
|
|
||||||
\begin{itemize}
|
|
||||||
\item Lots and lots for type safety.
|
|
||||||
\item Gradual typing, blame analysis, migratory types\dots
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Nonstrict types}
|
|
||||||
|
|
||||||
Goal: \emph{no false positives}.
|
|
||||||
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Nonstrict mode} enabled by developers who want type-drive tools.
|
|
||||||
\item \textbf{Victory condition} does not have an obvious definition!
|
|
||||||
\item \textbf{A shot at it}: a program is \emph{incorrectly flagged} if it contains
|
|
||||||
a flagged value (i.e.~a flagged program has successfully terminated).
|
|
||||||
\item \textbf{Progress + correct flagging} is what we want???
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\emph{Related work}:
|
|
||||||
\begin{itemize}
|
|
||||||
\item Success types (e.g. Erlang Dialyzer).
|
|
||||||
\item Incorrectness Logic.
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Mixing types}
|
|
||||||
|
|
||||||
Goal: \emph{support mixed strict/nonstrict development}.
|
|
||||||
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Per-module} strict/nonstrict mode.
|
|
||||||
\item \textbf{Combined} progress + preservation with progress + correct flagging?
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\emph{Related work}:
|
|
||||||
\begin{itemize}
|
|
||||||
\item Some on mixed languages, but with shared safety properties.
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\begin{frame}
|
|
||||||
|
|
||||||
\frametitle{Type inference}
|
|
||||||
|
|
||||||
Goal: \emph{provide benefits of type-directed tools to everyone}.
|
|
||||||
|
|
||||||
\begin{itemize}
|
|
||||||
\item \textbf{Infer types} for all variables. Resist the urge to give up and ascribe a top type when an error is encountered.
|
|
||||||
\item \textbf{System F} is in Luau, so everything is undecidable. Yay heuristics!
|
|
||||||
\item \textbf{Different modes} currently infer different types. Boo!
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\emph{Related work}:
|
|
||||||
\begin{itemize}
|
|
||||||
\item Lots, though not on mixed modes.
|
|
||||||
\end{itemize}
|
|
||||||
|
|
||||||
\end{frame}
|
|
||||||
|
|
||||||
\part{Thank you!\\Roblox is hiring!}
|
|
||||||
|
|
||||||
\end{document}
|
|
||||||
@ -1,69 +0,0 @@
|
|||||||
@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},
|
|
||||||
}
|
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 12 KiB |
Binary file not shown.
@ -1,156 +0,0 @@
|
|||||||
\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}
|
|
||||||
@ -1,122 +0,0 @@
|
|||||||
@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},
|
|
||||||
}
|
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 12 KiB |
Binary file not shown.
@ -1,366 +0,0 @@
|
|||||||
\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}
|
|
||||||
Loading…
Reference in New Issue
Block a user