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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:21 - 16:49: Type Inference IIResearch Papers at Sala I
Chair(s): Niki VazouIMDEA Software Institute
15:21 - 15:43
Dynamic Type Inference for Gradual Hindley–Milner Typing
Research Papers
Yusuke MiyazakiKyoto University, Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Link to publication DOI Pre-print Media Attached File Attached
15:43 - 16:05
Gradual Typing: A New Perspective
Research Papers
Giuseppe CastagnaCNRS - Université Paris Diderot, France, Victor LanvinIRIF, Université Paris Diderot, France, Tommaso PetruccianiDIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. SiekIndiana University, USA
Link to publication DOI Media Attached File Attached
16:05 - 16:27
Intersection Types and Runtime Errors in the Pi-Calculus
Research Papers
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Marc De VismeENS Lyon, Damiano MazzaCNRS, Akira YoshimizuINRIA
Link to publication DOI Media Attached File Attached
16:27 - 16:49
Principality and Approximation under Dimensional Bound
Research Papers
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
Link to publication DOI Media Attached File Attached