Abstract
Through the use of conditional compilation and related tools, many software projects can be used to generate a huge number of related programs. The problem of typing such variational software is difficult. The brute-force strategy of generating all variants and typing each one individually is: (1) usually infeasible for efficiency reasons and (2) produces results that do not map well to the underlying variational program. Recent research has focused mainly on efficiency and addressed only the problem of type checking. In this work we tackle the more general problem of variational type inference and introduce variational types to represent the result of typing a variational program. We introduce the variational lambda calculus (VLC) as a formal foundation for research on typing variational programs. We define a type system for VLC in which VLC expressions are mapped to correspondingly variational types. We show that the type system is correct by proving that the typing of expressions is preserved over the process of variation elimination, which eventually results in a plain lambda calculus expression and its corresponding type. We identify a set of equivalence rules for variational types and prove that the type unification problem modulo these equivalence rules is unitary and decidable; we also present a sound and complete unification algorithm. Based on the unification algorithm, the variational type inference algorithm is an extension of algorithm W. We show that it is sound and complete and computes principal types. We also consider the extension of VLC with sum types, a necessary feature for supporting variational data types, and demonstrate that the previous theoretical results also hold under this extension. Finally, we characterize the complexity of variational type inference and demonstrate the efficiency gains over the brute-force strategy.
- Abrahams, D. and Gurtovoy, A. 2004. C++ Template Metaprogramming: Concepts, Tools, and Techniques from Boost and Beyond. Addison-Wesley Professional. Google ScholarDigital Library
- Anantharaman, S., Narendran, P., and Rusinowitch, M. 2004. Unification modulo ACUI plus homomorphisms/distributivity. J. Autom. Reason. 33, 1--28. Google ScholarDigital Library
- Apel, S. and Hutchins, D. 2008. A calculus for uniform feature composition. ACM Trans. Program. Lang. Syst. 32, 5, 19:1--19:33. Google ScholarDigital Library
- Apel, S. and Kästner, C. 2009. An overview of feature-oriented software development. J. Object Technol. 8, 5, 49--84.Google ScholarCross Ref
- Apel, S., Kästner, C., and Lengauer, C. 2008. Feature featherweight java: A calculus for feature-oriented programming and stepwise refinement. In Proceedings of the International Conference on Generative Programming and Component Engineering. 101--112. Google ScholarDigital Library
- Apel, S., Kästner, C., Größlinger, A., and Lengauer, C. 2010. Type safety for feature-oriented product lines. Autom. Softw. Engin. 17, 3, 251--300. Google ScholarDigital Library
- Apel, S., von Rhein, A., Wendler, P., Größlinger, A., and Beyer, D. 2013. Strategies for product-line verification: Case studies and experiments. In Proceedings of the IEEE International Conference on Software Engineering. To appear. Google ScholarDigital Library
- Austern, M. H. 1998. Generic Programming and the STL: Using and Extending the C++ Standard Template Library. Addison-Wesley Longman. Google ScholarDigital Library
- Aversano, L., Penta, M. D., and Baxter, I. D. 2002. Handling preprocessor-conditioned declarations. In Proceedings of the International Workshop on Source Code Analysis and Manipulation. 83--92. Google ScholarDigital Library
- Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press. Google ScholarDigital Library
- Baader, F. and Snyder, W. 2001. Unification theory. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov Eds., North Holland, 445--532.Google Scholar
- Balat, V., Cosmo, R. D., and Fiore, M. P. 2004. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 64--76. Google ScholarDigital Library
- Batory, D., Sarvela, J. N., and Rauschmayer, A. 2004. Scaling step-wise refinement. IEEE Trans. Softw. Engin. 30, 6, 355--371. Google ScholarDigital Library
- Brabrand, C., Ribeiro, M., Tolêdo, T., and Borba, P. 2012. Intraprocedural dataflow analysis for software product lines. In Proceedings of the International Conference on Aspect-Oriented Software Development (AOSD’12). 13--24. Google ScholarDigital Library
- Bracha, G. and Cook, W. 1990. Mixin-based inheritance. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 303--311. Google ScholarDigital Library
- Chae, W. and Blume, M. 2008. Building a family of compilers. In Proceedings of the International Software Product Line Conference (SPLC’08). 307--316. Google ScholarDigital Library
- Chen, S. and Erwig, M. 2014. Counter-factual typing for debugging type errors. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. To appear. Google ScholarDigital Library
- Chen, S., Erwig, M., and Walkingshaw, E. 2012. An error-tolerant type system for variational lambda calculus. In Proceedings of the ACM International Conference on Functional Programming. 29--40. Google ScholarDigital Library
- Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., and Raskin, J.-F. 2010. Model checking lots of systems: Efficient verification of temporal properties in software product lines. In Proceedings of the IEEE International Conference on Software Engineering (ICSE’10). 335--344. Google ScholarDigital Library
- Classen, A., Heymans, P., Schobbens, P.-Y., and Legay, A. 2011. Symbolic model checking of software product lines. In Proceedings of the IEEE International Conference on Software Engineering (ICSE’11). 321--330. Google ScholarDigital Library
- Cordy, M., Classen, A., Perrouin, G., Schobbens, P.-Y., Heymans, P., and Legay, A. 2012. Simulation-based abstractions for software product-line model checking. In Proceedings of the IEEE International Conference on Software Engineering (ICSE’12). 672--682. Google ScholarDigital Library
- Czarnecki, K. and Eisenecker, U. W. 2000. Generative Programming: Methods, Tools, and Applications. Addison-Wesley. Google ScholarDigital Library
- Damas, L. and Milner, R. 1982. Principal type schemes for functional programming languages. In Proceedings of the 9th ACM Symposium on Principles of Programming Languages. 207--208. Google ScholarDigital Library
- Das, M. 2000. Unification-based pointer analysis with directional assignments. In Proceedings of the ACM SIGPLAN Conference on Programming language Design and Implementation (PLDI’00). 35--46. Google ScholarDigital Library
- Delaware, B., Cook, W., and Batory, D. 2009a. A machine-checked model of safe composition. In Proceedings of the Workshop on Foundations of Aspect-Oriented Languages. 31--35. Google ScholarDigital Library
- Delaware, B., Cook, W. R., and Batory, D. 2009b. Fitting the pieces together: A machine-checked model of safe composition. In Proceedings of the ACM SIGSOFT International Symposium on the Foundations of Software Engineering. 243--252. Google ScholarDigital Library
- Delaware, B., Cook, W., and Batory, D. 2011. Product lines of theorems. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11). 595--608. Google ScholarDigital Library
- Dezani-Ciancaglini, M., Ghilezan, S., and Venneri, B. 1997. The “relevance” of intersection and union types. Notre Dame J. Formal Logic 38, 2, 246--269.Google ScholarCross Ref
- Disenfeld, C. and Katz, S. 2012. A closer look at aspect interference and cooperation. In Proceedings of the International Conference on Aspect-Oriented Software Development (AOSD’12). 107--118. Google ScholarDigital Library
- Dos Reis, G. and Stroustrup, B. 2006. Specifying C++ concepts. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 295--308. Google ScholarDigital Library
- Downey, P. J., Sethi, R., and Tarjan, R. E. 1980. Variations on the common subexpression problem. J. ACM 27, 4, 758--771. Google ScholarDigital Library
- Elrad, T., Filman, R. E., and Bader, A. 2001. Aspect-oriented programming. Comm. ACM 44, 10, 28--32. Google ScholarDigital Library
- Erwig, M. and Walkingshaw, E. 2011. The choice calculus: A representation for software variation. ACM Trans. Softw. Engin. Methodol. 21, 1, 6:1--6:27. Google ScholarDigital Library
- Fähndrich, M., Carbin, M., and Larus, J. R. 2006. Reflective program generation with patterns. In Proceedings of the International Conference on Generative Programming and Component Engineering (GPCE’06). 275--284. Google ScholarDigital Library
- Flatt, M. and PLT. 2010. Reference: Racket. Tech. rep. PLT-TR-2010-1, PLT Inc. http://racket-lang.org/tr1/.Google Scholar
- Fogarty, S., Pasalic, E., Siek, J., and Taha, W. 2007. Concoqtion: Indexed types now! In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’07). 112--121. Google ScholarDigital Library
- Garcia, R. 2008. Static computation and reflection. Ph.D. thesis, Indiana University. http://d2i.indiana.edu/sites/default/files/Static_Computation_and_Reflection.pdf. Google ScholarDigital Library
- Garcia, R. and Lumsdaine, A. 2009. Toward foundations for type-reflective metaprogramming. In Proceedings of the International Conference on Generative Programming and Component Engineering (GPCE’09). 25--34. Google ScholarDigital Library
- Gazzillo, P. and Grimm, R. 2012. SuperC: Parsing all of C by taming the preprocessor. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’12). 323--334. Google ScholarDigital Library
- GNU Project. 2009. The C preprocessor. Free software foundation. http://gcc.gnu.org/onlinedocs/cpp/.Google Scholar
- Goldman, M., Katz, E., and Katz, S. 2010. Maven: Modular aspect verification and interference analysis. Formal Methods in Syst. Des. 37, 1, 61--92. Google ScholarDigital Library
- Gregor, D., Järvi, J., Siek, J., Stroustrup, B., Dos Reis, G., and Lumsdaine, A. 2006. Concepts: Linguistic support for generic programming in C++. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’06). 291--310. Google ScholarDigital Library
- Huang, S. S. and Smaragdakis, Y. 2008. Expressive and safe static reflection with MorphJ. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’08). 79--89. Google ScholarDigital Library
- Huang, S. S. and Smaragdakis, Y. 2011. Morphing: Structurally shaping a class by reflecting on others. ACM Trans. Program. Lang. Syst. 33, 2, 6:1--6:44. Google ScholarDigital Library
- Huang, S. S., Zook, D., and Smaragdakis, Y. 2005. Statically safe program generation with safegen. In Proceedings of the International Conference on Generative Programming and Component Engineering (GPCE’05). 309--326. Google ScholarDigital Library
- Huang, S. S., Zook, D., and Smaragdakis, Y. 2007. CJ: Enhancing java with safe type conditions. In Proceedings of the International Conference on Aspect-Oriented Software Development. 185--198. Google ScholarDigital Library
- Järvi, J., Gregor, D., Willcock, J., Lumsdaine, A., and Siek, J. 2006. Algorithm specialization in generic programming: Challenges of constrained generics in C++. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’06). 272--282. Google ScholarDigital Library
- Johann, P. and Ghani, N. 2008. Foundations for structured programming with GADTs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08). 297--308. Google ScholarDigital Library
- Kagawa, K. 2006. Polymorphic variants in Haskell. In Proceedings of the ACM SIGPLAN Workshop on Haskell. 37--47. Google ScholarDigital Library
- Kang, K. C., Cohen, S. G., Hess, J. A., Novak, W. E., and Peterson, A. S. 1990. Feature-oriented domain analysis (FODA) feasibility study. Tech. rep. CMU/SEI-90-TR-21, Software Engineering Institute, Carnegie Mellon University.Google Scholar
- Kästner, C., Apel, S., and Kuhlemann, M. 2008. Granularity in software product lines. In Proceedings of the IEEE International Conference on Software Engineering. 311--320. Google ScholarDigital Library
- Kästner, C., Giarrusso, P. G., Rendel, T., Erdweg, S., Ostermann, K., and Berger, T. 2011. Variability-aware parsing in the presence of lexical macros and conditional compilation. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11). 805--824. Google ScholarDigital Library
- Kästner, C., Apel, S., Thüm, T., and Saake, G. 2012a. Type checking annotation-based product lines. ACM Trans. Softw. Engin. Methodol. 21, 3, 14:1--14:39. Google ScholarDigital Library
- Kästner, C., Ostermann, K., and Erdweg, S. 2012b. A variability-aware module system. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 773--792. Google ScholarDigital Library
- Kenner, A., Kästner, C., Haase, S., and Leich, T. 2010. TypeChef: Toward type checking #ifdef variability in C. In Proceedings of the International Workshop on Feature-Oriented Software Development. 25--32. Google ScholarDigital Library
- Kim, C. H. P., Kästner, C., and Batory, D. 2008. On the modularity of feature interactions. In Proceedings of the International Conference on Generative Programming and Component Engineering. 19--23. Google ScholarDigital Library
- Liebig, J., von Rhein, A., Kästner, C., Apel, S., Dörre, J., and Lengauer, C. 2012. Large-scale variability-aware type checking and dataflow analysis. Tech. rep. MIP-1212, Department of Informatics and Mathematics, University of Passau. http://www.infosun.fim.uni-passau.de/publications/docs/TR_LRKADL12.pdf.Google Scholar
- Mezini, M. and Ostermann, K. 2003. Conquering aspects with Caesar. In Proceedings of the International Conference on Aspect-Oriented Software Development. 90--99. Google ScholarDigital Library
- Mezini, M. and Ostermann, K. 2004. Variability management with feature-oriented programming and aspects. ACM SIGSOFT Softw. Engin. Notes 29, 6, 127--136. Google ScholarDigital Library
- Miao, W. and Siek, J. G. 2010. Incremental type-checking for type-reflective metaprograms. In Proceedings of the International Conference on Generative Programming and Component Engineering (GPCE’10). 167--176. Google ScholarDigital Library
- Nelson, G. and Oppen, D. C. 1980. Fast decision procedures based on congruence closure. J. ACM 27, 2, 356--364. Google ScholarDigital Library
- Norell, U. 2007. Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Sceince and Engineering, Chalmers University of Technology and Göteborg University.Google Scholar
- Odersky, M., Sulzmann, M., and Wehr, M. 1999. Type inference with constrained types. Theory Pract. Object Syst. 5, 1, 35--55. Google ScholarDigital Library
- Paulin-Mohring, C. 1993. Inductive definitions in the system Coq rules and properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA’93). 328--345. Google ScholarDigital Library
- Pierce, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Pohl, K., Böckle, G., and van der Linden, F. 2005. Software Product Line Engineering: Foundations, Principles, and Techniques. Springer. Google ScholarDigital Library
- Reis, G. D. and Stroustrup, B. 2005. A formalism for C++. Tech. rep. ISO/IEC SC22/JTC1/WG21. http://www.open-std.org/jtc1/SC22/WG21/docs/papers/2005/n1885.pdf.Google Scholar
- Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1, 23--41. Google ScholarDigital Library
- Sheard, T. and Jones, S. P. 2002. Template meta-programming for Haskell. SIGPLAN Not. 37, 12, 60--75. Google ScholarDigital Library
- Shields, M., Sheard, T., and Peyton Jones, S. 1998. Dynamic typing as staged type inference. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’98). 289--302. Google ScholarDigital Library
- Siek, J. and Taha, W. 2006. A semantic analysis of C++ templates. In Procceedings of the European Conference on Object-Oriented Programming (ECOOP’06). 304--327. Google ScholarDigital Library
- Steensgaard, B. 1996. Points-to analysis in almost linear time. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’96). 32--41. Google ScholarDigital Library
- Stroustrup, B. 1994. The Design and Evolution of C++. Addison-Wesley Professional. Google ScholarDigital Library
- Sulzmann, M. 2001. A general type inference framework for Hindley/Milner style systems. In Proceedings of the International Symposium on Functional and Logic Programming. 248--263. Google ScholarDigital Library
- Sulzmann, M. and Stuckey, P. J. 2008. HM(X) type inference is CLP(X) solving. J. Funct. Program. 18, 2, 251--283. Google ScholarDigital Library
- Taha, W. and Sheard, T. 2000. MetaML and multi-stage programming with explicit annotations. Theor. Comput. Sci. 248, 1--2, 211--242. Google ScholarDigital Library
- Thaker, S., Batory, D., Kitchin, D., and Cook, W. 2007. Safe composition of product lines. In Proceedings of the International Conference on Generative Programming and Component Engineering. 95--104. Google ScholarDigital Library
- Warth, A., Stanojević, M., and Millstein, T. 2006. Statically scoped object adaptation with expanders. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’06). 37--56. Google ScholarDigital Library
- Xi, H. and Pfenning, F. 1999. Dependent types in practical programming. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’99). 214--227. Google ScholarDigital Library
Index Terms
- Extending Type Inference to Variational Programs
Recommendations
An error-tolerant type system for variational lambda calculus
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingConditional compilation and software product line technologies make it possible to generate a huge number of different programs from a single software project. Typing each of these programs individually is usually impossible due to the sheer number of ...
Migrating gradual types
Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically-typed to more statically-typed or vice versa, gradual typing itself does not provide a ...
An error-tolerant type system for variational lambda calculus
ICFP '12Conditional compilation and software product line technologies make it possible to generate a huge number of different programs from a single software project. Typing each of these programs individually is usually impossible due to the sheer number of ...
Comments