skip to main content
research-article

Manifest Contracts for Datatypes

Published: 14 January 2015 Publication History

Abstract

We study algebraic data types in a manifest contract system, a software contract system where contract information occurs as refinement types. We first compare two simple approaches: refinements on type constructors and refinements on data constructors. For example, lists of positive integers can be described by {l:int list | for_all (lambda y. y > 0) l} in the former, whereas by a user-defined datatype pos_list with cons of type {x:int | x > 0} X pos_list -> pos_list in the latter. The two approaches are complementary: the former makes it easier for a programmer to write types and the latter enables more efficient contract checking. To take the best of both worlds, we propose (1) a syntactic translation from refinements on type constructors to equivalent refinements on data constructors and (2) dynamically checked casts between different but compatible datatypes such as int list and pos_list. We define a manifest contract calculus to formalize the semantics of the casts and prove that the translation is correct.

Supplementary Material

MOV File (2676996.mov)

References

[1]
The Agda 2 homepage. http://wiki.portal.chalmers.se/ agda/pmwiki.php.
[2]
The Coq proof assistant. http://coq.inria.fr/.
[3]
R. Atkey, P. Johann, and N. Ghani. Refining inductive types. Logical Methods in Computer Science, 8(2:9):1--30, 2012.
[4]
J. F. Belo, M. Greenberg, A. Igarashi, and B. C. Pierce. Polymorphic contracts. In Proc. of ESOP, volume 6602 of LNCS, pages 18--37, 2011.
[5]
G. M. Bierman, A. D. Gordon, C. Hriţcu, and D. Langworthy. Se- mantic subtyping with an SMT solver. In Proc. of ACM ICFP, pages 105--116, 2010.
[6]
M. Blume and D. A. McAllester. Sound and complete models of contracts. J. Funct. Program., 16(4-5):375--414, July 2006.
[7]
O. Chitil. A semantics for lazy assertions. In Proc. of ACM PEPM, pages 141--150, 2011.
[8]
M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235--271, Sept. 1992.
[9]
R. B. Findler and M. Felleisen. Contracts for higher-order functions. In Proc. of ACM ICFP, pages 48--59, 2002.
[10]
R. B. Findler, S. Guo, and A. Rogers. Lazy contract checking for immutable data structures. In Proc. of IFL, volume 5083 of LNCS, pages 111--128, 2008.
[11]
C. Flanagan. Hybrid type checking. In Proc. of ACM POPL, pages 245--256, 2006.
[12]
T. Freeman and F. Pfenning. Refinement types for ML. In Proc. of ACM PLDI, pages 268--277, 1991.
[13]
M. Greenberg. Manifest Contracts. PhD thesis, University of Pennsylvania, 2013.
[14]
M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In Proc. of ACM POPL, pages 353--364, 2010.
[15]
J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pages 93--104, 2006.
[16]
D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In Trends in Functional Prog. (TFP), 2007.
[17]
M. Kawaguchi, P. M. Rondon, and R. Jhala. Type-based data structure verification. In Proc. of ACM PLDI, pages 304--315, 2009.
[18]
K. Knowles and C. Flanagan. Hybrid type checking. ACM TOPLAS, 32(2:6):1--34, Feb. 2010.
[19]
K. Knowles, A. Tomb, J. Gronski, S. N. Freund, and C. Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report). Technical report, UCSC, 2007.
[20]
C. McBride. Ornamental algebras, algebraic ornaments. J. Funct. Program., 2014. To appear.
[21]
B. Meyer. Object-Oriented Software Construction, 1st Edition. Prentice-Hall, 1988. ISBN 0--13--629031-0.
[22]
P. C. Nguyen, S. Tobin-Hochstadt, and D. Van Horn. Soft contract verification. In ACM ICFP, 2014.
[23]
B. C. Pierce. Types and Programming Languages. The MIT Press, Cambridge, MA, USA, 2002. ISBN 0--262--16209--1.
[24]
P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In ACM PLDI, 2008.
[25]
J. G. Siek and P. Wadler. Threesomes, with and without blame. In Proc. of ACM POPL, pages 365--376, 2010.
[26]
D. A. Turner. Miranda: A non-strict functional language with poly- morphic types. In Proc. of ACM FPCA, volume 201 of LNCS, pages 1--16, 1985.
[27]
N. Vazou, P. M. Rondon, and R. Jhala. Abstract refinement types. In Proc. of ESOP, volume 7792 of LNCS, pages 209--228, 2013.
[28]
N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. Peyton Jones. Refinement types for Haskell. In ACM ICFP, 2014.
[29]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.
[30]
H. Xi. Dependent ML: An approach to practical programming with dependent types. J. Funct. Program., 17(2):215--286, Mar. 2007.
[31]
H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. of ACM POPL, pages 214--227, 1999.
[32]
D. N. Xu. Hybrid contract checking via symbolic simplification. In Proc. of ACM PEPM, pages 107--116, 2012.
[33]
D. N. Xu, S. L. Peyton Jones, and K. Claessen. Static contract checking for Haskell. In Proc. of ACM POPL, pages 41--52, 2009.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. algebraic datatypes
  2. contract checking
  3. datatype translation
  4. refinement types

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2019)Manifest Contracts with Intersection TypesProgramming Languages and Systems10.1007/978-3-030-34175-6_3(33-52)Online publication date: 18-Nov-2019
  • (2019)Space-Efficient Latent ContractsTrends in Functional Programming10.1007/978-3-030-14805-8_1(3-23)Online publication date: 21-Feb-2019
  • (2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/361040845:4(1-62)Online publication date: 20-Dec-2023
  • (2018)Nondeterministic Manifest ContractsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236964(1-13)Online publication date: 3-Sep-2018
  • (2018)An extended account of contract monitoring strategies as patterns of communicationJournal of Functional Programming10.1017/S095679681800004728Online publication date: 7-Mar-2018
  • (2018)Foundations of dependent interoperabilityJournal of Functional Programming10.1017/S095679681800001128Online publication date: 13-Mar-2018
  • (2017)Soft contract verification for higher-order stateful programsProceedings of the ACM on Programming Languages10.1145/31581392:POPL(1-30)Online publication date: 27-Dec-2017
  • (2017)Stateful manifest contractsACM SIGPLAN Notices10.1145/3093333.300987552:1(530-544)Online publication date: 1-Jan-2017
  • (2017)Stateful manifest contractsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009875(530-544)Online publication date: 1-Jan-2017
  • (2017)Polymorphic Manifest Contracts, Revised and ResolvedACM Transactions on Programming Languages and Systems10.1145/299459439:1(1-36)Online publication date: 6-Feb-2017
  • 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