Skip to main content
SpringerLink
Log in

Memoization in Type-Directed Partial Evaluation

  • Conference paper
  • First Online:
Book cover Generative Programming and Component Engineering (GPCE 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2487))

Abstract

We use a code generator—type-directed partial evaluation— to verify conversions between isomorphic types, or more precisely to verify that a composite function is the identity function at some complicated type. A typed functional language such as ML provides a natural support to express the functions and type-directed partial evaluation provides a convenient setting to obtain the normal form of their composition. However, off-the-shelf type-directed partial evaluation turns out to yield gigantic normal forms.

We identify that this gigantism is due to redundancies, and that these redundancies originate in the handling of sums, which uses delimited continuations. We successfully eliminate these redundancies by extending type-directed partial evaluation with memoization capabilities. The result only works for pure functional programs, but it provides an unexpected use of code generation and it yields orders-of-magnitude improvements both in time and in space for type isomorphisms.

Basic Research in Computer Science (www. brics. dk), funded by the Danish National Research Foundation.

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. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip Scott. Normalization by evaluation for typed lambda calculus with coproducts. In Joseph Halpern, editor, Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 203–210, Boston, Massachusetts, June 2001. IEEE Computer Society Press.

    Google Scholar 

  2. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction-free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter Johnstone, editors, Category Theory and Computer Science, number 953 in Lecture Notes in Computer Science, pages 182–199, Cambridge, UK, August 1995. Springer-Verlag.

    Google Scholar 

  3. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for a polymorphic system. In Edmund M. Clarke, editor, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 98–106, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

    Google Scholar 

  4. Vincent Balat. PhD thesis, PPS, Université Paris VII-Denis Diderot, Paris, France, 2002. Forthcoming.

    Google Scholar 

  5. Vincent Balat and Olivier Danvy. Strong normalization by type-directed partial evaluation and run-time code generation. In Xavier Leroy and Atsushi Ohori, editors, Proceedings of the Second International Workshop on Types in Compilation, number 1473 in Lecture Notes in Computer Science, pages 240–252, Kyoto, Japan, March 1998. Springer-Verlag.

    Google Scholar 

  6. Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. Remarks on isomorphisms in typed lambda calculi with empty and sum types. In Gordon D. Plotkin, editor, Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, July 2002. IEEE Computer Society Press. To appear.

    Google Scholar 

  7. Gilles Barthe and Olivier Pons. Type isomorphisms and proof reuse in dependent type theory. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001, number 2030 in Lecture Notes in Computer Science, pages 57–71, Genova, Italy, April 2001. Springer-Verlag.

    Chapter  Google Scholar 

  8. Ulrich Berger. Program extraction from normalization proofs. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91–106, Utrecht, The Netherlands, March 1993. Springer-Verlag.

    Chapter  Google Scholar 

  9. Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In Bernhard Möller and John V. Tucker, editors, Prospects for hardware foundations (NADA), number 1546 in Lecture Notes in Computer Science, pages 117–137. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  10. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Gilles Kahn, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203–211, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press.

    Google Scholar 

  11. Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231–247, 1992.

    MATH  MathSciNet  Google Scholar 

  12. Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, January 1993. ACM Press.

    Google Scholar 

  13. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75–94, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  14. Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 242–257, St. Petersburg Beach, Florida, January 1996. ACM Press.

    Google Scholar 

  15. Olivier Danvy. Online type-directed partial evaluation. In Masahiko Sato and Yoshihito Toyama, editors, Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, pages 271–295, Kyoto, Japan, April 1998. World Scientific. Extended version available as the technical report BRICS RS-97-53.

    Google Scholar 

  16. Olivier Danvy. Type-directed partial evaluation. In John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann, editors, Partial Evaluation-Practice and Theory; Proceedings of the 1998 DIKU Summer School, number 1706 in Lecture Notes in Computer Science, pages 367–411, Copenhagen, Denmark, July 1998. Springer-Verlag.

    Google Scholar 

  17. Olivier Danvy, Morten Rhiger, and Kristoffer Rose. Normalization by evaluation with typed abstract syntax. Journal of Functional Programming, 11(6):673–680, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  18. Olivier Danvy and René Vestergaard. Semantics-based compiling: A case study in type-directed partial evaluation. InDoaitse Swierstra, editors. Eighth International Symposium on Programming Language Implementation and Logic Programming, number 1140 in Lecture Notes in Computer Science, Aachen, Germany, September 1996. Springer-Verlag. Kuchen and Swierstra [34], pages 182–197. Extended version available as the technical report BRICS-RS-96-13.

    Google Scholar 

  19. David Delahaye, Roberto Di Cosmo, and Benjamin Werner. Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes. In PRC/GDR de programmation, Pôle Preuves et Spécifications Algébriques, November 1997.

    Google Scholar 

  20. Roberto Di Cosmo. Type isomorphisms in a type assignment framework. In Andrew W. Appel, editor, Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 200–210, Albuquerque, New Mexico, January 1992. ACM Press.

    Google Scholar 

  21. Roberto Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485–525, 1993.

    MathSciNet  Google Scholar 

  22. Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.

    Google Scholar 

  23. John Doner and Alfred Tarski. An extended arithmetic of ordinal numbers. Fundamenta Mathematica, 65:95–127, 1969. See also http://www.pps.jussieu.fr/~dicosmo/Tarski/.

    MATH  MathSciNet  Google Scholar 

  24. Andrzej Filinski. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, Proceedings of the International Conference on Principles and Practice of Declarative Programming, number 1702 in Lecture Notes in Computer Science, pages 378–395, Paris, France, September 1999. Springer-Verlag. Extended version available as the technical report BRICS RS-99-17.

    Google Scholar 

  25. Andrzej Filinski. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151–165, Kraków, Poland, May 2001. Springer-Verlag.

    Chapter  Google Scholar 

  26. Yoshihiko Futamura, Kenroku Nogi, and Akihiko Takano. Essence of generalized partial computation. Theoretical Computer Science, 90(1):61–79, 1991.

    Article  MATH  Google Scholar 

  27. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

    Google Scholar 

  28. Bernd Grobauer. Topics in Semantics-based Program Manipulation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-6.

    MATH  Google Scholar 

  29. Bernd Grobauer and Zhe Yang. The second Futamura projection for type-directed partial evaluation. Higher-Order and Symbolic Computation, 14(2/3):173–219, 2001.

    Article  MATH  Google Scholar 

  30. R. Gurevič. Equational theory of positive numbers with exponentiation. Proceedings of the American Mathematical Society, 94(1):135–141, May 1985.

    Google Scholar 

  31. Simon Helsen and Peter Thiemann. Two flavors of offline partial evaluation. In Jieh Hsiang and Atsushi Ohori, editors, Advances in Computing Science-ASIAN’98, number 1538 in Lecture Notes in Computer Science, pages 188–205, Manila, The Philippines, December 1998. Springer-Verlag.

    Chapter  Google Scholar 

  32. John Hughes. Lazy memo-functions. In Jean-Pierre Jouannaud, editor, Functional Programming Languages and Computer Architecture, number 201 in Lecture Notes in Computer Science, pages 129–146, Nancy, France, September 1985. Springer-Verlag.

    Google Scholar 

  33. Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, London, UK, 1993. Available online at http://www.dina.kvl.dk/~sestoft/pebook/.

    MATH  Google Scholar 

  34. Herbert Kuchen and Doaitse Swierstra, editors. Eighth International Symposium on Programming Language Implementation and Logic Programming, number 1140 in Lecture Notes in Computer Science, Aachen, Germany, September 1996. Springer-Verlag.

    Google Scholar 

  35. Donald Michie. ‘Memo’ functions and machine learning. Nature, 218:19–22, April 1968.

    Google Scholar 

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

    Google Scholar 

  37. Larry C. Paulson. ML for the Working Programmer (2nd edition). Cambridge University Press, 1996.

    Google Scholar 

  38. Morten Rhiger. Higher-Order Program Generation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-4.

    MATH  Google Scholar 

  39. Mikael Rittri. Retrieving library identifiers by equational matching of types. In Mark E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, number 449 in Lecture Notes in Computer Science, pages 603–617, Kaiserslautern, Germany, July 1990. Springer-Verlag.

    Google Scholar 

  40. Mikael Rittri. Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University of Göteborg, Göteborg, Sweden, 1990.

    Google Scholar 

  41. Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71–89, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  42. Colin Runciman and Ian Toyn. Retrieving re-usable software components by polymorphic type. Journal of Functional Programming, 1(2):191–211, 1991.

    MATH  MathSciNet  Google Scholar 

  43. Sergei V. Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387–1400, 1983.

    Article  Google Scholar 

  44. Peter Thiemann. Implementing memoization for partial evaluation. InDoaitse Swierstra, editors. Eighth International Symposium on Programming Language Implementation and Logic Programming, number 1140 in Lecture Notes in Computer Science, Aachen, Germany, September 1996. Springer-Verlag. Kuchen and Swierstra [34], pages 198–212.

    Google Scholar 

  45. Jeffrey D. Ullman. Elements of ML Programming (ML 97 edition). Prentice-Hall, 1998.

    Google Scholar 

  46. Alex J. Wilkie. On exponentiation-a solution to Tarski’s high school algebra problem. Quaderni di Matematica, 2001. To appear. Mathematical Institute, University of Oxford (preprint).

    Google Scholar 

  47. Zhe Yang. Language Support for Program Generation: Reasoning, Implementation, and Applications. PhD thesis, Computer Science Department, New York University, New York, New York, August 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. PPS, Université Paris VII, Denis Diderot Case 7014, 2 place Jussieu, F-75251, Paris Cedex 05, France

    Vincent Balat

  2. BRICS Department of Computer Science, University of Aarhus, Ny Munkegade, Building 540, DK-8000, Aarhus C, Denmark

    Olivier Danvy

Authors
  1. Vincent Balat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olivier Danvy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Sciences, University of Texas at Austin, 2.124 Taylor Hall, TX, 78712, Austin, USA

    Don Batory

  2. Department of Telecommunications, ENSEIRB, University of Paris IV, 1, Ave. du Docteur Albert Schweitzer, 33402, Talence, France

    Charles Consel

  3. Department of Computer Science, Rice University, Mail Stop 132, 6100 S. Main Street, 77005-1892, Houston, Texas, USA

    Walid Taha

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Balat, V., Danvy, O. (2002). Memoization in Type-Directed Partial Evaluation. In: Batory, D., Consel, C., Taha, W. (eds) Generative Programming and Component Engineering. GPCE 2002. Lecture Notes in Computer Science, vol 2487. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45821-2_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-45821-2_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44284-4

  • Online ISBN: 978-3-540-45821-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation