Skip to main content
SpringerLink
Log in

Meta-programming with Typed Object-Language Representations

  • Conference paper
Generative Programming and Component Engineering (GPCE 2004)

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

Abstract

We present two case studies demonstrating the use of type-equality constraints in a meta-language to enforce semantic invariants of object-language programs such as scoping and typing rules. We apply this technique to several interesting problems, including (1) the construction of tagless interpreters; (2) statically checking de Bruijn indices involving pattern-based binding constructs; and (3) evolving embedded DSL implementations to include domain-specific types and optimizations that respect those types.

The work described in this paper is supported by the National Science Foundation under the grant CCR-0098126.

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. Cheney, J., Hinze, R.: First class phantom types. Technical Report CUCIS TR2003-1901, Cornell University (2003), http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901

  2. Sheard, T., Benaissa, Z., Pašalić, E.: DSL implementation using staging and monads. In: Second Conference on Domain-Specific Languages (DSL 1999), Austin, Texas, USEUNIX (1999)

    Google Scholar 

  3. Taha, W., Makholm, H., Hughes, J.: Tag elimination and jones-optimality. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, p. 257. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Pašalić, E., Taha, W., Sheard, T.: Tagless staged interpreters for typed languages. In: The International Conference on Functional Programming (ICFP 2002), Pittsburgh, USA, ACM, New York (2002)

    Google Scholar 

  5. Bruijn, N.G.d.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagaciones Mathematische 34, 381–392 (1972); This also appeared in the Proceedings of the Koninklijke Nederlandse Akademie van Wetenschappen, Amsterdam, series A, 75(5)

    Google Scholar 

  6. Baars, A.I., Swierstra, S.D.: Typing dynamic typing. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP 2002), Pittsburgh, Pennsylvania, USA, October 4-6 (2002); SIGPLAN Notices 37(9), ACM Press (2002)

    Google Scholar 

  7. Cheney, J., Hinze, R.: Phantom types (2003), Available from http://www.informatik.uni-bonn.de/~ralf/publications/Phantom.pdf

  8. Weirich, S.: Type-safe cast: functional pearl. In: Proceedings of the ACM Sigplan International Conference on Functional Programming (ICFP 2000). ACM Sigplan Notices, vol. 35(9), pp. 58–67. ACM Press, New York (2000)

    Chapter  Google Scholar 

  9. Nordström, B., Peterson, K., Smith, J.M.: Programming in Martin-Lof’s Type Theory. International Series of Monographs on Computer Science, vol. 7. Oxford University Press, New York (1990); Currently available online from first authors homepage

    Google Scholar 

  10. Sheard, T., Pasalic, E., Linger, R.N.: The ωmega implementation. Available on request from the author (2003)

    Google Scholar 

  11. Jones, M.P.: Qualified Types: Theory and Practice. PhD thesis, Oxford University, Also available as Programming Research Group technical report 106 (1992)

    Google Scholar 

  12. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the ACM 27, 356–364 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  13. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 214–227. ACM, New York (1999)

    Chapter  Google Scholar 

  14. Taha, W., Sheard, T.: MetaML: Multi-stage programming with explicit annotations. Theoretical Computer Science 248 (2000)

    Google Scholar 

  15. Taha, W., Calcagno, C., Huang, L., Leroy, X.: MetaOCaml: A compiled, type-safe multi-stage programming language (2001), Available from http://cs-www.cs.yale.edu/homes/taha/MetaOCaml/

  16. Sheard, T., Jones, S.P.: Template meta-programming for Haskell. ACM SIGPLAN Notices 37, 60–75 (2002)

    Article  Google Scholar 

  17. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993), Avaiable online from http://www.dina.dk/~sestoft

    MATH  Google Scholar 

  18. 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 

  19. Huang, L., Taha, W.: A practical implementation of tag elimination (2002) (in preperation)

    Google Scholar 

  20. Sheard, T., Linger, N.: Search-based binding time analysis using type-directed pruning. In: Proceedings of the ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM), pp. 20–31. ACM Press, New York (2002)

    Google Scholar 

  21. Linger, N., Sheard, T.: Binding-time analysis for metaml via type inference and constraint solving. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  22. Cheney, J., Hinze, R.: A lightweight implementation of generics and dynamics. In: Proc. of the workshop on Haskell, pp. 90–104. ACM Press, New York (2002)

    Chapter  Google Scholar 

  23. Leijen, D., Meijer, E.: Domain-specific embedded compilers. In: Proceedings of the 2nd Conference on Domain-Specific Languages, Berkeley, CA, USENIX Association, pp. 109–122 (1999)

    Google Scholar 

  24. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Norris, C., Fenwick, J.J.B. (eds.) Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2003). ACM SIGPLAN Notices, vol. 38(1), pp. 224–235. ACM Press, New York (2003)

    Chapter  Google Scholar 

  25. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Proceedings Symposium on Logic in Computer Science, Washington, pp. 194–204. IEEE Computer Society Press, Los Alamitos (1987); The conference was held at Cornell University, Ithaca, New York

    Google Scholar 

  26. Pfenning, F., Schürmann, C.: System description: Twelf – A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  27. Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J., Giménez, E., Herbelin, H., Huet, G., Muñoz, C., Murthy, C., Parent, C., Paulin, C., Saíbi, A., Werner, B.: The Coq Proof Assistant Reference Manual – Version V6.1. Technical Report 0203, INRIA (1997)

    Google Scholar 

  28. Augustsson, L., Carlsson, M.: An exercise in dependent types: A well-typed interpreter. In: Workshop on Dependent Types in Programming, Gothenburg (1999), Available online from www.cs.chalmers.se/~augustss/cayenne/interp.ps

  29. Chen, C., Xi, H.: Meta-Programming through Typeful Code Representation. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden, pp. 275–286 (2003)

    Google Scholar 

  30. Hudak, P.: Building domain-specific embedded languages. ACM Computing Surveys 28, 196 (1996)

    Article  Google Scholar 

  31. Elliott, C., Finne, S., de Moor, O.: Compiling embedded languages. Journal of Functional Programming 8, 543–572 (1998)

    Article  MathSciNet  Google Scholar 

  32. Rhiger, M.: A foundation for embedded languages. ACM Transactions on Programming Languages and Systems TOPLAS 25, 291–315 (2003)

    Article  Google Scholar 

  33. Benaissa, Z.E.A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: λν, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming 6, 699–722 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  34. Jones, M.P.: The hugs 98 user manual (2000)

    Google Scholar 

  35. Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: Czarnecki, K., Pfenning, F., Smaragdakis, Y. (eds.) Generative Programming and Component Engineering (GPCE). LNCS, Springer, Heidelberg (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. OGI School of Science & Engineering, Oregon Health & Science University,  

    Emir Pašalić & Nathan Linger

Authors
  1. Emir Pašalić
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nathan Linger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Software Integrated Systems, Vanderbilt University, P.O. Box 1829, 37235, Sta. B. Nashville, TN, USA

    Gabor Karsai

  2. Software Engineering Research Group, Delft University of Technology, The Netherlands

    Eelco Visser

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pašalić, E., Linger, N. (2004). Meta-programming with Typed Object-Language Representations. In: Karsai, G., Visser, E. (eds) Generative Programming and Component Engineering. GPCE 2004. Lecture Notes in Computer Science, vol 3286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30175-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30175-2_8

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-30175-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation