Ezgi Çiçek
ABSTRACT
Incremental computation aims to speed up re-runs of a program after its inputs have been modified slightly. It works by recording a trace of the program's first run and propagating changes through the trace in incremental runs, trying to re-use as much of the original trace as possible. The recent work CostIt is a type and effect system to establish the time complexity of incremental runs of a program, as a function of input changes. However, CostIt is limited in two ways. First, it prohibits input changes that influence control flow. This makes it impossible to type programs that, for instance, branch on inputs that may change. Second, the soundness of CostIt is proved relative to an abstract cost semantics, but it is unclear how the semantics can be realized.
In this paper, we address both these limitations. We present DuCostIt, a re-design of CostIt, that combines reasoning about costs of change propagation and costs of from-scratch evaluation. The latter lifts the restriction on control flow changes. To obtain the type system, we refine Flow Caml, a type system for information flow analysis, with cost effects. Additionally, we inherit from CostIt index refinements to track data structure sizes and a co-monadic type. Using a combination of binary and unary step-indexed logical relations, we prove DuCostIt's cost analysis sound relative to not only an abstract cost semantics, but also a concrete semantics, which is obtained by translation to an ML-like language.
- A type theory for incremental computational complexity with control flow changes (technical appendix). Online at http://www. mpi-sws.org/~ecicek/ducostit_appendix.pdf.Google Scholar
- U. A. Acar. Self-Adjusting Computation. PhD thesis, Department of Computer Science, Carnegie Mellon University, 2005. Google ScholarDigital Library
- U. A. Acar, G. E. Blelloch, and R. Harper. Adaptive functional programming. ACM Trans. Program. Lang. Syst., 28(6), 2006. Google ScholarDigital Library
- U. A. Acar, G. E. Blelloch, M. Blume, R. Harper, and K. Tangwongsan. An experimental analysis of self-adjusting computation. ACM Trans. Program. Lang. Syst., 32(1):3:1–3:53, 2009. Google ScholarDigital Library
- A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the 15th European Conference on Programming Languages and Systems, ESOP’06, pages 69–83, 2006. Google ScholarDigital Library
- Y. Cai, P. G. Giarrusso, T. Rendel, and K. Ostermann. A theory of changes for higher-order languages: Incrementalizing λ-calculi by static differentiation. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, pages 145–155, 2014. Google ScholarDigital Library
- M. Carlsson. Monads for incremental computing. In Proceedings of the 7th International Conference on Functional Programming, ICFP ’02, pages 26–35, 2002. Google ScholarDigital Library
- Y. Chen, J. Dunfield, and U. A. Acar. Type-directed automatic incrementalization. In Proceedings of the 33rd Conference on Programming Language Design and Implementation, PLDI ’12, pages 299– 310, 2012. Google ScholarDigital Library
- Y. Chen, J. Dunfield, M. A. Hammer, and U. A. Acar. Implicit selfadjusting computation for purely functional programs. J. Functional Programming, 24(1):56–112, 2014.Google ScholarCross Ref
- W.-N. Chin and S.-C. Khoo. Calculating sized types. In Proceedings of the Workshop on Partial Evaluation and Semantics-based Program Manipulation, PEPM ’00, pages 62–72, 1999. Google ScholarDigital Library
- E. Çiçek, D. Garg, and U. A. Acar. Refinement types for incremental computational complexity. In Programming Languages and Systems - 24th European Symposium on Programming Proceedings, pages 406– 431, 2015.Google Scholar
- U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, LICS ’11, pages 133–142, 2011. Google ScholarDigital Library
- U. Dal lago and B. Petit. The geometry of types. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL ’13, pages 167–178, 2013. Google ScholarDigital Library
- N. Danner, D. R. Licata, and R. Ramyaa. Denotational cost semantics for functional languages with inductive types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 140–151, 2015. Google ScholarDigital Library
- M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL ’13, pages 357–370, 2013. Google ScholarDigital Library
- S. Gulwani, K. K. Mehra, and T. Chilimbi. Speed: Precise and efficient static estimation of program computational complexity. In Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL ’09, pages 127–139, 2009. Google ScholarDigital Library
- M. A. Hammer, U. A. Acar, and Y. Chen. Ceal: A C-based language for self-adjusting computation. In Proceedings of the 2009 Conference on Programming Language Design and Implementation, PLDI ’09, pages 25–37, 2009. Google ScholarDigital Library
- M. A. Hammer, K. Y. Phang, M. Hicks, and J. S. Foster. Adapton: Composable, demand-driven incremental computation. In Proceedings of the 35th Conference on Programming Language Design and Implementation, PLDI ’14, pages 156–166, 2014. Google ScholarDigital Library
- A. Heydon, R. Levin, and Y. Yu. Caching function calls using precise dependencies. In Proceedings of the Conference on Programming Language Design and Implementation, PLDI ’00, pages 311–320, 2000. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. In Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL ’11, pages 357–370, 2011. Google ScholarDigital Library
- J. Hughes and L. Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In Proceedings of the Fourth International Conference on Functional Programming, ICFP ’99, pages 70–81, 1999. Google ScholarDigital Library
- C. Koch. Incremental query evaluation in a ring of databases. In Proceedings of the Twenty-ninth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’10, pages 87–98, 2010. Google ScholarDigital Library
- R. Ley-Wild, U. A. Acar, and M. Fluet. A cost semantics for selfadjusting computation. In Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL ’09, pages 186–199, 2009. Google ScholarDigital Library
- Y. A. Liu and T. Teitelbaum. Systematic derivation of incremental programs. Science of Computer Programming, 24(1):1–39, 1995. Google ScholarDigital Library
- R. Paige and S. Koenig. Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst., 4(3):402–454, 1982. Google ScholarDigital Library
- F. Pottier and V. Simonet. Information flow inference for ML. ACM Trans. Prog. Lang. Sys., 25(1):117–158, 2003. Google ScholarDigital Library
- P. B. Vasconcelos and K. Hammond. Inferring cost equations for recursive, polymorphic and higher-order functional programs. In Implementation of Functional Languages, 15th International Workshop, IFL 2003, pages 86–101, 2003. Google ScholarDigital Library
- H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of the 26th Symposium on Principles of Programming Languages, POPL ’99, pages 214–227, 1999. Google ScholarDigital Library
Index Terms
- A type theory for incremental computational complexity with control flow changes
Recommendations
A type theory for incremental computational complexity with control flow changes
ICFP '16Incremental computation aims to speed up re-runs of a program after its inputs have been modified slightly. It works by recording a trace of the program's first run and propagating changes through the trace in incremental runs, trying to re-use as much ...
Computational higher-dimensional type theory
POPL '17Formal constructive type theory has proved to be an effective language for mechanized proof. By avoiding non-constructive principles, such as the law of the excluded middle, type theory admits sharper proofs and broader interpretations of results. From ...
Gradual type theory
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based ...
Comments