Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Space-Efficient Latent Contracts

  • Conference paper
  • First Online:
Trends in Functional Programming (TFP 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10447))

Included in the following conference series:

Abstract

Standard higher-order contract monitoring breaks tail recursion and leads to space leaks that can change a program’s asymptotic complexity; space-efficiency restores tail recursion and bounds the amount of space used by contracts. Space-efficient contract monitoring for contracts enforcing simple type disciplines (a/k/a gradual typing) is well studied. Prior work establishes a space-efficient semantics for manifest contracts without dependency [10]; we adapt that work to a latent calculus with dependency. We guarantee space efficiency when no dependency is used; we cannot generally guarantee space efficiency when dependency is used, but instead offer a framework for making such programs space efficient on a case-by-case basis.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Readers may observe that the contract betrays a deeper knowledge of numbers than the functions themselves. We offer this example as minimal, not naturally occurring.

  2. 2.

    Concrete syntax for such predicates can be written much more nicely, but we ignore such concerns here.

  3. 3.

    Robby Findler, personal correspondence, 2016-05-19.

References

  1. Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. J. Funct. Program. (JFP) 1(4), 375–416 (1991)

    Article  MathSciNet  Google Scholar 

  2. Ahmed, A., Findler, R.B., Siek, J., Wadler, P.: Blame for all. In: Principles of Programming Languages (POPL) (2011)

    Google Scholar 

  3. Dimoulas, C., Felleisen, M.: On contract satisfaction in a higher-order world. TOPLAS 33(5), 16:1–16:29 (2011)

    Article  Google Scholar 

  4. Dimoulas, C., Findler, R.B., Flanagan, C., Felleisen, M.: Correct blame for contracts: no more scapegoating. In: Principles of Programming Languages (POPL) (2011)

    Google Scholar 

  5. Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Complete monitors for behavioral contracts. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 214–233. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_11

    Chapter  Google Scholar 

  6. Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: International Conference on Functional Programming (ICFP) (2002)

    Google Scholar 

  7. Findler, R.B., Guo, S., Rogers, A.: Lazy contract checking for immutable data structures. In: Chitil, O., Horváth, Z., Zsók, V. (eds.) IFL 2007. LNCS, vol. 5083, pp. 111–128. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85373-2_7

    Chapter  Google Scholar 

  8. Flatt, M., PLT: Reference: Racket. Technical report, PLT-TR-2010-1, PLT Design Inc. (2010). http://racket-lang.org/tr1/

  9. Garcia, R.: Calculating threesomes, with blame. In: International Conference on Functional Programming (ICFP) (2013)

    Google Scholar 

  10. Greenberg, M.: Space-efficient manifest contracts. In: Principles of Programming Languages (POPL) (2015)

    Google Scholar 

  11. Greenberg, M., Pierce, B.C., Weirich, S.: Contracts made manifest. In: Principles of Programming Languages (POPL) (2010)

    Google Scholar 

  12. Grossman, D., Morrisett, G., Zdancewic, S.: Syntactic type abstraction. TOPLAS 22(6), 1037–1080 (2000)

    Article  Google Scholar 

  13. Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. In: Trends in Functional Programming (TFP), pp. 404–419, April 2007

    Google Scholar 

  14. Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. High. Order Symbol. Comput. 23(2), 167–189 (2010)

    Article  MathSciNet  Google Scholar 

  15. Jhala, R.: Refinement types for Haskell. In: Programming Languages Meets Program Verification (PLPV), p. 27. ACM, New York (2014)

    Google Scholar 

  16. Meyer, B.: Eiffel: The Language. Prentice-Hall Inc., Upper Saddle River (1992)

    MATH  Google Scholar 

  17. Plotkin, G.: LCF considered as a programming language. Theoret. Comput. Sci. 5(3), 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  18. Racket contract system (2013)

    Google Scholar 

  19. Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Programming Language Design and Implementation (PLDI) (2008)

    Google Scholar 

  20. Sekiyama, T., Igarashi, A., Greenberg, M.: Polymorphic manifest contracts, revised and resolved. TOPLAS (2016, accepted in September; to appear)

    Google Scholar 

  21. Sekiyama, T., Nishida, Y., Igarashi, A.: Manifest contracts for datatypes. In: Principles of Programming Languages (POPL), pp. 195–207. ACM, New York (2015)

    Google Scholar 

  22. Siek, J., Thiemann, P., Wadler, P.: Blame, coercion, and threesomes: together again for the first time. In: Programming Language Design and Implementation (PLDI) (2015)

    Google Scholar 

  23. Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional Programming Workshop, September 2006

    Google Scholar 

  24. Siek, J.G., Wadler, P.: Threesomes, with and without blame. In: Principles of Programming Languages (POPL), pp. 365–376. ACM, New York (2010)

    Google Scholar 

  25. Thiemann, P.: A delta for hybrid type checking. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 411–432. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30936-1_22

    Chapter  Google Scholar 

  26. Tobin-Hochstadt, S., Van Horn, D.: Higher-order symbolic execution via contracts. In: OOPSLA, pp. 537–554. ACM, New York (2012)

    Article  Google Scholar 

  27. Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209–228. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_13

    Chapter  Google Scholar 

  28. Wadler, P.: A complement to blame. In: Ball, T., Bodik, R., Krishnamurthi, S., Lerner, B.S., Morrisett, G. (eds.) SNAPL. LIPIcs, vol. 32, pp. 309–320. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  29. Wadler, P., Findler, R.B.: Well-typed programs can’t be blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1–16. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_1

    Chapter  Google Scholar 

Download references

Acknowledgments

The existence of this paper is due to comments from Sam Tobin-Hochstadt and David Van Horn that I chose to interpret as encouragement. Robby Findler provided the Racket example and helped correct and clarify a draft; Sam Tobin-Hochstadt also offered corrections and suggestions. The reviews offered helpful comments, too.

Author information

Authors and Affiliations

  1. Pomona College, Claremont, CA, USA

    Michael Greenberg

Authors
  1. Michael Greenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Greenberg .

Editor information

Editors and Affiliations

  1. University of Maryland, College Park, MD, USA

    David Van Horn

  2. Chalmers University of Technology, Gothenburg, Sweden

    John Hughes

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Greenberg, M. (2019). Space-Efficient Latent Contracts. In: Van Horn, D., Hughes, J. (eds) Trends in Functional Programming. TFP 2016. Lecture Notes in Computer Science(), vol 10447. Springer, Cham. https://doi.org/10.1007/978-3-030-14805-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-14805-8_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-14804-1

  • Online ISBN: 978-3-030-14805-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation