POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 15:35 - 16:00 at Auditorium - Gradual Typing and Contracts Chair(s): Ronald Garcia

A long-standing shortcoming of statically-typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types distinguish different values of datatypes; if a program annotated with refinements passes type checking, pattern-matching failures become impossible. Unfortunately, refinement is a monolithic property of a type, exacerbating the difficulty of adding refinement types to nontrivial programs.

Gradual typing has explored how to incrementally move between static typing and dynamic typing. We develop a type system with gradual sums that combines refinement with imprecision. Then, we develop a bidirectional version of the type system, which rules out excessive imprecision, and give a type-directed translation to a target language with explicit casts. We prove that the static sublanguage cannot have match failures, that a well-typed program remains well-typed if its type annotations are made less precise, and that making annotations less precise causes target programs to fail later. Several of these results correspond to criteria for gradual typing given by Siek et al. (2015).

Fri 20 Jan

14:20 - 16:00: POPL - Gradual Typing and Contracts at Auditorium
Chair(s): Ronald GarciaUniversity of British Columbia
POPL-2017-papers14:20 - 14:45
Michael Vitousek, Cameron SwordsIndiana University, Jeremy G. SiekIndiana University Bloomington
POPL-2017-papers14:45 - 15:10
Nicolás Lehmann, Éric TanterUniversity of Chile, Chile
Link to publication DOI Pre-print
POPL-2017-papers15:10 - 15:35
Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington
POPL-2017-papers15:35 - 16:00
Khurram A. JaferyUniversity of British Columbia, Joshua DunfieldUniversity of British Columbia