research-article

Sums of uncertainty: refinements go gradual

Authors:

Khurram A. Jafery,

Jana DunfieldAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 1

Pages 804 - 817

https://doi.org/10.1145/3093333.3009865

Published: 01 January 2017 Publication History

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).

Supplementary Material

Auxiliary Archive (p804-jafery-s.zip)

Appendix with definitions, lemmas, and proofs, omitted from the POPL 2017 paper "Sums of Uncertainty: Refinements Go Gradual" for space reasons.

Download
411.41 KB

References

[1]

Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Trans. Prog. Lang. Syst., 13(2):237–268, 1991.

Digital Library

[2]

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In Principles of Programming Languages, pages 201–214, 2011.

[3]

Esteban Allende, Johan Fabry, Ronald Garcia, and Éric Tanter. Confined gradual typing. In OOPSLA, pages 251–270, 2014.

Digital Library

[4]

Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. A theory of gradual effect systems. In ICFP, pages 283–295, 2014.

[5]

Thierry Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1–3):167–177, 1996.

Digital Library

[6]

Rowan Davies. Practical Refinement-Type Checking. PhD thesis, Carnegie Mellon University, 2005. CMU-CS-05-110. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In ICFP, pages 198–208, 2000.

Digital Library

[7]

Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, 1991. The William James Lectures, 1976.

[8]

Jana Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007. CMU-CS-07-129. Jana Dunfield. Elaborating evaluation-order polymorphism. In Int'l Conf. Functional Programming, 2015. arXiv:1504.07680 {cs.PL}. Jana Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ICFP, 2013. arXiv:1306.6032 {cs.PL}. Jana Dunfield and Frank Pfenning. Tridirectional typechecking. In Principles of Programming Languages, pages 281-292, 2004.

Digital Library

[9]

Tim Freeman. Refinement Types for ML. PhD thesis, Carnegie Mellon University, 1994. CMU-CS-94-110. Tim Freeman and Frank Pfenning. Refinement types for ML. In Programming Language Design and Implementation, pages 268–277, 1991.

Digital Library

[10]

Ronald Garcia and Matteo Cimini. Principal type schemes for gradual programs. In Principles of Programming Languages, pages 303–315, 2015.

Digital Library

[11]

Ronald Garcia, Alison M. Clark, and Éric Tanter. Abstracting gradual typing. In Principles of Programming Languages, pages 429–442, 2016.

Digital Library

[12]

Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1934. English translation, Investigations into logical deduction, in M. Szabo, editor, Collected papers of Gerhard Gentzen (North-Holland, 1969), pages 68–131. Ruud Koot and Jurriaan Hage. Type-based exception analysis for non-strict higher-order functional languages with imprecise exception semantics. In Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, pages 127–138, 2015.

Digital Library

[13]

Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, 1(1):11–60, 1996. Notes for lectures given in 1983 in Siena, Italy. Trevor L. McDonell, Timothy A. K. Zakian, Matteo Cimini, and Ryan R. Newton. Ghostbuster: A tool for simplifying and converting GADTs. In ICFP, pages 338–350, 2016.

[14]

Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

Digital Library

[15]

Frank Pfenning. Lecture notes on harmony. Lecture notes for 15–317: Constructive Logic, Carnegie Mellon University, September 2009.

[16]

www.cs.cmu.edu/ ∼fp/courses/15317f09/lectures/03-harmony.pdf. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511–540, 2001.

Digital Library

[17]

Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Principles of Programming Languages, pages 371–382, 2008.

Digital Library

[18]

Brigitte Pientka and Jana Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In Int?l Joint Conference on Automated Reasoning (IJCAR), pages 15?21, 2010.

Digital Library

[19]

Benjamin C. Pierce and David N. Turner. Local type inference. In Principles of Programming Languages, pages 252–265, 1998.

Digital Library

[20]

Full version in ACM Trans. Prog. Lang. Sys., 22(1):1–44, 2000.

Digital Library

[21]

Dag Prawitz. Natural Deduction. Almqvist & Wiksells, 1965.

