Implicit self-adjusting computation for purely functional programs

Abstract

Computational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. Self-adjusting programs have been shown to be efficient for a reasonably broad range of problems but the approach still requires an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create and operate on data that can change over time.

We describe techniques for automatically translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer need only annotate the (top-level) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well-typed self-adjusting programs and preserves the source program's input-output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program.

References

1. M. Abadi, B. W. Lampson, and J.-J. Lévy. Analysis and caching of dependencies. In International Conference on Functional Programming, pages 83--91, 1996.
2. U. A. Acar, G. E. Blelloch, and R. Harper. Adaptive functional programming. ACM Trans. Prog. Lang. Sys., 28 (6): 990--1034, 2006.
3. U. A. Acar, A. Ihler, R. Mettu, and O. Sümer. Adaptive Bayesian inference. In Neural Information Processing Systems (NIPS), 2007.
4. U. A. Acar, G. E. Blelloch, M. Blume, R. Harper, and K. Tangwongsan. An experimental analysis of self-adjusting computation. ACM Trans. Prog. Lang. Sys., 32 (1): 3:1--3:53, 2009.
5. U. A. Acar, G. E. Blelloch, R. Ley-Wild, K. Tangwongsan, and D. Türkoğlu. Traceable data types for self-adjusting computation. In Programming Language Design and Implementation, 2010a.
6. U. A. Acar, A. Cotter, B. Hudson, and D. Türkoğlu. Dynamic well-spaced point sets. In Symposium on Computational Geometry, 2010b.
7. M. Carlsson. Monads for incremental computing. In International Conference on Functional Programming, pages 26--35, 2002.
8. Y. Chen, J. Dunfield, M. A. Hammer, and U. A. Acar. Online appendix to Implicit Self-Adjusting Computation for Purely Functional Programs, 2011. https://www.cs.queensu.ca/~jana/Chen11appendix.pdf.
9. Y.-J. Chiang and R. Tamassia. Dynamic algorithms in computational geometry. Proceedings of the IEEE, 80 (9): 1412--1434, 1992.
10. K. Crary, A. Kliger, and F. Pfenning. A monadic analysis of information flow security with mutable state. Journal of Functional Programming, 15 (2): 249--291, Mar. 2005.
11. L. Damas and R. Milner. Principal type-schemes for functional programs. In Principles of Programming Languages, pages 207--212. ACM, 1982.
12. A. Demers, T. Reps, and T. Teitelbaum. Incremental evaluation of attribute grammars with application to syntax-directed editors. In Principles of Programming Languages, pages 105--116, 1981.
13. C. Demetrescu, I. Finocchi, and G. Italiano. Handbook on Data Structures and Applications, chapter 36: Dynamic Graphs. CRC Press, 2005.
14. J. Field and T. Teitelbaum. Incremental reduction in the lambda calculus. In ACM Conf. LISP and Functional Programming, pages 307--322, 1990.
15. J. S. Foster, R. Johnson, J. Kodumal, and A. Aiken. Flow-insensitive type qualifiers. ACM Trans. Prog. Lang. Sys., 28: 1035--1087, 2006.
16. L. Guibas. Modeling motion. In J. Goodman and J. O'Rourke, editors, Handbook of Discrete and Computational Geometry, pages 1117--1134. Chapman and Hall/CRC, 2nd edition, 2004.
17. M. A. Hammer, U. A. Acar, and Y. Chen. CEAL: a C-based language for self-adjusting computation. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2009.
18. N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Principles of Programming Languages (POPL '98), pages 365--377, 1998.
19. R. Ley-Wild, M. Fluet, and U. A. Acar. Compiling self-adjusting programs with continuations. In Proceedings of the International Conference on Functional Programming, 2008.
20. R. Ley-Wild, U. A. Acar, and M. Fluet. A cost semantics for self-adjusting computation. In Proceedings of the 26th Annual ACM Symposium on Principles of Programming Languages, 2009.
21. MLton. MLton web site. http://www.mlton.org.
22. A. C. Myers. JFlow: practical mostly-static information flow control. In Principles of Programming Languages, pages 228--241, 1999.
23. M. Odersky, M. Sulzmann, and M. Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5 (1): 35--55, 1999.
24. F. Pottier and V. Simonet. Information flow inference for ML. ACM Trans. Prog. Lang. Sys., 25 (1): 117--158, Jan. 2003.
25. W. Pugh and T. Teitelbaum. Incremental computation via function caching. In Principles of Programming Languages, pages 315--328, 1989.
26. G. Ramalingam and T. Reps. A categorized bibliography on incremental computation. In Principles of Programming Languages, pages 502--510, 1993.
27. A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE J. Selected Areas in Communications, 21 (1), 2003.
28. D. Sands. Calculi for Time Analysis of Functional Programs. PhD thesis, University of London, Imperial College, September 1990.
29. 995)P. M. Sansom and S. L. Peyton Jones. Time and space profiling for non-strict, higher-order functional languages. In Principles of Programming Languages, pages 355--366, 1995.
30. A. Shankar and R. Bodik. DITTO: Automatic incrementalization of data structure invariant checks (in Java). In Programming Language Design and Implementation, 2007.
31. V. Simonet. Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. In APLAS, pages 283--302, 2003.
32. D. Spoonhower, G. E. Blelloch, R. Harper, and P. B. Gibbons. Space profiling for parallel functional programs. In International Conference on Functional Programming, 2008.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features

      • Language types

        • Functional languages

• Theory of computation

  • Semantics and reasoning

    • Program constructs