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

Tidying up

Browse source
This commit is contained in:
Alan Jeffrey 2023-10-09 16:42:44 -05:00
parent 1edb6a6e9e
commit 3cfad6c692
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
papers/incorrectness24/incorrectness24.pdf
View file

Binary file not shown.

6
papers/incorrectness24/incorrectness24.tex
View file

@ -167,8 +167,8 @@ prohibitively expensive.
The difficult part of non-strict mode error-reporting is predicting The difficult part of non-strict mode error-reporting is predicting
run-time errors. We do this using an error-reporting run-time errors. We do this using an error-reporting
pass that synthesizes a type context such that if any of the $x : T$ in pass that synthesizes a type context $\Delta$ such that if any of the $x : T$ in
the type context are satisfied, then the program will $\Delta$ are satisfied, then the program will
produce a type error. For example in the program produce a type error. For example in the program
\begin{verbatim} \begin{verbatim}
function h(x, y) function h(x, y)
@ -335,7 +335,7 @@ we call any function of type
(S \fun T) \cap (\neg S \fun \ERROR) (S \fun T) \cap (\neg S \fun \ERROR)
\] \]
a \emph{checked} function, since it performs a run-time check a \emph{checked} function, since it performs a run-time check
on its argument. They are called \emph{strong functions} on its argument. They are called \emph{strong arrows}
in Elixir~\cite{DesignElixir}. in Elixir~\cite{DesignElixir}.
Note that this type system has the usual subtyping rule for Note that this type system has the usual subtyping rule for