Shifting the stage: staging with delimited control

ABSTRACT

It is often hard to write programs that are efficient yet reusable. For example, an efficient implementation of Gaussian elimination should be specialized to the structure and known static properties of the input matrix. The most profitable optimizations, such as choosing the best pivoting or memoization, cannot be expected of even an advanced compiler because they are specific to the domain, but expressing these optimizations directly makes for ungainly source code. Instead, a promising and popular way to reconcile efficiency with reusability is for a domain expert to write code generators.

Two pillars of this approach are types and effects. Typed multilevel languages such as MetaOCaml ensure _safety_: a well-typed code generator neither goes wrong nor generates code that goes wrong. Side effects such as state and control ease correctness: an effectful generator can resemble the textbook presentation of an algorithm, as is familiar to domain experts, yet insert let for memoization and if for bounds-checking, as is necessary for efficiency. However, adding effects blindly renders multilevel types unsound.

We introduce the first two-level calculus with control effects and a sound type system. We give small-step operational semantics as well as a continuation-passing style (CPS) translation. For soundness, our calculus restricts the code generator's effects to the scope of generated binders. Even with this restriction, we can finally write efficient code generators for dynamic programming and numerical methods in direct style, like in algorithm textbooks, rather than in CPS or monadic style.

REFERENCES

