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

Minor wordsmithing

Browse source
This commit is contained in:
ajeffrey@roblox.com 2023-07-20 09:54:33 -07:00
parent 98c40a0cfb
commit cf8e94fb71
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
papers/hatra23/hatra23.pdf
View file

Binary file not shown.

8
papers/hatra23/hatra23.tex
View file

@ -29,7 +29,7 @@
\begin{abstract} \begin{abstract}
In HATRA 2021, we presented \emph{The Goals Of The Luau Type System}, In HATRA 2021, we presented \emph{The Goals Of The Luau Type System},
describing the human factors issues with designing a type system for a describing the human factors of designing a type system for a
language with a heterogeneous developer community. In this extended language with a heterogeneous developer community. In this extended
abstract we provide a progress report on the work so far, focusing on abstract we provide a progress report on the work so far, focusing on
the unexpected aspects: semantic subtyping and type error the unexpected aspects: semantic subtyping and type error
@ -63,8 +63,8 @@ type-driven tooling is important for productivity. These needs result in a desig
minimizing false negatives (i.e.~type soundness). minimizing false negatives (i.e.~type soundness).
\end{itemize} \end{itemize}
For both communities, type-driven tooling is important, so we For both communities, type-driven tooling is important, so we
provide \emph{infallible type inference}, which infers types no matter provide \emph{infallible type inference}, which infers types
the inputs. even for ill-typed or syntactically invalid programs.
\section{Progress} \section{Progress}
@ -90,7 +90,7 @@ an error-suppressing type, and any failures of subtyping involving
error-suppressing types are not reported. Users can explicitly error-suppressing types are not reported. Users can explicitly
suppress type errors by declaring variables with type $\ANY$, and suppress type errors by declaring variables with type $\ANY$, and
since an expression with a type error has an error-suppressing type we since an expression with a type error has an error-suppressing type we
avoid cascading errors. Error-suppression is in production Luau, and is avoid cascading errors. Error suppression is in production Luau, and is
mechanically verified~\cite{BJ23:agda-typeck}. mechanically verified~\cite{BJ23:agda-typeck}.
\section{Further work} \section{Further work}