Skip to main content
SpringerLink
Log in

Finally Tagless, Partially Evaluated

Tagless Staged Interpreters for Simpler Typed Languages

  • Conference paper
Book cover Programming Languages and Systems (APLAS 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4807))

Included in the following conference series:

Abstract

We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers.

Our main idea is to encode HOAS de Bruijn or higher-order abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations.

Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck. To achieve self hyp interpretation and show Jones hyp optimality, we relate this exemplar of higher-rank and higher-kind polymorphism (provided by ML functors and Haskell 98 constructor classes) to plugging a term into a context of let hyp polymorphic bindings.

We thank Martin Sulzmann and Walid Taha for helpful discussions. Sam Staton, Pieter Hofstra, and Bart Jacobs kindly provided some useful references. We thank anonymous reviewers for pointers to related work.

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. Asai, K.: Binding-time analysis for both static and dynamic expressions. New Generation Computing 20(1), 27–52 (2001)

    Article  Google Scholar 

  2. Baars, A.I., Swierstra, S.D.: Typing dynamic typing. In: ICFP, pp. 157–166 (2002)

    Google Scholar 

  3. Balat, V., Di Cosmo, R., Fiore, M.P.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: POPL, pp. 64–76 (2004)

    Google Scholar 

  4. Benton, P.N.: Embedded interpreters. JFP 15(4), 503–542 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware design in Haskell. In: ICFP, pp. 174–184 (1998)

    Google Scholar 

  6. Calcagno, C., Moggi, E., Taha, W.: ML-like inference for classifiers. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 79–93. Springer, Heidelberg (2004)

    Google Scholar 

  7. Danvy, O.: Type-directed partial evaluation. In: POPL, pp. 242–257 (1996)

    Google Scholar 

  8. Danvy, O., López, P.E.M.: Tagging, encoding, and Jones optimality. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, pp. 335–347. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001)

    Article  MathSciNet  Google Scholar 

  10. Fiore, M.P.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: PPDP, pp. 26–37 (2002)

    Google Scholar 

  11. Fogarty, S., Pasalic, E., Siek, J., Taha, W.: Concoqtion: Indexed types now! In: PEPM (2007)

    Google Scholar 

  12. Glück, R.: Jones optimality, binding-time improvements, and the strength of program specializers. In: ASIA-PEPM, pp. 9–19 (2002)

    Google Scholar 

  13. Harper, R., Morrisett, J.G.: Compiling polymorphism using intensional type analysis. In: POPL, pp. 130–141 (1995)

    Google Scholar 

  14. Hinze, R., Jeuring, J., Löh, A.: Type-indexed data types. Science of Computer Programming 51(1–2), 117–151 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  15. Honsell, F., Lenisa, M.: Coinductive characterizations of applicative structures. Math. Structures in Comp. Sci. 9(4), 403–435 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  16. Hudak, P.: Building domain-specific embedded languages. ACM Comp. Surv. 28(4es), 196 (1996)

    Article  Google Scholar 

  17. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  18. Läufer, K., Odersky, M.: Self-interpretation and reflection in a statically typed language. In: OOPSLA\(\slash\)ECOOP Workshop on Object-Oriented Reflection and Metalevel Architectures (1993)

    Google Scholar 

  19. MetaOCaml http://www.metaocaml.org

  20. Miller, D., Nadathur, G.: A logic programming approach to manipulating formulas and programs. In: IEEE Symp. on Logic Programming, pp. 379–388 (1987)

    Google Scholar 

  21. Nanevski, A., Pfenning, F.: Staged computation with names and necessity. JFP 15(6), 893–939 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  22. Oliveira, B.C.d.S., Gibbons, J.: TypeCase: A design pattern for type-indexed functions. In: Haskell Workshop, pp. 98–109 (2005)

    Google Scholar 

  23. Pašalić, E., Taha, W., Sheard, T.: Tagless staged interpreters for typed languages. In: ICFP, pp. 157–166 (2002)

    Google Scholar 

  24. Peyton Jones, S.L., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: ICFP, pp. 50–61 (2006)

    Google Scholar 

  25. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI, pp. 199–208 (1988)

    Google Scholar 

  26. Pfenning, F., Lee, P.: Metacircularity in the polymorphic λ-calculus. Theor. Comp. Sci. 89(1), 137–159 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  27. Ramsey, N.: ML module mania: A type-safe, separately compiled, extensible interpreter. In: ML Workshop (2005)

    Google Scholar 

  28. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proc. ACM Natl. Conf. vol. 2, 717–740 Repr. with a foreword in HOSC 11(4) 363–397 (1972)

    Google Scholar 

  29. Rhiger, M.: Higher-Order Program Generation. PhD thesis, BRICS, Denmark (2001)

    Google Scholar 

  30. Shao, Z.: Typed cross-module compilation. In: ICFP, pp. 141–152 (1998)

    Google Scholar 

  31. Sperber, M., Thiemann, P.: Two for the price of one: Composing partial evaluation and compilation. In: PLDI, pp. 215–225 (1997)

    Google Scholar 

  32. Sumii, E., Kobayashi, N.: A hybrid approach to online and offline partial evaluation. HOSC 14(2–3), 101–142 (2001)

    MATH  Google Scholar 

  33. Taha, W., Makholm, H., Hughes, J.: Tag elimination and Jones-optimality. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 257–275. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  34. Taha, W., Nielsen, M.F.: Environment classifiers. In: POPL, pp. 26–37 (2003)

    Google Scholar 

  35. Thiemann, P.: Cogen in six lines. In: ICFP, pp. 180–189 (1996)

    Google Scholar 

  36. Washburn, G., Weirich, S.: Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. In: ICFP, pp. 249–262 (2003)

    Google Scholar 

  37. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL, pp. 224–235 (2003)

    Google Scholar 

  38. Yang, Z.: Encoding types in ML-like languages. In: ICFP, pp. 289–300 (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. McMaster University,  

    Jacques Carette

  2. FNMOC,  

    Oleg Kiselyov

  3. Rutgers University,  

    Chung-chieh Shan

Authors
  1. Jacques Carette
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oleg Kiselyov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Chung-chieh Shan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Zhong Shao

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Carette, J., Kiselyov, O., Shan, Cc. (2007). Finally Tagless, Partially Evaluated. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-76637-7_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-76636-0

  • Online ISBN: 978-3-540-76637-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation