Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-29T01:26:05.766Z Has data issue: false hasContentIssue false
  • English
  • Français

Implicit self-adjusting computation for purely functional programs

Part of: JFP Research Articles

Published online by Cambridge University Press:  31 March 2014

YAN CHEN ,
JANA DUNFIELD ,
MATTHEW A. HAMMER  and
UMUT A. ACAR
YAN CHEN
Affiliation:
Max Planck Institute for Software Systems, Kaiserslautern and Saarbrücken, Germany (e-mails: [email protected], [email protected])
JANA DUNFIELD
Affiliation:
Max Planck Institute for Software Systems, Kaiserslautern and Saarbrücken, Germany (e-mails: [email protected], [email protected])
MATTHEW A. HAMMER
Affiliation:
University of Maryland, College Park, MD, USA (e-mail: [email protected])
UMUT A. ACAR
Affiliation:
Carnegie Mellon University, Pittsburgh, PA, USA and INRIA Paris-Rocquencourt, Paris, France (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Articles
Information
Journal of Functional Programming , Volume 24 , Issue 1 , January 2014 , pp. 56 - 112
Copyright
Copyright © Cambridge University Press 2014 

References

Abadi, M., Lampson, B. W. & Lévy, J.-J. (1996) Analysis and caching of dependencies. In International Conference on Functional Programming, Philadelphia, PA. New York, NY: ACM Press, pp. 83–91.Google Scholar
Acar, U. A., Blelloch, G. E., Blume, M., Harper, R. & Tangwongsan, K. (2006a) A library for self-adjusting computation. Electron. Notes Theor. Comput. Sci. 148 (2), 127–154.Google Scholar
Acar, U. A., Blelloch, G. E., Blume, M., Harper, R. & Tangwongsan, K. (2009) An experimental analysis of self-adjusting computation. ACM Trans. Prog. Lang. Syst. 32 (1), 31–53.Google Scholar
Acar, U. A., Blelloch, G. E. & Harper, R. (2006b) Adaptive functional programming. ACM Trans. Prog. Lang. Syst. 28 (6), 990–1034.Google Scholar
Acar, U. A., Blelloch, G. E., Ley-Wild, R., Tangwongsan, K. & Türkoğlu, D. (2010a) Traceable data types for self-adjusting computation. In Programming Language Design and Implementation. New York, NY: ACM Press, pp. 483–496.Google Scholar
Acar, U. A., Cotter, A., Hudson, B. & Türkoğlu, D. (2010b) Dynamic well-spaced point sets. In Symposium on Computational Geometry. New York, NY: ACM Press, pp. 756–773.Google Scholar
Barendregt, H., Coppo, M. & Dezani-Ciancaglini, M. (1983) A filter lambda model and the completeness of type assignment. J. Symb. Log. 48 (4), 931–940.Google Scholar
Bellman, R. (1957) Dynamic Programming. Princeton, NJ: Princeton University Press.Google Scholar
Burchett, K., Cooper, G. H. & Krishnamurthi, S. (2007) Lowering: A static optimization technique for transparent functional reactivity. In Partial Evaluation and Semantics-Based Program Manipulation. New York, NY: ACM Press, pp. 71–80.Google Scholar
Carlsson, M. (2002) Monads for incremental computing. In International Conference on Functional Programming. New York, NY: ACM Press, pp. 26–35.Google Scholar
Chen, Y., Dunfield, J. & Acar, U. A. (2012) Type-directed automatic incrementalization. In Programming Language Design and Implementation. New York, NY: ACM Press, pp. 299–310.Google Scholar
Chen, Y., Dunfield, J., Hammer, M. A. & Acar, U. A. (2011) Implicit self-adjusting computation for purely functional programs. In International Conference on Functional Programming. New York, NY: ACM Press, pp. 129–141.Google Scholar
Chiang, Y.-J. & Tamassia, R. (1992) Dynamic algorithms in computational geometry. Proc. IEEE 80 (9), 1412–1434.Google Scholar
Cooper, G. H. & Krishnamurthi, S. (2006) Embedding dynamic dataflow in a call-by-value language. In European Symposium on Programming. Berlin, Germany: Springer-Verlag, pp. 294–308.Google Scholar
Crary, K., Kliger, A. & Pfenning, F. (2005) A monadic analysis of information flow security with mutable state. J. Funct. Program. 15 (2), 249–291.Google Scholar
Damas, L. & Milner, R. (1982) Principal type-schemes for functional programs. In Principles of Programming Languages. New York, NY: ACM Press, pp. 207–212.Google Scholar
Demers, A., Reps, T. & Teitelbaum, T. (1981) Incremental evaluation of attribute grammars with application to syntax-directed editors. In Principles of Programming Languages. New York, NY: ACM Press, pp. 105–116.Google Scholar
Demetrescu, C., Finocchi, I. & Italiano, G. F. (2005) Handbook on Data Structures and Applications, Chap. 36: Dynamic Graphs. Boca Raton, FL: CRC Press.Google Scholar
Efremidis, S. G., Reppy, J. H. & Mughal, K. A. (1993) Attribute Grammars in ML. Technical Report 93-1401, Cornell University, Ithaca, NY.Google Scholar
Elliott, C. & Hudak, P. (1997) Functional reactive animation. In International Conference on Functional Programming. New York, NY: ACM Press, pp. 263–273.Google Scholar
Field, J. & Teitelbaum, T. (1990) Incremental reduction in the lambda calculus. In ACM Conference on LISP and Functional Programming, Nice, France. New York, NY: ACM Press, pp. 307–322.Google Scholar
Foster, J. S., Johnson, R., Kodumal, J. & Aiken, A. (2006) Flow-insensitive type qualifiers. ACM Trans. Prog. Lang. Syst. 28, 1035–1087.Google Scholar
Guibas, L. (2004) Modeling motion. In Handbook of Discrete and Computational Geometry, Goodman, J. & O'Rourke, J., (eds), 2nd ed.. Boca Raton, FL: CRC Press, pp. 1117–1134.Google Scholar
Hammer, M. A., Acar, U. A. & Chen, Y. (2009) CEAL: A C-based language for self-adjusting computation. In Programming Language Design and Implementation. New York, NY: ACM Press, pp. 25–37.Google Scholar
Heintze, N. & Riecke, J. G. (1998) The SLam calculus: Programming with secrecy and integrity. In Principles of Programming Languages. New York, NY: ACM Press, pp. 365–377.Google Scholar
Jeffrey, A. (2012) LTL types FRP: Linear-time temporal logic propositions as types, proofs as functional reactive programs. In Workshop on Programming Languages Meets Program Verification. New York, NY: ACM Press, pp. 49–60.Google Scholar
Krishnaswami, N. R. (2013) Higher-order reactive programming without space time leaks. In International Conference on Functional Programming. New York, NY: ACM Press, pp. 221–232.Google Scholar
Ley-Wild, R., Acar, U. A. & Fluet, M. (2009) A cost semantics for self-adjusting computation. In Principles of Programming Languages. New York, NY: ACM Press, pp. 186–199.Google Scholar
Ley-Wild, R., Fluet, M. & Acar, U. A. (2008) Compiling self-adjusting programs with continuations. In International Conference on Functional Programming. New York, NY: ACM Press, pp. 321–334.Google Scholar
Liu, H., Cheng, E. & Hudak, P. (2009) Causal commutative arrows and their optimization. In International Conference on Functional Programming (ICFP '09). New York, NY: ACM Press, pp. 35–46.Google Scholar
Liu, H. & Hudak, P. (2007) Plugging a space leak with an arrow. Electron. Notes Theor. Comput. Sci. 193, 29–45.Google Scholar
Myers, A. C. (1999) JFlow: Practical mostly static information flow control. In Principles of Programming Languages. New York, NY: ACM Press, pp. 228–241.Google Scholar
Nilsson, H. (2005) Dynamic optimization for functional reactive programming using generalized algebraic data types. In International Conference on Functional Programming. New York, NY: ACM Press, pp. 54–65.Google Scholar
Odersky, M., Sulzmann, M. & Wehr, M. (1999) Type inference with constrained types. Theory Pract. Object Syst. 5 (1), 35–55.Google Scholar
Pfenning, F. & Davies, R. (2001) A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11, 511–540.Google Scholar
Pottier, F. & Simonet, V. (2003) Information flow inference for ML. ACM Trans. Prog. Lang. Syst. 25 (1), 117–158.Google Scholar
Pugh, W. & Teitelbaum, T. (1989) Incremental computation via function caching. In Principles of Programming Languages. New York, NY: ACM Press, pp. 315–328.Google Scholar
Ramalingam, G. & Reps, T. (1993) A categorized bibliography on incremental computation. In Principles of Programming Languages. New York, NY: ACM Press, pp. 502–510.Google Scholar
Reps, T. (1982a) Generating Language-Based Environments. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY.Google Scholar
Reps, T. (1982b) Optimal-time incremental semantic analysis for syntax-directed editors. In Principles of Programming Languages. New York, NY: ACM Press, pp. 169–176.Google Scholar
Reps, T. & Teitelbaum, T. (1989) The Synthesizer Generator: A System for Constructing Language-Based Editors. Berlin, Germany: Springer-Verlag.Google Scholar
Sabelfeld, A. & Myers, A. C. (2003) Language-based information-flow security. IEEE J. Sel. Areas Commun. 21 (1), 5–19.Google Scholar
Sands, D. (1990) Calculi for Time Analysis of Functional Programs. PhD thesis, Imperial College, University of London, London, UK.Google Scholar
Sansom, P. M. & Peyton Jones, S. L. (1995) Time and space profiling for non-strict, higher-order functional languages. In Principles of Programming Languages. New York, NY: ACM Press, pp. 355–366.Google Scholar
Sculthorpe, N. & Nilsson, H. (2010) Keeping calm in the face of change. Higher Order Symb. Comput. 23 (2), 227–271.Google Scholar
Shankar, A. & Bodik, R. (2007) DITTO: Automatic incrementalization of data structure invariant checks (in Java). In Programming Language Design and Implementation. New York, NY: ACM Press, pp. 310–319.Google Scholar
Simonet, V. (2003) Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. In Asian Symposium on Programming Languages and Systems. Berlin, Germany: Springer-Verlag, pp. 283–302.Google Scholar
Spoonhower, D., Blelloch, G. E., Harper, R. & Gibbons, P. B. (2008) Space profiling for parallel functional programs. In International Conference on Functional Programming. New York, NY: ACM Press.Google Scholar
Sundaresh, R. S. & Hudak, P. (1991) Incremental compilation via partial evaluation. In Principles of Programming Languages. New York, NY: ACM Press, pp. 1–13.Google Scholar
Wan, Z., Taha, W. & Hudak, P. (2002) Event-driven FRP. In Practical Aspects of Declarative Languages. Berlin, Germany: Springer-Verlag, pp. 155–172.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.