Tagless staged interpreters for typed languages

ABSTRACT

Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or mor.Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. .To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (called Meta-D) and prove its type safety. To formalize Meta-D, we extend Shao, Saha, Trifonov and Papaspyrou's λH language to a multi-level setting. Building on λH allows us to demonstrate type safety in a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work needed for establishing the soundness of that system.

REFERENCES

• 1: Lennart Augustsson. Cayenne -- a language with dependent types. Available from http://www.cs.chalmers.se/~augustss/cayenne.
• 2: Lennart Augustsson and Magnus Carlsson. 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.
• 3: Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University Press, Oxford, 1991.
• 4: Jon Bentley, Programming pearls: little languages, Communications of the ACM, v.29 n.8, p.711-721, Aug. 1986 [doi>10.1145/6424.315691]
• 5: Luca Cardelli. Phase distinctions in type theory. Unpublished manuscript available online from author's homepage, 1988.
• 6: Thierry Coquand, Bengt Nordström, Jan~M. Smith, and Bjorne von Sydow. Type theory and programming. Bulletin of the European Association for Theoretical Computer Science, 52:203--228, February 1994. Columns: Logic in Computer Science.
• 7: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• 8: Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
• 9: Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
• 10: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.258-270, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237788]
• 11: Peter Dybjer. Inductively defined sets in Martin-Löf's set theory. In A. Avron, R. Harper, F. Honsell, I. Mason, and G. Plotkin, editors, Workshop on General Logic, February 1987.
• 12: Peter Dybjer. Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Preliminary Proc. of 1st Int. Workshop on Logical Frameworks, Antibes, France, 7--11 May 1990, pages 213--230. 1990. ftp://ftp.inria.fr/INRIA/Projects/coq/types/Proceedings/\\book90.ps.Z.
• 13: Peter Dybjer, Inductive sets and families in Martin-Lo¨f's type theory and their set-theoretic semantics, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 14: Peter Dybjer. Inductive families. Formal Aspects of Computing, 6(4):440--465, 1994.
• 15: Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525--549, 2000.
• 16: Peter Dybjer and Anton Setzer. Finite axiomatizations of inductive and inductive-recursive definitions. In R. Backhouse and T. Sheard, editors, Informal Proc. of Workshop on Generic Programming, WGP'98, Marstrand, Sweden, 18 June 1998. Dept. of Computing Science, Chalmers Univ. of Techn., and Göteborg Univ., June 1998. Electronic version available at http://wsinwp01.win.tue.nl:1234/WGPProceedings/.
• 17: Eduardo Giménez. A tutorial on recursive types in Coq. Technical Report TR-0221, INRIA Rocquencourt, May 1998.
• 18: Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
• 19: Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Proceedings Symposium on Logic in Computer Science, pages 194--204, Washington, 1987. IEEE Computer Society Press. The conference was held at Cornell University, Ithaca, New York.
• 20: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 21: Liwen Huang and Walid Taha. A practical implementation of tag elimination. In preperation.
• 22: Paul Hudak, Building domain-specific embedded languages, ACM Computing Surveys (CSUR), v.28 n.4es, Dec. 1996 [doi>10.1145/242224.242477]
• 23: P. Hudak, Modular Domain Specific Languages and Tools, Proceedings of the 5th International Conference on Software Reuse, p.134, June 02-05, 1998
• 24: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 25: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 26: Henning Makholm, On Jones-Optimal Specialization for Strongly Typed Languages, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, p.129-148, September 20, 2000
• 27: Meta-D: A dependently typed multi-stage language. Available online from http://www.cse.ogi.edu/~pasalic/metad/, 2002.
• 28: MetaOCaml: A compiled, type-safe multi-stage programming language. Available online from http://cs-www.cs.yale.edu/homes/taha/MetaOCaml/, 2001.
• 29: Torben Æ. Mogensen, Inherited Limits, Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, p.189-202, June 29-July 10, 1998
• 30: Eugenio Moggi , Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, An Idealized MetaML: Simpler, and More Expressive, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.193-207, March 22-28, 1999
• 31: Bengt Nordström, Programming in Constructive Set Theory: Some examples, Proceedings of the 1981 conference on Functional programming languages and computer architecture, p.141-154, October 18-22, 1981, Portsmouth, New Hampshire, United States [doi>10.1145/800223.806773]
• 32: Bengt Nordström, Kent Peterson, and Jan M. Smith. Programming in Martin-Lof's Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, New York, NY, 1990. Currently available online from first authors homepage.
• 33: Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000,USA. Available online from ftp://cse.ogi.edu/pub/tech-reports/README.html.
• 34: Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. Research report RR 92-49, Laboratoire de l'Informatique du Parallélisme, Ecole normale supérieure de Lyon, December 1992.
• 35: Christine Paulin-Mohring, Inductive Definitions in the system Coq - Rules and Properties, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.328-345, March 16-18, 1993
• 36: Emir Pašalic, Walid Taha, and Tim Sheard. Tagless staged interpreters for typed languages (formal development). Technical Report 02-006, OGI, 2002. Available from {33}.
• 37: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 38: Frank Pfenning , Peter Lee, LEAP: A Language with Eval And Polymorphism, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.345-359, March 13-17, 1989
• 39: Benjamin C. Pierce, Basic category theory for computer scientists, MIT Press, Cambridge, MA, 1991
• 40: Calton Pu, Andrew Black, Crispin Cowan, and Jonathan Walpole. Microlanguages for operating system specialization. In Proceedings of the Workshop on Domain-Specific Languages, Paris, 1997.
• 41: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 42: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 43: Zhong Shao , Andrew W. Appel, A type-based compiler for standard ML, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.116-129, June 18-21, 1995, La Jolla, California, United States
• 44: Zhong Shao , Bratin Saha , Valery Trifonov , Nikolaos Papaspyrou, A type system for certified binaries, ACM SIGPLAN Notices, v.37 n.1, p.217-232, Jan. 2002
• 45: Tim Sheard , Zine-el-abidine Benaissa , Emir Pasalic, DSL implementation using staging and monads, Proceedings of the 2nd conference on Domain-specific languages, p.81-94, October 03-06, 1999, Austin, Texas, United States
• 46: Mark Shields , Tim Sheard , Simon Peyton Jones, Dynamic typing as staged type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.289-302, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268970]
• 47: Yannis Smaragdakis and Don Batory. DiSTiL: A transformation library for data structures. In USENIX Conference on Domain-Specific Languages, October 1997.
• 48: Walid Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, 1999
• 49: Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, September 2000
• 50: Walid Taha, A sound reduction semantics for untyped CBN mutli-stage computation. Or, the theory of MetaML is non-trival (extended abstract), Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.34-43, January 22-23, 2000, Boston, Massachusetts, United States
• 51: Walid Taha , Zine-El-Abidine Benaissa , Tim Sheard, Multi-Stage Programming: Axiomatization and Type Safety, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.918-929, July 13-17, 1998
• 52: Walid Taha , Paul Hudak , Zhanyong Wan, Directions in Functional Programming for Real(-Time) Applications, Proceedings of the First International Workshop on Embedded Software, p.185-203, October 08-10, 2001
• 53: 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.
• 54: Walid Taha , Henning Makholm , John Hughes, Tag Elimination and Jones-Optimality, Proceedings of the Second Symposium on Programs as Data Objects, p.257-275, May 21-23, 2001
• 55: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 56: R. D. Tennent, Principles of Programming Languages, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 57: Valery Trifonov , Bratin Saha , Zhong Shao, Fully reflexive intensional type analysis, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.82-93, September 2000
• 58: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 59: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
• 60: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Languages, Performance

Keywords:
calculus of constructions, definitional interpreters, domain-specific languages, multi-stage programming