skip to main content
10.1145/2676726.2676967acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Space-Efficient Manifest Contracts

Published: 14 January 2015 Publication History

Abstract

The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types---contracts mediating untyped and typed code---is well studied, sound space efficiency for manifest contracts---contracts that check stronger properties than simple types, e.g., "is a natural'' instead of "is an integer''---remains an open problem.
We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. The essential trick is breaking the contract checking down into coercions: structured, blame-annotated lists of checks. By carefully preventing duplicate coercions from appearing, we can restore space efficiency while keeping the same observable behavior.

Supplementary Material

MOV File (2676967_1.mov)
MOV File (2676967_2.mov)
MOV File (2676967_3.mov)

References

[1]
J. F. Belo, M. Greenberg, A. Igarashi, and B. C. Pierce. Polymorphic contracts. In European Symposium on Programming (ESOP), 2011.
[2]
G. M. Bierman, A. D. Gordon, C. Hri\ctcu, and D. Langworthy. Semantic subtyping with an SMT solver. In International Conference on Functional Programming (ICFP), 2010.
[3]
C. Dimoulas, R. Findler, and M. Felleisen. Option contracts. In OOPSLA, pages 475 -- 494, 2013.
[4]
R. B. Findler. Contracts as pairs of projections. In Symposium on Logic Programming, 2006.
[5]
R. B. Findler and M. Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), 2002.
[6]
R. B. Findler, S.-Y. Guo, and A. Rogers. Lazy contract checking for immutable data structures. In Implementation and Application of Functional Languages, pages 111--128. 2008. 10.1007/978--3--540--85373--2_7.
[7]
C. Flanagan. Hybrid type checking. In Principles of Programming Languages (POPL), 2006.
[8]
R. Garcia. Calculating threesomes, with blame. In International Conference on Functional Programming (ICFP), 2013.
[9]
M. Greenberg. Manifest Contracts. PhD thesis, University of Pennsylvania, November 2013.
[10]
M. Greenberg. Space-efficient manifest contracts, 2014. URL http://arxiv.org/abs/1410.2813. Technical report.
[11]
M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In Principles of Programming Languages (POPL), 2010.
[12]
M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. Journal of Functional Programming (JFP), 22 (3): 225--274, May 2012.
[13]
J. Gronski and C. Flanagan. Unifying hybrid types and contracts. In Trends in Functional Programming (TFP), 2007.
[14]
F. Henglein. Dynamic typing: Syntax and proof theory. Sci. Comput. Program., 22 (3): 197--230, 1994.
[15]
D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In Trends in Functional Programming (TFP), pages 404--419, 2007.
[16]
D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. Higher Order Symbol. Comput., 23 (2): 167--189, June 2010.
[17]
K. Knowles and C. Flanagan. Hybrid type checking. ACM Trans. Prog. Lang. Syst., 32: 6:1--6:34, 2010.
[18]
K. Knowles, A. Tomb, J. Gronski, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, 2006.
[19]
E. Koukoutos and V. Kuncak. Checking data structure properties orders of magnitude faster. In Runtime Verification, pages 263--268. 2014. 10.1007/978--3--319--11164--3_22.
[20]
R. Lipton, October 2010. URL http://goo.gl/6Grgt0.
[21]
R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17: 348--375, Aug. 1978.
[22]
PLT. Racket contract system, 2013. URL http://pre.plt-scheme.org/docs/html/guide/contracts.html.
[23]
A. Rastogi, A. Chaudhuri, and B. Hosmer. The ins and outs of gradual type inference. In Principles of Programming Languages (POPL), 2012. 10.1145/2103656.2103714.
[24]
J. Siek, R. Garcia, and W. Taha. Exploring the design space of higher-order casts. In Programming Languages and Systems, volume 5502 of LNCS, pages 17--31. 2009.
[25]
J. Siek, P. Thiemann, and P. Wadler. Blame, coercion, and threesomes: Together again for the first time. Draft., 2014. URL http://homepages.inf.ed.ac.uk/wadler/topics/blame.html#coercions.
[26]
J. G. Siek and R. Garcia. Interpretations of the gradually-typed lambda calculus. In Scheme and Functional Programming (SFP), 2012.
[27]
J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, September 2006.
[28]
J. G. Siek and P. Wadler. Threesomes, with and without blame. In Principles of Programming Languages (POPL), pages 365--376, 2010.
[29]
N. Swamy, M. Hicks, and G. M. Bierman. A theory of typed coercions and its applications. In International Conference on Functional Programming (ICFP), pages 329--340, 2009. ISBN 978--1--60558--332--7.
[30]
S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: From scripts to programs. In OOPSLA, 2006. 10.1145/1176617.1176755.
[31]
P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In European Symposium on Programming (ESOP), 2009.
[32]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115: 38--94, 1994.

Cited By

View all
  • (2024)Gradually Typed Languages Should Be Vigilant!Proceedings of the ACM on Programming Languages10.1145/36498428:OOPSLA1(864-892)Online publication date: 29-Apr-2024
  • (2024)Type-directed operational semantics for gradual typingJournal of Functional Programming10.1017/S095679682400007834Online publication date: 26-Sep-2024
  • (2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
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].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. coercions
  2. contracts
  3. function proxy
  4. pre- and post-conditions
  5. space efficiency

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)5
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Gradually Typed Languages Should Be Vigilant!Proceedings of the ACM on Programming Languages10.1145/36498428:OOPSLA1(864-892)Online publication date: 29-Apr-2024
  • (2024)Type-directed operational semantics for gradual typingJournal of Functional Programming10.1017/S095679682400007834Online publication date: 26-Sep-2024
  • (2023)Typed–Untyped Interactions: A Comparative AnalysisACM Transactions on Programming Languages and Systems10.1145/357983345:1(1-54)Online publication date: 5-Mar-2023
  • (2022)Deep and shallow types for gradual languagesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523430(580-593)Online publication date: 9-Jun-2022
  • (2021)Gradual type theoryJournal of Functional Programming10.1017/S095679682100012531Online publication date: 14-Oct-2021
  • (2019)A space-efficient call-by-value virtual machine for gradual set-theoretic typesProceedings of the 31st Symposium on Implementation and Application of Functional Languages10.1145/3412932.3412940(1-12)Online publication date: 25-Sep-2019
  • (2019)Toward efficient gradual typing for structural types via coercionsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314627(517-532)Online publication date: 8-Jun-2019
  • (2019)Gradual type theoryProceedings of the ACM on Programming Languages10.1145/32903283:POPL(1-31)Online publication date: 2-Jan-2019
  • (2019)Space-Efficient Latent ContractsTrends in Functional Programming10.1007/978-3-030-14805-8_1(3-23)Online publication date: 21-Feb-2019
  • (2018)Collapsible contracts: fixing a pathology of gradual typingProceedings of the ACM on Programming Languages10.1145/32765032:OOPSLA(1-27)Online publication date: 24-Oct-2018
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media