Tag Elimination and Jones-Optimality

(Preliminary Report)
  • Walid Taha
  • Henning Makholm
  • John Hughes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2053)


Tag elimination is a program transformation for removing unnecessary tagging and untagging operations from automatically generated programs. Tag elimination was recently proposed as having immediate applications in implementations of domain specific languages (where it can give a two-fold speedup), and may provide a solution to the long standing problem of Jones-optimal specialization in the typed setting. This paper explains in more detail the role of tag elimination in the implementation of domain-specific languages, presents a number of significant simplifications and a high-level, higher-order, typed self-applicable interpreter. We show how tag elimination achieves Jones-optimality.


Type Versus Partial Evaluation Partial Evaluator Extensional Semantic Substitution Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Olivier Danvy. A simple solution to type specialization. In 25th International Colloquium on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science, Aalborg, 1998.CrossRefGoogle Scholar
  2. [2]
    Fritz Henglein and Jakob Rehof. Safe polymorphic type inference for a dynamically typed language: Translating Scheme to ML. In Proceedings of the International Conference on Functional Programming Languages and Computer Architecture (FPCA), La Jolla, 1995. ACM Press.Google Scholar
  3. [3]
    John Hughes. Type specialization. ACM Computing Surveys, 30(3es), 1998.Google Scholar
  4. [4]
    John Hughes. The correctness of type specialisation. In European Symposium on Programming (ESOP), 2000.Google Scholar
  5. [5]
    Neil D. Jones. Challenging problems in partial evaluation and mixed computation. In D. Bjørner, A. P. Ershov, and N. D. Jones, editors, Partial Evaluation and Mixed Computation, pages 1–14, North-Holland, 1988. IFIP World Congress Proceedings, Elsevier Science Publishers B.V.Google Scholar
  6. [6]
    Neil D. Jones, Carsten K Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.Google Scholar
  7. [7]
    Henning Makholm. On Jones-optimal specialization for strongly typed languages. In [13], pages 129–148, 2000.CrossRefGoogle Scholar
  8. [8]
    John C. Mitchell. On abstraction and the expressive power of programming languages. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, volume 526 of Lecture Notes in Computer Science, pages 290–310. Springer-Verlag, 1991.Google Scholar
  9. [9]
    Torben Mogensen. Inherited limits. In Partial Evaluation: Practice and Theory, volume 1706 of Lecture Notes in Computer Science, pages 189–202. Springer-Verlag, 1999.Google Scholar
  10. [10]
    Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard. An idealized MetaML: Simpler, and more expressive. In European Symposium on Programming (ESOP), volume 1576 of Lecture Notes in Computer Science, pages 193–207. Springer-Verlag, 1999.Google Scholar
  11. [11]
    Frank Pfenning and Peter Lee. LEAP: A language with eval and polymorphism. In Josep Díaz and Fernando Orejas, editors, TAPSOFT’89: Proceedings of the International Joint Conference on Theory and Practice of Software Development,, volume 352 of Lecture Notes in Computer Science, pages 345–359. Springer-Verlag, 1989.Google Scholar
  12. [12]
    Brian Cantwell Smith. Reflection and Semantics in a Procedural Language. PhD thesis, Massachusetts Institute of Technology, 1982.Google Scholar
  13. [13]
    Walid Taha, editor. Semantics, Applications, and Implementation of Program Generation, volume 1924 of Lecture Notes in Computer Science, Montréal, 2000. Springer-Verlag.zbMATHGoogle Scholar
  14. [14]
    Walid Taha. A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trivial. In Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Maniplation (PEPM), Boston, 2000. ACM Press.Google Scholar
  15. [15]
    Walid Taha and Henning Makholm. Tag elimination — or — type specialisation is a type-indexed effect. In Subtyping and Dependent Types in Programming, APPSEM Workshop. INRIA technical report, 2000.Google Scholar
  16. [16]
    Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. In Proceedings of the Symposium on Partial Evaluation and Semantic-Based Program Manipulation (PEPM), pages 203–217, Amsterdam, 1997. ACM Press.CrossRefGoogle Scholar
  17. [17]
    Mitchell Wand. The theory of fexprs is trivial. Lisp and Symbolic Computation, 10:189–199, 1998.CrossRefGoogle Scholar
  18. [18]
    Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  19. [19]
    Zhe Yang. Encoding types in ML-like languages. In Proceedings of the International Conference on Functional Programming (ICFP), pages 289–300, Baltimore, 1998. ACM Press.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Walid Taha
    • 1
  • Henning Makholm
    • 2
  • John Hughes
    • 3
  1. 1.Department of Computer ScienceYale UniversityNew HavenUSA
  2. 2.DIKU, University of CopenhagenCopenhagenDenmark
  3. 3.Department of Computing SciencesChalmers, GöteborgSweden

Personalised recommendations