Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 15:43 - 16:05 at Sala I - Type Inference II Chair(s): Niki Vazou

We define a new, more semantic interpretation of gradual types and use it to “gradualize” two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism.

In particular, we use the new interpretation to define two preorders on types, subtyping and materialization, and we employ these preorders to define three gradual type systems —Hindley-Milner, with subtyping, and with union and intersection types— which we present in two different forms: declaratively and algorithmically.

The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the existing standard rules of the type system. This yields clearer, more intelligible, and streamlined definitions; it also shows a direct correlation between cast insertion and materialization that suggests a logical interpretation of the cast calculus, an essential component of gradual typing systems. For the algorithmic presentation, we show how it can be defined by using already existing constraint solving algorithms simply by adding some pre-/post-processing steps. We relate corresponding declarative and algorithmic presentations by soundness and completeness results.

As customary, the semantics of the various gradually-typed languages is given in terms of a compilation into cast calculi that use blame labels to pinpoint cast failures. To that end, we show how to define the operational semantics for casts in the presence of unions and intersections, which is an important and far-from-obvious result. We also show a direct correlation between the safety of a cast and the “polarity” of its blame label, allowing for a simpler formulation of the so-called blame safety property.

Slides (main.pdf)369KiB

Thu 17 Jan

Displayed time zone: Belfast change

15:21 - 16:49
Type Inference IIResearch Papers at Sala I
Chair(s): Niki Vazou IMDEA Software Institute
15:21
22m
Talk
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Yusuke Miyazaki Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
15:43
22m
Talk
Gradual Typing: A New Perspective
Research Papers
Giuseppe Castagna CNRS - Université Paris Diderot, France, Victor Lanvin IRIF, Université Paris Diderot, France, Tommaso Petrucciani DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. Siek Indiana University, USA
Link to publication DOI Media Attached File Attached
16:05
22m
Talk
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Ugo Dal Lago University of Bologna, Italy / Inria, France, Marc De Visme ENS Lyon, Damiano Mazza CNRS, Akira Yoshimizu INRIA
Link to publication DOI Media Attached File Attached
16:27
22m
Talk
Principality and Approximation under Dimensional Bound
Research Papers
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
Link to publication DOI Media Attached File Attached