• 1: Asai, Kenichi, and Yukiyoshi Kameyama. 2007. Polymorphic delimited continuations. In APLAS, 239--254. LNCS 4807.
• 2: Anders Bondorf, Improving binding times without explicit CPS-conversion, Proceedings of the 1992 ACM conference on LISP and functional programming, p.1-10, June 22-24, 1992, San Francisco, California, United States
• 3: Anders Bondorf , Olivier Danvy, Automatic autoprojection of recursive equations with global variable and abstract data types, Science of Computer Programming, v.16 n.2, p.151-195, Sept. 1991 [doi>10.1016/0167-6423(91)90002-F]
• 4: Cristiano Calcagno , Eugenio Moggi , Walid Taha, Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.25-36, July 09-15, 2000
• 5: Carette, Jacques, and Oleg Kiselyov. 2008. Multi-stage programming with functors and monads: Eliminating abstraction overhead from generic code. Science of Computer Programming.
• 6: Albert Cohen , Sébastien Donadio , Maria-Jesus Garzaran , Christoph Herrmann , Oleg Kiselyov , David Padua, In search of a program generator to implement generic transformations for high-performance computing, Science of Computer Programming, v.62 n.1, p.25-46, September 2006 [doi>10.1016/j.scico.2005.10.013]
• 7: Czarnecki, Krzysztof, John T. O'Donnell, Jörg Striegnitz, and Walid Taha. 2004. DSL implementation in MetaOCaml, Template Haskell, and C++. In DSPG 2003, 51--72. LNCS 3016.
• 8: Danvy, Olivier, and Andrzej Filinski. 1989. A functional abstraction of typed contexts. Tech. Rep. 89/12, DIKU, University of Copenhagen, Denmark. http://www.daimi.au.dk/~danvy/Papers/fatc.ps.gz.
• 9: Olivier Danvy , Andrzej Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.151-160, June 27-29, 1990, Nice, France [doi>10.1145/91556.91622]
• 10: Danvy, Olivier. 1992. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science 2(4): 361--391.
• 11: R. Davies, A temporal-logic approach to binding-time analysis, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.184, July 27-30, 1996
• 12: Eckhardt, Jason, Roumen Kaiabachev, Emir Pašalic, Kedar N. Swadi, and Walid Taha. 2005. Implicitly heterogeneous multistage programming. In GPCE, 275--292. LNCS 3676.
• 13: Conal Elliott, Programming graphics processors functionally, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, September 22-22, 2004, Snowbird, Utah, USA [doi>10.1145/1017472.1017482]
• 14: M Felleisen , D P Friedman, A reduction semantics for imperative higher-order languages, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.206-223, March 1987, Eindhoven, The Netherlands
• 15: Andrzej Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.446-457, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178047]
• 16: Frigo, Matteo, and Steven G. Johnson. 2005. The design and implementation of FFTW3. Proceedings of the IEEE 93(2):216--231.
• 17: Gomard, Carsten K., and Neil D. Jones. 1991. A partial evaluator for the untyped lambda calculus. Journal of Functional Programming 1(1):21--69.
• 18: Kevin Hammond , Greg Michaelson, Hume: a domain-specific language for real-time embedded systems, Proceedings of the 2nd international conference on Generative programming and component engineering, p.37-56, September 22-25, 2003, Erfurt, Germany
• 19: Yukiyoshi Kameyama , Oleg Kiselyov , Chung-chieh Shan, Closing the stage: from staged code to typed closures, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA [doi>10.1145/1328408.1328430]
• 20: Kiselyov, Oleg. 2006. Native delimited continuations in (byte-code) OCaml. http://okmij.org/ftp/Computation/Continuations.html#caml-shift.
• 21: Oleg Kiselyov , Chung-chieh Shan , Amr Sabry, Delimited dynamic binding, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 22: Kiselyov, Oleg, and Walid Taha. 2005. Relating FFTW and split-radix. In ICESS, 488--493. LNCS 3605.
• 23: Julia L. Lawall , Olivier Danvy, Continuation-based partial evaluation, Proceedings of the 1994 ACM conference on LISP and functional programming, p.227-238, June 27-29, 1994, Orlando, Florida, United States
• 24: Lengauer, Christian, and Walid Taha, eds. 2006. Special issue on the 1st MetaOCaml workshop (2004), vol. 62(1) of Science of Computer Programming.
• 25: Xavier Leroy , François Pessaux, Type-based analysis of uncaught exceptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.340-377, March 2000 [doi>10.1145/349214.349230]
• 26: McAdam, Bruce J. 2001. Y in practical programs. Workshop on fixed points in computer science; http://www.dsi.uniroma1.it/~labella/absMcAdam.ps.
• 27: MetaOCaml. 2006. MetaOCaml. http://www.metaocaml.org.
• 28: Michie, Donald. 1968. "Memo" functions and machine learning. Nature 218:19--22.
• 29: Luc Moreau, A Syntactic Theory of Dynamic Binding, Higher-Order and Symbolic Computation, v.11 n.3, p.233-279, 1998 [doi>10.1023/A:1010087314987]
• 30: F. Nielson , R. H. Nielson, Automatic binding time analysis for a typed &lgr;-calculus, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-106, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73569]
• 31: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 32: Michel Parigot, Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, Proceedings of the International Conference on Logic Programming and Automated Reasoning, p.190-201, July 15-20, 1992
• 33: Pušchel, Emir, Walid Taha, and Tim Sheard. 2002. Tagless staged interpreters for typed languages. In ICFP, 157--166.
• 34: Peyton Jones, Simon L. 2003. The Haskell 98 language and libraries. Journal of Functional Programming 13(1):1--255.
• 35: Pušchel, Markus, José M. F. Moura, Jeremy Johnson, David Padua, Manuela Veloso, Bryan W. Singer, Jianxin Xiong, Franz Franchetti, Aca Gačić, Yevgen Voronenko, Kang Chen, Robert W. Johnson, and Nick Rizzolo. 2005. SPIRAL: Code generation for DSP transforms. Proceedings of the IEEE 93(2): 232--275.
• 36: Sørensen, Morten Heine B., Robert Glück, and Neil D. Jones. 1994. Towards unifying deforestation, supercompilation, partial evaluation, and generalized partial computation. In ESOP, 485--500. LNCS 788.
• 37: Eijiro Sumii , Naoki Kobayashi, A Hybrid Approach to Online and Offline Partial Evaluation, Higher-Order and Symbolic Computation, v.14 n.2-3, p.101-142, September 2001 [doi>10.1023/A:1012984529382]
• 38: Swadi, Kedar, Walid Taha, and Oleg Kiselyov. 2005. Dynamic programming benchmark. http://www.metaocaml.org/examples/dp/
• 39: Kedar Swadi , Walid Taha , Oleg Kiselyov , Emir Pasalic, A monadic approach for avoiding code duplication when staging memoized functions, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina [doi>10.1145/1111542.1111570]
• 40: 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
• 41: Taha, Walid. 2005. Resource-aware programming. In ICESS, 38--43. LNCS 3605.
• 42: Walid Taha , Michael Florentin Nielsen, Environment classifiers, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-37, January 15-17, 2003, New Orleans, Louisiana, USA
• 43: Talpin, Jean-Pierre, and Pierre Jouvelot. 1992. Polymorphic type, region and effect inference. Journal of Functional Programming 2(3):245--271.
• 44: Hayo Thielecke, From control effects to typed continuation passing, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.139-149, January 15-17, 2003, New Orleans, Louisiana, USA
• 45: Peter Thiemann, Combinators for program generation, Journal of Functional Programming, v.9 n.5, p.483-525, September 1999 [doi>10.1017/S0956796899003469]
• 46: Thiemann, Peter, and Dirk Dussart. 1999. Partial evaluation for higher-order languages with state. http://www.informatik.uni-freiburg.de/~thiemann/papers/mlpe.ps.gz.
• 47: Wadler, Philip L. 1992. Comprehending monads. Mathematical Structures in Computer Science 2(4):461--493.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Design, Languages

Keywords:
code generation, continuations, delimited control, multilevel languages, mutable state, side effects, staged programming