[22]

Jeremy Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming, pages 2–27. Springer, 2007.

Digital Library

[23]

Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, pages 81–92, September 2006.

[24]

Jeremy G. Siek and Manish Vachharajani. Gradual typing with unification-based inference. In Symposium on Dynamic Languages (DLS), pages 7:1–7:12, 2008.

Digital Library

[25]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, volume 32. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015.

[26]

Philip Wadler and Robert Bruce Findler. Well-typed programs can’t be blamed. In European Symposium on Programming, pages 1– 16, 2009.

Digital Library

[27]

Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Principles of Programming Languages, pages 214–227, 1999.

Digital Library

Cited By

Ortin FGarcia MPerez-Schofield BQuiroga J(2022)The StaDyn programming languageSoftwareX10.1016/j.softx.2022.10121120(101211)Online publication date: Dec-2022
https://doi.org/10.1016/j.softx.2022.101211
Ramírez Pulido KOrtega-Arjona Jdel Carmen González Huesca L(2020)Gradual Typing Using Union Typing With RecordsElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2020.10.013354(171-186)Online publication date: Dec-2020
https://doi.org/10.1016/j.entcs.2020.10.013
CAMPORA JCHEN SERWIG MWALKINGSHAW E(2022)Migrating gradual typesJournal of Functional Programming10.1017/S095679682200008932Online publication date: 6-Oct-2022
https://doi.org/10.1017/S0956796822000089
Show More Cited By

Index Terms

Sums of uncertainty: refinements go gradual
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs

Recommendations

Sums of uncertainty: refinements go gradual
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

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 ...
Gradual refinement types
POPL '17

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...
Gradual refinement types
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 1

POPL '17

January 2017

901 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3093333

Editor:
Matthew Fluet

Issue’s Table of Contents

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Published in SIGPLAN Volume 52, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
267
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ortin FGarcia MPerez-Schofield BQuiroga J(2022)The StaDyn programming languageSoftwareX10.1016/j.softx.2022.10121120(101211)Online publication date: Dec-2022
https://doi.org/10.1016/j.softx.2022.101211
Ramírez Pulido KOrtega-Arjona Jdel Carmen González Huesca L(2020)Gradual Typing Using Union Typing With RecordsElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2020.10.013354(171-186)Online publication date: Dec-2020
https://doi.org/10.1016/j.entcs.2020.10.013
CAMPORA JCHEN SERWIG MWALKINGSHAW E(2022)Migrating gradual typesJournal of Functional Programming10.1017/S095679682200008932Online publication date: 6-Oct-2022
https://doi.org/10.1017/S0956796822000089
Lakhani ZDas ADeYoung HMordido APfenning F(2022)Polarized SubtypingProgramming Languages and Systems10.1007/978-3-030-99336-8_16(431-461)Online publication date: 5-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99336-8_16
Malewski SGreenberg MTanter É(2021)Gradually structured dataProceedings of the ACM on Programming Languages10.1145/34855035:OOPSLA(1-29)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485503
Campora JChen S(2020)Taming type annotations in gradual typingProceedings of the ACM on Programming Languages10.1145/34282594:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428259
Castagna GLanvin VPetrucciani TSiek J(2019)Gradual typing: a new perspectiveProceedings of the ACM on Programming Languages10.1145/32903293:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290329
IGARASHI ATHIEMANN PTSUDA YVASCONCELOS VWADLER P(2019)Gradual session typesJournal of Functional Programming10.1017/S095679681900016929Online publication date: 18-Nov-2019
https://doi.org/10.1017/S0956796819000169
Toro MGarcia RTanter É(2018)Type-Driven Gradual Security with ReferencesACM Transactions on Programming Languages and Systems10.1145/322906140:4(1-55)Online publication date: 13-Dec-2018
https://dl.acm.org/doi/10.1145/3229061
Xie NBi XOliveira B(2018)Consistent Subtyping for AllProgramming Languages and Systems10.1007/978-3-319-89884-1_1(3-30)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_1
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents