Skip to main content
SpringerLink
Log in

Typed Tagless Final Interpreters

  • Chapter
Generic and Indexed Programming

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7470))

Abstract

The so-called ‘typed tagless final’ approach of [6] has collected and polished a number of techniques for representing typed higher-order languages in a typed metalanguage, along with type-preserving interpretation, compilation and partial evaluation. The approach is an alternative to the traditional, or ‘initial’ encoding of an object language as a (generalized) algebraic data type. Both approaches permit multiple interpretations of an expression, to evaluate it, pretty-print, etc. The final encoding represents all and only typed object terms without resorting to generalized algebraic data types, dependent or other fancy types. The final encoding lets us add new language forms and interpretations without breaking the existing terms and interpreters.

These lecture notes introduce the final approach slowly and in detail, highlighting extensibility, the solution to the expression problem, and the seemingly impossible pattern-matching. We develop the approach further, to type-safe cast, run-time-type representation, Dynamics, and type reconstruction. We finish with telling examples of type-directed partial evaluation and encodings of type-and-effect systems and linear lambda-calculus.

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 49.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.: On typing delimited continuations: Three new solutions to the printf problem. Higher-Order and Symbolic Computation 22(3), 275–291 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  2. Atkey, R.: Syntax for Free: Representing Syntax with Binding Using Parametricity. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 35–49. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Atkey, R., Lindley, S., Yallop, J.: Unembedding domain-specific languages. In: Weirich, S. (ed.) Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, pp. 37–48. ACM Press, New York (2009)

    Chapter  Google Scholar 

  4. Baars, A.I., Swierstra, S.D.: Typing dynamic typing. In: [21], pp. 157–166 (2002)

    Google Scholar 

  5. Böhm, C., Berarducci, A.: Automatic synthesis of typed Λ-programs on term algebras. Theoretical Computer Science 39, 135–154 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  6. Carette, J., Kiselyov, O., Shan, C.-c.: Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming 19(5), 509–543 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  7. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5(2), 56–68 (1940)

    Article  MathSciNet  MATH  Google Scholar 

  8. Danvy, O.: Functional unparsing. Journal of Functional Programming 8(6), 621–625 (1998)

    Article  MATH  Google Scholar 

  9. Danvy, O.: Lecture notes on type-directed partial evaluation (1999), http://www.brics.dk/~danvy/tdpe-ln.pdf

  10. Danvy, O., Filinski, A.: Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  11. Ertl, A.: Threaded code (2008), http://www.complang.tuwien.ac.at/forth/threaded-code.html

  12. Fischer, S., Kiselyov, O., Shan, C.-c.: Purely functional lazy non-deterministic programming. In: Hutton, G., Tolmach, A.P. (eds.) ICFP 2009: Proceedings of the ACM International Conference on Functional Programming, pp. 11–22. ACM Press, New York (2009)

    Chapter  Google Scholar 

  13. Garrigue, J.: Code reuse through polymorphic variants. In: Workshop on Foundations of Software Engineering (2000)

    Google Scholar 

  14. Gries, D. (ed.): Programming methodology: A collection of articles by members of IFIP WG 2.3. Springer, Berlin (1978)

    Google Scholar 

  15. Guillemette, L.-J., Monnier, S.: A typepreserving compiler in Haskell. In: Hook, J., Thiemann, P. (eds.) ICFP 2008: Proceedings of the ACM International Conference on Functional Programming. ACM SIGPLAN Notices, vol. 43(9), pp. 75–86. ACM Press, New York (2008)

    Chapter  Google Scholar 

  16. Gunter, C.A., Mitchell, J.C.: Theoretical aspects of object-oriented programming: Types, semantics, and language design. MIT Press, Cambridge (1994)

    MATH  Google Scholar 

  17. Hall, C.V., Hammond, K., Peyton-Jones, S.L., Wadler, P.L.: Type classes in Haskell. ACM Transactions on Programming Languages and Systems 18(2), 109–138 (1996)

    Article  Google Scholar 

  18. Hinze, R.: Formatting: A class act. Journal of Functional Programming 13(5), 935–944 (2003)

    Article  MATH  Google Scholar 

  19. Hofer, C., Ostermann, K., Rendel, T., Moors, A.: Polymorphic embedding of DSLs. In: Smaragdakis, Y., Siek, J.G. (eds.) Proceedings of GPCE 2008: 7th International Conference on Generative Programming and Component Engineering, pp. 137–147. ACM Press, New York (2008)

    Chapter  Google Scholar 

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

    Google Scholar 

  21. ICFP, ICFP 2002: Proceedings of the ACM International Conference on Functional Programming. ACM Press, New York (2002)

    Google Scholar 

  22. Johann, P., Ghani, N.: Foundations for structured programming with GADTs. In: Necula, G.C., Wadler, P. (eds.) POPL 2008: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 297–308. ACM Press, New York (2008)

    Chapter  Google Scholar 

  23. Kamin, S.: Final data types and their specification. ACM Transactions on Programming Languages and Systems 5(1), 97–121 (1983)

    Article  MATH  Google Scholar 

  24. Lämmel, R., Kiselyov, O.: Exploring typed language design in Haskell: Lecture 1. Haskell’s take on the Expression Problem (2010), http://userpages.uni-koblenz.de/~laemmel/TheEagle/

  25. Lämmel, R., Kiselyov, O.: Lecture 2: Spin-offs from the Expression Problem (2010), http://userpages.uni-koblenz.de/~laemmel/TheEagle/resources/xproblem2.html

  26. Magi, S.: Mobile code in C# via finally tagless interpreters (2009), http://higherlogics.blogspot.com/2009/06/mobile-code-in-c-via-finally-tagless.html

  27. McAdam, B.J.: Y in practical programs. In: Workshop on Fixed Points in Computer Science (2001), http://www.dsi.uniroma1.it/~labella/absMcAdam.ps

  28. Miller, D., Nadathur, G.: A logic programming approach to manipulating formulas and programs. In: Haridi, S. (ed.) IEEE Symposium on Logic Programming, pp. 379–388. IEEE Computer Society Press, Washington, DC (1987)

    Google Scholar 

  29. Mu, S.-C.: Typed λ-Calculus Interpreter in Agda (2008), http://www.iis.sinica.edu.tw/~scm/2008/typed-lambda-calculus-interprete/

  30. Oliveira, B.C.d.S., Gibbons, J.: TypeCase: A design pattern for type-indexed functions. In: Proceedings of the 2005 Haskell Workshop, pp. 98–109. ACM Press, New York (2005)

    Chapter  Google Scholar 

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

    Google Scholar 

  32. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI 1988: Proceedings of the ACM Conference on Programming Language Design and Implementation. ACM SIGPLAN Notices, vol. 23(7), pp. 199–208. ACM Press, New York (1988)

    Chapter  Google Scholar 

  33. Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science 5, 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  34. Pogodalla, S.: Abstract Categorial Grammar homepage, http://www.loria.fr/equipes/calligramme/acg

  35. Reynolds, J.C.: User-defined types and procedural data structures as complementary approaches to data abstraction. In: Schuman, S.A. (ed.) New Directions in Algorithmic Languages. IFIP Working Group 2.1 on Algol, Rocquencourt, pp. 157–168. INRIA, France (1975); Also in [14, 309–317], [16, 13–23]

    Google Scholar 

  36. Swierstra, W.: Data types á la carte. Journal of Functional Programming 18(4), 423–436 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  37. Szabó, Z.G.: Compositionality. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (Winter 2008)

    Google Scholar 

  38. Thiemann, P.: Combinators for program generation. Journal of Functional Programming 9(5), 483–525 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  39. Thiemann, P., Sulzmann, M.: Tag-Free Combinators for Binding-Time Polymorphic Program Generation. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 87–102. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  40. Wadler, P.: The expression problem. Message to java-genericity electronic mailing list (1998), http://www.daimi.au.dk/~madst/tool/papers/expression.txt

  41. Wand, M.: Final algebra semantics and data type extensions. Journal of Computer and System Sciences 19(1), 27–44 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  42. Washburn, G.A., Weirich, S.: Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. Journal of Functional Programming 18(1), 87–140 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  43. Weirich, S.: Encoding Intensional Type Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 92–106. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  44. Weirich, S.: Typechecking into GADT (2004), http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs

  45. Weirich, S.: Type-safe run-time polytypic programming. Journal of Functional Programming 16(6), 751–791 (2006)

    Article  MathSciNet  Google Scholar 

  46. Winskel, G.: Formal semantics of programming languages. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

  47. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL 2003: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 224–235. ACM Press, New York (2003)

    Google Scholar 

  48. Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI 1998: Proceedings of the ACM Conference on Programming Language Design and Implementation. ACM SIGPLAN Notices, vol. 33(5), pp. 249–257. ACM Press, New York (1998)

    Chapter  Google Scholar 

  49. Yang, Z.: Encoding types in ML-like languages. In: ICFP 1998: Proceedings of the ACM International Conference on Functional Programming. ACM SIGPLAN Notices, vol. 34(1), pp. 289–300. ACM Press, New York (1998)

    Chapter  Google Scholar 

Download references

Authors
  1. Oleg Kiselyov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Jeremy Gibbons

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Kiselyov, O. (2012). Typed Tagless Final Interpreters. In: Gibbons, J. (eds) Generic and Indexed Programming. Lecture Notes in Computer Science, vol 7470. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32202-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32202-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32201-3

  • Online ISBN: 978-3-642-32202-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation