Merge remote-tracking branch 'origin' into ajeffrey-property-readonly

papers/.gitignore

@@ -6,4 +6,7 @@
 *.fls
 *.log
 *.out
-*.xcp
+*.xcp
+*.nav
+*.snm
+*.toc

papers/hatra21/README.md

@@ -27,8 +27,10 @@ sudo tlmgr install preprint
 sudo tlmgr install libertine
 sudo tlmgr install inconsolata
 sudo tlmgr install newtx
-sudo tlmgr install latexmk
-```
+sudo tlmgr install latexmk`
+sudo tlmgr install montserrat
+sudo tlmgr install ly1
+``
 
 ## Building the paper
 

papers/hatra21/hatra21.tex

@@ -8,6 +8,7 @@
 \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}}

papers/hatra21/talk.tex

@@ -0,0 +1,203 @@
+\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}

rfcs/syntax-if-expression.md

@@ -20,7 +20,7 @@ To solve these problems, we propose introducing a first-class ternary conditiona
 
 Concretely, the `if-then-else` expression must match `if <expr> then <expr> else <expr>`; it can also contain an arbitrary number of `elseif` clauses, like `if <expr> then <expr> elseif <expr> then <expr> else <expr>`. Note that in either case, `else` is mandatory.
 
-The result of the expression is the then-expression when condition is truthful (not `nil` or `false`) and else-expression otherwise.
+The result of the expression is the then-expression when condition is truthful (not `nil` or `false`) and else-expression otherwise. Only one of the two possible resulting expressions is evaluated.
 
 Example: