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 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast change
15:00 - 16:10 | Integrating Static and Dynamic TypingResearch Papers at L1 Chair(s): Ronald GarciaUniversity of British Columbia | ||
15:00 23mTalk | Theorems for Free for Free: Parametricity, With and Without Types Research Papers Amal AhmedNortheastern University, USA, Dustin JamnerNortheastern University, USA, Jeremy G. SiekIndiana University, USA, Philip WadlerUniversity of Edinburgh, UK DOI | ||
15:23 23mTalk | On Polymorphic Gradual Typing Research Papers Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan DOI | ||
15:46 23mTalk | Gradual Typing with Union and Intersection Types Research Papers Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France DOI | ||