luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-04-18 10:53:45 +01:00
Code Issues Projects Releases Packages Wiki Activity

more tweaking

Browse source
This commit is contained in:
Lily Brown 2021-07-22 13:11:22 -07:00
parent a1c8f620c1
commit a9001eb41d
2 changed files with 27 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
papers/hatra21/hatra21.pdf
View file

Binary file not shown.

41
papers/hatra21/hatra21.tex
View file

@ -40,7 +40,9 @@
Luau is the scripting language that powers user-generated experiences on the Luau is the scripting language that powers user-generated experiences on the
Roblox platform. It is a statically-typed language with type inference based Roblox platform. It is a statically-typed language with type inference based
on the dynamically-typed Lua language. These types are used for providing on the dynamically-typed Lua language. These types are used for providing
autocomplete suggestions in Roblox Studio, the IDE for authoring Roblox experiences. 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, 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. focusing on where the goals differ from those of other type systems.
\end{abstract} \end{abstract}
@ -60,8 +62,10 @@ used by creators of Roblox experiences. Luau is derived from the Lua
programming language~\cite{Lua}, with additional capabilities, programming language~\cite{Lua}, with additional capabilities,
including a type inference engine. including a type inference engine.
This paper will discuss some of the goals of the Luau type system, This paper will discuss some of the goals of the Luau type system, such
focusing on where the goals differ from those of other type systems. as supporting goal-driven learning, non-strict typing semantics, and
mixed strict and non-strict types. Particular focus is placed on how
these goals differ from traditional type systems' goals.
\section{Human Aspects} \section{Human Aspects}
\subsection{Heterogeneous developer community} \subsection{Heterogeneous developer community}
@ -81,6 +85,8 @@ contribute to the energetic creative community, forming the next generation of d
\subsection{Goal-driven learning} \subsection{Goal-driven learning}
Goal: \emph{support learning how to perform specific tasks organically}
All developers are goal-driven, but this is especially true for All developers are goal-driven, but this is especially true for
learners. A learner will download Roblox Studio with an learners. A learner will download Roblox Studio with an
experience in mind, such as designing an obstacle course (an ``obby'') experience in mind, such as designing an obstacle course (an ``obby'')
@ -110,12 +116,13 @@ editor, seen in Fig.~\ref{fig:studio}(b).
This onboarding experience is different from many initial exposures to This onboarding experience is different from many initial exposures to
programming, in that by the time the user first opens the script programming, in that by the time the user first opens the script
editor, they have already built much of their creation, and have a editor, they have already built much of their creation, and have a
very specific concrete aim. It suggests a Luau goal for helping the very specific concrete aim. As such, Luau must allow users to perform a
majority of creators: \emph{support learning how to perform specific specific task with a minimum of ``boilerplate'' code.
tasks}.
\subsection{Type-driven development} \subsection{Type-driven development}
Goal: \emph{enable users to leverage types in their development process}
Professional development studios are also goal-directed (though the Professional development studios are also goal-directed (though the
goals may be more abstract, such as ``decrease user churn'' or goals may be more abstract, such as ``decrease user churn'' or
``improve frame rate'') but have additional needs: ``improve frame rate'') but have additional needs:
@ -144,7 +151,7 @@ property, which is achieved by changing the name in one place,
and then fixing the resulting type errors---once the type system stops and then fixing the resulting type errors---once the type system stops
reporting errors, the refactoring is complete. reporting errors, the refactoring is complete.
To \emph{help support the transition from novice to experienced developer}, To help support the transition from novice to experienced developer,
types are introduced gradually, through API documentation and type discovery. types are introduced gradually, through API documentation and type discovery.
Type inference provides many of the benefits of type-driven development Type inference provides many of the benefits of type-driven development
even to creators who are not explicitly providing types. even to creators who are not explicitly providing types.
@ -255,9 +262,12 @@ tools and techniques such as autocomplete, API documentation
and support for refactoring can still be useful. and support for refactoring can still be useful.
For such developers, Luau provides a For such developers, Luau provides a
\emph{nonstrict mode}, which we hope will eventually be useful for all \emph{nonstrict mode}, which we hope will eventually be useful for all
developers. This does \emph{not} aim for soundness, but instead has developers. The non-strict typing mode is particularly useful when
the goal of ``no false positives``, in the sense that any flagged code adopting Luau types in pre-existing code, which was not authored with
is guaranteed to produce a runtime error when executed. 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.
On the face of it, this is undecidable, since a program such as On the face of it, this is undecidable, since a program such as
$(\IF f() \THEN \ERROR \END)$ will produce a runtime error when $f()$ is $(\IF f() \THEN \ERROR \END)$ will produce a runtime error when $f()$ is
@ -305,11 +315,11 @@ Goal: \emph{support mixed strict/nonstrict development}.
Like every active software community, Roblox developers share code Like every active software community, Roblox developers share code
with one another constantly. First- and third-party developers alike with one another constantly. First- and third-party developers alike
frequently share entire software packages written in Luau. To add to frequently share entire software packages written in Luau. To add to
this, many Roblox experiences are authored by a team. this, many Roblox experiences are authored by a team. It is therefore
It is therefore crucial that we offer first-class support for mixing crucial that we offer first-class support for mixing code written in
code written in strict and nonstrict modes. strict and nonstrict modes.
Some issues raised by mixed-mode types: Some questions raised by mixed-mode types:
\begin{itemize} \begin{itemize}
\item How much feedback can we offer for a nonstrict script that is \item How much feedback can we offer for a nonstrict script that is
@ -323,6 +333,9 @@ Some issues raised by mixed-mode types:
\item Can we have strict and non-strict mode infer the same types, \item Can we have strict and non-strict mode infer the same types,
only with different flagging? only with different flagging?
\item Is strict-mode code sound when it relies on non-strict code,
which has weaker invariants?
\end{itemize} \end{itemize}
\emph{Related work}: this appears to be an under-explored area. \emph{Related work}: this appears to be an under-explored area.