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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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.
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.
Vincent Balat. PhD thesis, PPS, Université Paris VII-Denis Diderot, Paris, France, 2002. Forthcoming.
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.
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.
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.
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.
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.
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.
Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231–247, 1992.
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.
Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75–94, 1997.
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.
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.
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.
Olivier Danvy, Morten Rhiger, and Kristoffer Rose. Normalization by evaluation with typed abstract syntax. Journal of Functional Programming, 11(6):673–680, 2001.
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.
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.
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.
Roberto Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485–525, 1993.
Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.
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/.
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.
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.
Yoshihiko Futamura, Kenroku Nogi, and Akihiko Takano. Essence of generalized partial computation. Theoretical Computer Science, 90(1):61–79, 1991.
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
Bernd Grobauer. Topics in Semantics-based Program Manipulation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-6.
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.
R. Gurevič. Equational theory of positive numbers with exponentiation. Proceedings of the American Mathematical Society, 94(1):135–141, May 1985.
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.
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.
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/.
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.
Donald Michie. ‘Memo’ functions and machine learning. Nature, 218:19–22, April 1968.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.
Larry C. Paulson. ML for the Working Programmer (2nd edition). Cambridge University Press, 1996.
Morten Rhiger. Higher-Order Program Generation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-4.
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.
Mikael Rittri. Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University of Göteborg, Göteborg, Sweden, 1990.
Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71–89, 1991.
Colin Runciman and Ian Toyn. Retrieving re-usable software components by polymorphic type. Journal of Functional Programming, 1(2):191–211, 1991.
Sergei V. Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387–1400, 1983.
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.
Jeffrey D. Ullman. Elements of ML Programming (ML 97 edition). Prentice-Hall, 1998.
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).
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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