We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.
Wed 6 SepDisplayed time zone: Belfast change
15:00 - 16:10 | Integrating Static and Dynamic TypingResearch Papers at L1 Chair(s): Ronald Garcia University of British Columbia | ||
15:00 23mTalk | Theorems for Free for Free: Parametricity, With and Without Types Research Papers Amal Ahmed Northeastern University, USA, Dustin Jamner Northeastern University, USA, Jeremy G. Siek Indiana University, USA, Philip Wadler University of Edinburgh, UK DOI | ||
15:23 23mTalk | On Polymorphic Gradual Typing Research Papers Yuu Igarashi Kyoto University, Japan, Taro Sekiyama IBM Research, Japan, Atsushi Igarashi Kyoto University, Japan DOI | ||
15:46 23mTalk | Gradual Typing with Union and Intersection Types Research Papers Giuseppe Castagna CNRS, France / University of Paris Diderot, France, Victor Lanvin ENS Cachan, France DOI | ||