Sums of uncertainty: refinements go gradual
From MaRDI portal
Publication:5370915
DOI10.1145/3009837.3009865zbMATH Open1380.68094arXiv1611.02392OpenAlexW2556346428MaRDI QIDQ5370915FDOQ5370915
Authors: Khurram A. Jafery, Joshua Dunfield 
Publication date: 20 October 2017
Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)
Abstract: 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 of 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).
Full work available at URL: https://arxiv.org/abs/1611.02392
Recommendations
Cited In (7)
This page was built for publication: Sums of uncertainty: refinements go gradual
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370915)
