mirror of
https://github.com/luau-lang/luau.git
synced 2024-12-14 22:21:10 +00:00
204 lines
5.6 KiB
TeX
204 lines
5.6 KiB
TeX
|
\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}
|