Implementing typeful program transformations

ABSTRACT

The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct programs, for representing object programs, that is, the programs in the object language on which the program transformation is to be performed. In practice, most representations chosen for typed object programs are typeless in the sense that the type of an object program cannot be reflected in the type of its representation. This is unsatisfactory as such typeless representations make it impossible to capture in the type system of the meta language various invariants in a program transformation that are related to the types of object programs. In this paper, we propose an approach to implementing program transformations that makes use of a first-order typeful program representation formed in Dependent ML (DML), where the type of an object program as well as the types of the free variables in the object program can be reflected in the type of the representation of the object program. We introduce some programming techniques needed to handle this typeful program representation, and then present an implementation of a CPS transform function where the relation between the type of an object program and that of its CPS transform is captured in the type system of DML. In a broader context, we claim to have taken a solid step along the line of research on constructing certifying compilers.

REFERENCES

• 1: M. Abadi, L. Cardelli, Curien, P.-L., and Lévy, J.-J. Explicit substitutions. Journal of Functional Programming, 1(4):375--416, 1991.
• 2: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 3: L. Augustsson and M. Carlsson. An excercise in dependent types: A well-typed interpreter, 1999. Available as http://www.cs.chalmers.se/˜augustss/cayenne/interp.ps
• 4: Arthur I. Baars , S. Doaitse Swierstra, Typing dynamic typing, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.157-166, October 04-06, 2002, Pittsburgh, PA, USA
• 5: Olivier Danvy , Morten Rhiger, A Simple Take on Typed Abstract Syntax in Haskell-like Languages, Proceedings of the 5th International Symposium on Functional and Logic Programming, p.343-358, March 07-09, 2001
• 6: N. G. de Bruijn. Lambda calculus notation with nameless dummies. Indagationes mathematicae, 34:381--392, 1972.
• 7: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 8: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 9: Albert R. Meyer , Mitchell Wand, Continuation Semantics in Typed Lambda-Calculi (Summary), Proceedings of the Conference on Logic of Programs, p.219-224, June 17-19, 1985
• 10: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 11: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 12: 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
• 13: Emir PašaliΕ , Walid Taha , Tim Sheard, Tagless staged interpreters for typed languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.218-229, October 04-06, 2002, Pittsburgh, PA, USA
• 14: S. Peyton Jones et al. Haskell 98 -- A non-strict, purely functional language. Available at http://www.haskell.org/onlinereport/, Feb. 1999.
• 15: 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
• 16: G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125--159, December 1975.
• 17: Carsten Schürmann , Frank Pfenning, Automated Theorem Proving in a Simple Meta-Logic for LF, Proceedings of the 15th International Conference on Automated Deduction: Automated Deduction, p.286-300, July 05-10, 1998
• 18: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 19: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, 1998
• 20: H. Xi. Dependent ML. Available at http://www.cs.bu.edu/˜hwxi/DML/DML.html, 2001.
• 21: 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.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

General Terms:
Languages, Theory

Keywords:
CPS, DML, continuation-passing style, dependent ML, dependent types, typeful program transformation