Skip to main content
SpringerLink
Log in

Gradual Refinement

Blending Pattern Matching with Data Abstraction

  • Conference paper
Mathematics of Program Construction (MPC 2010)

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

Included in the following conference series:

Abstract

Pattern matching is advantageous for understanding and reasoning about function definitions, but it tends to tightly couple the interface and implementation of a datatype. Significant effort has been invested in tackling this loss of modularity; however, decoupling patterns from concrete representations while maintaining soundness of reasoning has been a challenge. Inspired by the development of invertible programming, we propose an approach to abstract datatypes based on a right-invertible language rinv—every function has a right (or pre-) inverse. We show how this new design is able to permit a smooth incremental transition from programs with algebraic datatypes and pattern matching, to ones with proper encapsulation (implemented as abstract datatypes), while maintaining simple and sound reasoning.

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

Access this chapter

Log in via an institution
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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alimarine, A., Smetsers, S.: Optimizing generic functions. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 16–31. Springer, Heidelberg (2004)

    Google Scholar 

  2. Alimarine, A., Smetsers, S., van Weelden, A., van Eekelen, M., Plasmeijer, R.: There and back again: Arrows for invertible programming. In: Haskell Workshop, pp. 86–97. ACM, New York (2005)

    Google Scholar 

  3. Bird, R.S.: The promotion and accumulation strategies in transformational programming. ACM Transactions on Programming Languages and Systems 6(4), 487–504 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bird, R.S.: An introduction to the theory of lists. In: Broy, M. (ed.) Logic of Programming and Calculi of Discrete Design. NATO ASI Series F, vol. 36, pp. 3–42. Springer, Heidelberg (1987); Also available as Technical Monograph PRG-56, from the Programming Research Group, Oxford University

    Google Scholar 

  5. Bird, R.S.: A calculus of functions for program derivation. In: Research Topics in Functional Programming, pp. 287–307. Addison-Wesley, Reading (1990)

    Google Scholar 

  6. Bohannon, A., Foster, J.N., Pierce, B.C., Pilkiewicz, A., Schmitt, A.: Boomerang: Resourceful lenses for string data. In: Principles of Programming Languages, January 2008. ACM, New York (2008)

    Google Scholar 

  7. Burstall, R., MacQueen, D., Sannella, D.: Hope: An experimental applicative language. In: Lisp and Functional Programming, pp. 136–143. ACM, New York (1980)

    Google Scholar 

  8. Burton, F.W., Cameron, R.D.: Pattern matching with abstract data types. Journal of Functional Programming 3(2), 171–190 (1993)

    Article  MathSciNet  Google Scholar 

  9. Emir, B., Odersky, M., Williams, J.: Matching objects with patterns. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 273–298. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Erwig, M.: Active patterns. In: Kluge, W.E. (ed.) IFL 1996. LNCS, vol. 1268, pp. 21–40. Springer, Heidelberg (1997)

    Google Scholar 

  11. Erwig, M., Peyton Jones, S.: Pattern guards and transformational patterns. In: Haskell Workshop. ACM, New York (2000)

    Google Scholar 

  12. Fokkinga, M., Meijer, E.: Program calculation properties of continuous algebras. Technical Report CS-R9104, CWI, Amsterdam, Netherlands (January 1991)

    Google Scholar 

  13. Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: A linguistic approach to the view update problem. ACM Transactions on Programming Languages and Systems 29(3) (May 2007); Preliminary version in POPL ’05 (2005)

    Google Scholar 

  14. Foster, J.N., Pierce, B.C., Zdancewic, S.: Updatable security views. In: CSF ’09: Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, Washington, DC, USA, pp. 60–74. IEEE Computer Society Press, Los Alamitos (2009)

    Chapter  Google Scholar 

  15. Foster, J.N., Pilkiewicz, A., Pierce, B.C.: Quotient lenses. In: International Conference on Functional Programming, pp. 383–396. ACM, New York (2008)

    Google Scholar 

  16. Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM 55(4) (2008)

    Google Scholar 

  17. Hu, Z., Mu, S.-C., Takeichi, M.: A programmable editor for developing structured documents based on bidirectional transformations. In: Partial Evaluation and Program Manipulation, pp. 178–189. ACM, New York (2004)

    Google Scholar 

  18. Hughes, J.: Generalising monads to arrows. Science of Computer Programming 37(1-3), 67–111 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  19. Jay, C.B.: The pattern calculus. ACM Transactions on Programming Languages and Systems 26(6) (2004)

    Google Scholar 

  20. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Principles of Programming Languages, pp. 81–92. ACM, New York (2001)

    Google Scholar 

  21. Licata, D., Peyton Jones, S.: View patterns: lightweight views for Haskell (2007), http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns

  22. Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, Boston (2000)

    Google Scholar 

  23. Liskov, B., Zilles, S.: Programming with abstract data types. In: ACM Symposium on Very High Level Languages (1974)

    Google Scholar 

  24. Liu, J., Myers, A.C.: JMatch: Iterable abstract pattern matching for Java. In: Dahl, V., Wadler, P. (eds.) PADL 2003. LNCS, vol. 2562, pp. 110–127. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Magalhães, J.P., Holdermans, S., Jeuring, J., Löh, A.: Optimizing generics is easy! In: PEPM ’10: Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulation, pp. 33–42. ACM, New York (2010)

    Chapter  Google Scholar 

  26. Martin, C., Gibbons, J., Bayley, I.: Disciplined, efficient, generalised folds for nested datatypes. Formal Aspects of Computing 16(1), 19–35 (2004)

    Article  MATH  Google Scholar 

  27. Meertens, L.G.L.T.: Algorithmics: Towards programming as a mathematical activity. In: CWI Symposium on Mathematics and Computer Science. CWI-Monographs, vol. 1, pp. 289–344. North-Holland, Amsterdam (1986)

    Google Scholar 

  28. Moreau, P.-E., Ringeissen, C., Vittek, M.: A pattern matching compiler for multiple target languages. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 61–76. Springer, Heidelberg (2003)

    Google Scholar 

  29. Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Communications of the ACM 22(2), 96–103 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  30. Morita, K., Morihata, A., Matsuzaki, K., Hu, Z., Takeichi, M.: Automatic inversion generates divide-and-conquer parallel programs. In: PLDI ’07: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 146–155. ACM, New York (2007)

    Chapter  Google Scholar 

  31. Mu, S.-C., Hu, Z., Takeichi, M.: An algebraic approach to bi-directional updating. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 2–18. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  32. Mu, S.-C., Hu, Z., Takeichi, M.: An injective language for reversible computation. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 289–313. Springer, Heidelberg (2004)

    Google Scholar 

  33. Nogueira, P., Moreno-Navarro, J.J.: Bialgebra views: A way for polytypic programming to cohabit with data abstraction. In: Workshop on Generic Programming, pp. 61–73. ACM, New York (2008)

    Google Scholar 

  34. Okasaki, C.: Views for Standard ML. In: ACM Workshop on ML (1998)

    Google Scholar 

  35. Palao Gostanza, P., Peña, R., Núñez, M.: A new look at pattern matching in abstract data types. In: International Conference on Functional Programming, pp. 110–121. ACM, New York (1996)

    Google Scholar 

  36. Sereni, D.: Termination analysis and call graph construction for higher-order functional programs. In: Ramsey, N. (ed.) International Conference on Functional Programming, pp. 71–84. ACM Press, New York (2007)

    Google Scholar 

  37. Sleep, M.R., Holmström, S.: A short note concerning lazy reduction rules for append. Software: Practice and Experience 12(11) (1982)

    Google Scholar 

  38. Steele Jr, G.L.: Organizing functional code for parallel execution or, foldl and foldr considered slightly harmful. In: International Conference on Functional Programming, pp. 1–2. ACM, New York (2009)

    Google Scholar 

  39. Syme, D., Neverov, G., Margetson, J.: Extensible pattern matching via a lightweight language extension. In: International Conference on Functional Programming, pp. 29–40. ACM, New York (2007)

    Google Scholar 

  40. Thompson, S.: Lawful functions and program verification in Miranda. Science of Computer Programming 13(2-3), 181–218 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  41. Tullsen, M.: First class patterns. In: Pontelli, E., Santos Costa, V. (eds.) PADL 2000. LNCS, vol. 1753, p. 1. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  42. Wadler, P.: A critique of Abelson and Sussman: Why calculating is better than scheming. ACM SIGPLAN Notices 22(3), 83–94 (1987)

    Article  Google Scholar 

  43. Wadler, P.: Views: A way for pattern matching to cohabit with data abstraction. In: Principles of Programming Languages, pp. 307–313. ACM, New York (1987)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, Oxford University, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Meng Wang & Jeremy Gibbons

  2. Graduate School of Information Sciences, Tohoku University, Aramaki aza Aoba 6-3-09, Aoba-ku, Sendai-city, Miyagi-pref., 980-8579, Japan

    Kazutaka Matsuda

  3. National Institute of Informatics, GRACE Center, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo, 101-8430, Japan

    Zhenjiang Hu

Authors
  1. Meng Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeremy Gibbons
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kazutaka Matsuda
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zhenjiang Hu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’informatique et de génie logiciel, Pavillon Adrien-Pouliot, Université Laval, 1065 Avenue de la Médicine, G1V 0A6, Québec, Canada

    Claude Bolduc , Jules Desharnais  & Béchir Ktari ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wang, M., Gibbons, J., Matsuda, K., Hu, Z. (2010). Gradual Refinement. In: Bolduc, C., Desharnais, J., Ktari, B. (eds) Mathematics of Program Construction. MPC 2010. Lecture Notes in Computer Science, vol 6120. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13321-3_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13321-3_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13320-6

  • Online ISBN: 978-3-642-13321-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation