Typed self-representation

ABSTRACT

Self-representation -- the ability to represent programs in their own language -- has important applications in reflective languages and many other domains of programming language design. Although approaches to designing typed program representations for sublanguages of some base language have become quite popular recently, the question whether a fully metacircular typed self-representation is possible is still open. This paper makes a big step towards this aim by defining the F_ω* calculus, an extension of the higher-order polymorphic lambda calculus F_ω that allows typed self-representations. While the usability of these representations for metaprogramming is still limited, we believe that our approach makes a significant step towards a new generation of reflective languages that are both safe and efficient.

REFERENCES

• 1: Thorsten Altenkirch , Conor McBride, Generic Programming within Dependently Typed Programming, Proceedings of the IFIP TC2/WG2.1 Working Conference on Generic Programming, p.1-20, July 11-12, 2002
• 2: Brian Aydemir , Arthur Charguéraud , Benjamin C. Pierce , Randy Pollack , Stephanie Weirich, Engineering formal metatheory, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 3: H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 4: S. Berardi. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Technical report, Department of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino, 1988.
• 5: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 6: C. Böhm and A. Berarducci. Automatic synthesis of typed lambda-programs on term algebras. Theor. Comput. Sci., 39:135--154, 1985.
• 7: J. Carette, O. Kiselyov, and C. Shan. Finally tagless, partially evaluated. In APLAS'07, extended version to appear in Journal of Functional Programming, pages 222--238. Springer LNCS 4807, 2007.
• 8: T. Coquand. An analysis of Girard's paradox. In Symposium on Logic in Computer Science, pages 227--236. IEEE Computer Society Press, 1986.
• 9: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Journal of the ACM (JACM), v.48 n.3, p.555-604, May 2001 [doi>10.1145/382780.382785]
• 10: N.G. de Bruijn. Lambda calculus notation with nameless dummies. a tool for automatic formula manipulation with application to the church-rosser theorem. Indagationes Mathematicae, 34:381--392, 1972.
• 11: Leonidas Fegaras , Tim Sheard, Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space), Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.284-294, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237792]
• 12: J.Y. Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thése de doctorat detat, Université de Paris VII, 1972.
• 13: Masami Hagiya, Meta-circular interpreter for a strongly typed language, Journal of Symbolic Computation, v.8 n.6, p.651-680, Dec. 1989 [doi>10.1016/S0747-7171(89)80066-5]
• 14: 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]
• 15: Ralf Hinze , Johan Jeuring , Andres Löh, Type-indexed data types, Science of Computer Programming, v.51 n.1-2, p.117-151, May 2004 [doi>10.1016/j.scico.2003.07.001]
• 16: Christian Hofer , Klaus Ostermann , Tillmann Rendel , Adriaan Moors, Polymorphic embedding of dsls, Proceedings of the 7th international conference on Generative programming and component engineering, October 19-23, 2008, Nashville, TN, USA [doi>10.1145/1449913.1449935]
• 17: K. Läufer and M. Odersky. Self-interpretation and reflection in a statically typed language. In Proc. OOPSLA Workshop on Reflection and Metalevel Architectures. ACM, Oct. 1993.
• 18: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 19: Aleksandar Nanevski, Meta-programming with names and necessity, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.206-217, October 04-06, 2002, Pittsburgh, PA, USA
• 20: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
• 21: Frank Pfenning , Peter Lee, Metacircularity in the polymorphic &lgr;-calculus, Theoretical Computer Science, v.89 n.1, p.137-159, Oct. 21, 1991
• 22: Frank Pfenning , Christine Paulin-Mohring, Inductively Defined Types in the Calculus of Constructions, Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics, p.209-228, March 29-April 01, 1989
• 23: M. B. Reinhold, TYPECHECKING IS UNDECIDABLE WHEN ''TYPE'' IS A TYPE, Massachusetts Institute of Technology, Cambridge, MA, 1989
• 24: 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]
• 25: Jeffrey Mark Siskind , Barak A. Pearlmutter, First-class nonstandard interpretations by opening closures, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 26: Brian Cantwell Smith, Reflection and semantics in LISP, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-35, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800513]
• 27: Guy L. Steele, Jr., Growing a Language, Higher-Order and Symbolic Computation, v.12 n.3, p.221-236, October 1999 [doi>10.1023/A:1010085415024]
• 28: 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
• 29: J. Terlouw. Een nadere bewijstheoretische analyse van GSTT's. Technical report, Department of Computer Science, Catholic University, Nijmegen, The Netherlands, 1989.
• 30: Geoffrey Washburn , Stephanie Weirich, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism*, Journal of Functional Programming, v.18 n.1, p.87-140, January 2008 [doi>10.1017/S0956796807006557]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages, Theory

Keywords:
lambda calculus, language design, reflection, self interpretation, types