Thu 8 Nov 2018 11:15 - 11:37 at Studio 2 - Types and Contracts Chair(s): Hakjoo Oh

The premise of gradual typing is that programmers should get the best of both worlds: the static guarantees of static types, and the dynamic flexibility of untyped programming. This is an enticing benefit, but one that, in practice, may carry significant costs. Significant enough, in fact, to threaten the very practicality of gradual typing; slowdowns as high as 120x are reported as arising from gradual typing.

If one examines these results closely, though, it becomes clear that the costs of gradual typing are not evenly distributed. Indeed, while mixing typed and untyped code almost invariably carries non-trivial costs, truly deal breaking slowdowns are concentrated among a set of pathological cases. Unfortunately, the very presence of these pathological cases—and therefore the possibility of hitting them during development—makes gradual typing a risky proposition in any setting that even remotely cares about performance.

This work attacks one source of large overheads in these pathological cases: an accumulation of contract wrappers that perform redundant checks. The work introduces a novel strategy for contract checking—\emph{collapsible contracts}—which eliminates this redundancy and drastically reduces the overhead of contract wrappers for this pathological case. In turn, this brings their overhead in line with the common case, and thus makes gradual typing a more predictable development choice.

We implemented this checking strategy as part of the Racket contract system, which is used in the Typed Racket gradual typing system. Our experiments show that our strategy successfully brings a class of pathological cases in line with normal cases, while not introducing an undue overhead to normal cases.

Thu 8 Nov
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00: Types and ContractsOOPSLA at Studio 2
Chair(s): Hakjoo OhKorea University
10:30 - 10:52
Horn-ICE Learning for Synthesizing Invariants and Contracts
Deepak D'Souza, Ezudheen P, Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderMax Planck Institute for Software Systems, P. MadhusudanUniversity of Illinois at Urbana-Champaign
10:52 - 11:15
Gradual Liquid Type InferenceDistinguished Paper Award
Niki VazouIMDEA Software Institute, Éric TanterUniversity of Chile & Inria Paris, David Van HornUniversity of Maryland, USA
11:15 - 11:37
Collapsible Contracts: Fixing a Pathology of Gradual Typing
Daniel FelteyNorthwestern University, USA, Ben GreenmanNortheastern University, USA, Christophe ScholliersUniversiteit Gent, Belgium, Robby FindlerNorthwestern University, USA, Vincent St-AmourNorthwestern University
11:37 - 12:00
The Root Cause of Blame: Contracts for Intersection and Union Types
Jack WilliamsUniversity of Edinburgh, UK, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK