Commit bbe3ee47 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added footnote for STH (Sam Tobin Hochstadt)

parent b86b4001
......@@ -143,7 +143,14 @@ maximal interpretation would yield
$(\dyn \to \code{number}\vee\code{string}) \land ((\code{number} \land \dyn) \to \code{number})
\land ((\dyn \textbackslash \code{number}) \to \code{string})$. However, as
we stated before, this would introduce an unnecessary cast if the function
were to be applied to an integer. Hence the need for the second part of
were to be applied to an integer.\footnote{%
Notice that considering
$\code{number} \land \dyn\simeq \code{number}$ as in~\cite{siek2016recursive} is
not an option here, since it would force us to choose between having
the gradual guarantee or having, say,
$\code{number} \land \code{string}$ be more precise than
$\code{number} \land \dyn$.}%
Hence the need for the second part of
Rule~\textsc{[AbsInf+]}: the maximal interpretation of $\code{number} \land \dyn$
is $\code{number}$, and it is clear that, if $\code x$ is given type \code{number},
the function type-checks, thanks to occurrence typing. Thus, after some
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment