Commit c16eb9e5 by Victor Lanvin

### Reworked section on gradual types

parent 12183920
 ... ... @@ -56,26 +56,39 @@ reducing $e$ to a value and checking whether the type of the value is a subtype of $t$. In standard gradual semantics, \code{\Cast{\dyn}{42}} is a value. And this value is of type \code{\dyn}, which is not a subtype of \code{number}. Therefore the check in \code{foo} would fail for \code{\Cast{\dyn}{42}}, and so would the whole function call. Although this behavior is type safe, this is the opposite of what every programmer would expect: one would expect the test \code{(typeof($e$)==="number")} to return true for \code{\Cast{\dyn}{42}} and false for, say, \code{\Cast{\dyn}{true}}, whereas the standard semantics of type-cases would return false in both cases. would the whole function call. Although this behavior is type safe, this violates the gradual guarantee~\cite{siek2015refined} since giving a \emph{more precise} type to the parameter \code{x} (such as \code{number}) would make the function succeed, as the cast to $\dyn$ would not be inserted. A solution is to modify the semantics of type-cases, and in particular of \code{typeof}, to strip off all the casts in a value, even nested ones. This however adds a new overhead at runtime. Another solution is to simply accept this counter-intuitive result, which has at least the benefit of promoting the dynamic type to a first class type, instead of just considering it as a directive to the front-end. Indeed, this would allow to dynamically check whether some argument has the dynamic type \code{\dyn} (i.e., whether it was applied to a cast to such a type) simply by \code{(typeof($e$)==="\dyn")}. Whatever solution we choose it is clear that in both cases it would be much better if the application \code{foo(42)} were compiled as is, thus getting rid of a cast that at best is useless and at worse gives a counter-intuitive and unexpected semantics. \code{typeof}, to strip off all the casts in values, even nested ones. While this adds a new overhead at runtime, this is preferable to losing the gradual guarantee, and the overhead can be mitigated by having a proper representation of cast values that allows to strip all casts at once. However, this problem gets much more complex when considering functional values. In fact, as we hinted in Section~\ref{ssec:algorithm}, there is no way to modify the semantics of type cases to preserve both the gradual guarantee and the soundness of the system in the presence of arbitrary type cases. For example, consider the function $f = \lambda^{(\Int \to \Int) \to \Int} g. \tcase{g}{(\Int \to \Int)}{g\ 1}{\code{true}}$. This function is well-typed since the type of the parameter guarantees that only the first branch can be taken, and thus that only an integer can be returned. However, if we apply this function to $h = \MCast{\Int \to \Int}{(\lambda^{\dyn \to \dyn} x.\ x)}$, the type case strips off the cast around $h$ (to preserve the gradual guarantee), then checks if $\lambda^{\dyn \to \dyn} x.\ x$ has type $\Int \to \Int$. Since $\dyn \to \dyn$ is not a subtype of $\Int \to \Int$, the check fails and the application returns $\code{true}$, which is unsound. Therefore, to preserve soundness in the presence of gradual types, type cases should not test functional types other than $\Empty \to \Any$, which is the same restriction as the one presented by~\citet{siek2016recursive}. While this solves the problem of the gradual guarantee, it is clear that it would be much better if the application \code{foo(42)} were compiled as is, without introducing the cast \code{\Cast{\dyn}{42}}, thus getting rid of the overhead associated with removing this cast in the type case. This is where the previous section about refining function types comes in handy. To get rid of all superfluous casts, we have to fully exploit the information provided to us by occurrence typing and deduce for the function in~\eqref{foo3} the type ... ...
 ... ... @@ -294,4 +294,21 @@ series = {POPL ’12} timestamp = {Tue, 14 May 2019 10:00:41 +0200}, biburl = {https://dblp.org/rec/conf/esop/Bonnaire-Sergeant16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } \ No newline at end of file } @inproceedings{siek2015refined, title={Refined criteria for gradual typing}, author={Siek, Jeremy G and Vitousek, Michael M and Cimini, Matteo and Boyland, John Tang}, booktitle={1st Summit on Advances in Programming Languages (SNAPL 2015)}, year={2015}, organization={Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik} } @incollection{siek2016recursive, title={The recursive union of some gradual types}, author={Siek, Jeremy G and Tobin-Hochstadt, Sam}, booktitle={A List of Successes That Can Change the World}, pages={388--410}, year={2016}, publisher={Springer} }
 ... ... @@ -110,6 +110,7 @@ \newcommand{\Undef}{\Keyw{Undef}} \newcommand{\undefcst}{\texttt{undef}} \newcommand {\Cast}[2]{\tt #2$$\langle$$#1$$\rangle$$} \newcommand {\MCast}[2]{#2\langle #1\rangle} \newcommand {\ifty}[4]{\ensuremath{\texttt{(}#1\in#2\texttt{)?}#3\texttt{:}#4}} \newcommand {\code}[1]{\texttt{\color{darkblue}#1}} \newcommand {\p}[1]{\texttt{#1}} ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.896110475063324, "perplexity": 1726.0902531165978}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2022-40/segments/1664030337906.7/warc/CC-MAIN-20221007014029-20221007044029-00650.warc.gz"}