# Choice Calculus

The choice calculus is a simple, formal language for representing *variation*. It supports research in areas that deal with variation in software, such as software product lines. Within this domain, it intends to fulfill a role similar to the lambda calculus in programming languages research, providing a minimal basis for communicating ideas and sharing results.

The core choice calculus is very small—just two constructs, *choices* and *tree nodes*—but it can be easily extended with new language features that support different ways of developing, maintaining, and analyzing variability. The core choice calculus is also generic, emphasizing that variation can often be treated orthogonally to other concerns, but it can be instantiated by different object languages and data types when they interact fundamentally with variability.

The primary reference for the choice calculus is the original TOSEM paper [3], however, the most comprehensive and up-to-date introduction is my PhD thesis [1]. The tutorial from the 2011 GTTSE Summer School [2] is also a good (and hopefully fun) entry point. The tutorial promotes the idea of “variation anywhere” and of generically lifting non-variational algorithms to variational ones.

Using the choice calculus we have developed safe transformations, quality criteria, and new abstraction techniques for variational programs. We have also developed a notion of variational types and extended the Damas-Milner algorithm to perform efficient type inference on a variational lambda calculus [5,6].

The choice calculus also has its own web page: choicecalculus.org.

## Introductions to the Choice Calculus

- The Choice Calculus: A Formal Language of Variation[Abstract, PDF]PhD thesis, Oregon State University, 2013
In this thesis I present the choice calculus, a formal language for representing variation in software and other structured artifacts. The choice calculus is intended to support variation research in a way similar to the lambda calculus in programming language research. Specifically, it provides a simple formal basis for presenting, proving, and communicating theoretical results. It can serve as a common language of discourse for researchers working on different views of similar problems and provide a shared back end in tools.

This thesis collects a large amount of work on the choice calculus. It defines the syntax and denotational semantics of the language along with modular language extensions that add features important to variation research. It presents several theoretical results related to the choice calculus, such as an equivalence relation that supports semantics-preserving transformations of choice calculus expressions, and a type system for ensuring that an expression is well formed. It also presents a Haskell DSEL based on the choice calculus for exploring the concept of variational programming.

- Variation Programming with the Choice Calculus[Abstract, PDF, Code]Generative and Transformational Techniques in Software Engineering (GTTSE), 55–99, 2012
The choice calculus provides a language for representing and transforming variation in software and other structured documents. Variability is captured in localized choices between alternatives. The space of all variations is organized by dimensions, which provide scoping and structure to choices. The variation space can be reduced through a process of selection, which eliminates a dimension and resolves all of its associated choices by replacing each with one of their alternatives. The choice calculus also allows the definition of arbitrary functions for the flexible construction and transformation of all kinds of variation structures. In this tutorial we will first present the motivation, general ideas, and principles that underlie the choice calculus. This is followed by a closer look at the semantics. We will then present practical applications based on several small example scenarios and consider the concepts of “variation programming” and “variation querying”. The practical applications involve work with a Haskell library that supports variation programming and experimentation with the choice calculus.

- The Choice Calculus: A Representation for Software Variation[Abstract, PDF]ACM Trans. on Software Engineering and Methodology (TOSEM), vol. 21, num. 1, 6:1–6:27, 2011
Many areas of computer science are concerned with some form of variation in software–from managing changes to software over time, to supporting families of related artifacts. We present the choice calculus, a fundamental representation for software variation that can serve as a common language of discourse for variation research, filling a role similar to the lambda calculus in programming language research. We also develop an associated theory of software variation, including sound transformations of variation artifacts, the definition of strategic normal forms, and a design theory for variation structures, which will support the development of better algorithms and tools.

## Applications of the Choice Calculus

- Projectional Editing of Variational SoftwareACM SIGPLAN Int. Conf. on Generative Programming and Component Engineering (GPCE), 29–38, 2014Best paper[Abstract, PDF]
Editing the source code of variational software is complicated by the presence of variation annotations, such as #ifdef statements, and by code that is only included in some configurations. When editing some configurations and not others, it would be easier to edit a simplified version of the source code that includes only the configurations we currently care about. In this paper, we present a projectional editing model for variational software. Using our approach, a programmer can partially configure a variational program, edit this simplified view of the code, and then automatically update the original, fully variational source code. The model is based on an isolation principle where edits affect only the variants that are visible in the view. We show that this principle has several nice properties that are suggested by related work on bidirectional transformations.

- Extending Type Inference to Variational Programs[Abstract, PDF]ACM Trans. on Programming Languages and Systems (TOPLAS), vol. 36, num. 1, 1:1–1:54, 2014
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.

- An Error-Tolerant Type System for Variational Lambda Calculus[Abstract, PDF]ACM SIGPLAN Int. Conf. on Functional Programming (ICFP), 29–40, 2012
Conditional 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 possible variants. Our previous work has addressed this problem with a type system for variational lambda calculus (VLC), an extension of lambda calculus with basic constructs for introducing and organizing variation. Although our type inference algorithm is more efficient than the brute-force strategy of inferring the types of each variant individually, it is less robust since type inference will fail for the entire variational expression if any one variant contains a type error. In this work, we extend our type system to operate on VLC expressions containing type errors. This extension directly supports locating ill-typed variants and the incremental development of variational programs. It also has many subtle implications for the unification of variational types. We show that our extended type system possesses a principal typing property and that the underlying unification problem is unitary. Our unification algorithm computes partial unifiers that lead to result types that (1) contain errors in as few variants as possible and (2) are most general. Finally, we perform an empirical evaluation to determine the overhead of this extension compared to our previous work, to demonstrate the improvements over the brute-force approach, and to explore the effects of various error distributions on the inference process.

- #ifdef Confirmed Harmful: Promoting Understandable Software Variation[Abstract, PDF]IEEE Int. Symp. on Visual Languages and Human-Centric Computing (VL/HCC), 143–150, 2011
Maintaining variation in software is a difficult problem that poses serious challenges for the understanding and editing of software artifacts. Although the C preprocessor (CPP) is often the default tool used to introduce variability to software, because of its simplicity and flexibility, it is infamous for its obtrusive syntax and has been blamed for reducing the comprehensibility and maintainability of software. In this paper, we address this problem by developing a prototype for managing software variation at the source code level. We evaluate the difference between our prototype and CPP with a user study, which indicates that the prototype helps users reason about variational code faster and more accurately than CPP. Our results also support the research of others, providing evidence for the effectiveness of related tools, such as CIDE and FeatureCommander.

- Program Fields for Continuous Software[Abstract, PDF]ACM SIGSOFT Workshop on the Future of Software Engineering Research (FoSER), 105–108, 2010
We propose program fields, a formal representation for groups of related programs, as a new abstraction to support future software engineering research in several areas. We will discuss opportunities offered by program fields and research questions that have to be addressed.

## Extensions to the Choice Calculus

- Adding Configuration to the Choice Calculus[Abstract, PDF]Int. Workshop on Variability Modelling of Software-Intensive Systems (VaMoS), 13:1–13:8, 2013
The choice calculus is a formal language for representing variation in software artifacts. Variability is organized in the choice calculus through the use of dimensions, where each dimension represents a decision that must be made in order to obtain a particular variant. However, the process of selecting alternatives from dimensions was relegated to an external operation. This precludes many interesting variation and reuse patterns, such as nested product lines, and theoretical results, such as a syntactic description of configuration, that would be possible if selection were a part of the language itself.

In this paper we add a selection operation to the choice calculus and illustrate how that increases the expressiveness of the calculus. We investigate some alternative semantics of this operation and study their impact and utility. Specifically, we will examine selection in the context of static and dynamically scoped dimension declarations, as a well as a modest and greedy form of dimension elimination. We also present a design for a type system to ensure configuration safety and modularity of nested product lines.

- A Calculus for Modeling and Implementing Variation[Abstract, PDF]ACM SIGPLAN Int. Conf. on Generative Programming and Component Engineering (GPCE), 132–140, 2012
We present a formal calculus for modeling and implementing variation in software. It unifies the compositional and annotative approaches to feature implementation and supports the development of abstractions that can be used to directly relate feature models to their implementation. Since the compositional and annotative approaches are complementary, the calculus enables implementers to use the best combination of tools for the job and focus on inherent feature interactions, rather than those introduced by biases in the representation. The calculus also supports the abstraction of recurring variational patterns and provides a metaprogramming platform for organizing variation in artifacts.

## Variational Data Structures

- Variational Data Structures: Exploring Trade-Offs in Computing With Variability[Abstract, PDF]ACM SIGPLAN Symp. on New Ideas in Programming and Reflections on Software (Onward!), 213–226, 2014
Variation is everywhere, and in the construction and analysis of customizable software it is paramount. In this context, there arises a need for variational data structures for efficiently representing and computing with related variants of an underlying data type. So far, variational data structures have been explored and developed ad hoc. This paper is a first attempt and a call to action for systematic and foundational research in this area. Research on variational data structures will benefit not only customizable software, but many other application domains that must cope with variability. In this paper, we show how support for variation can be understood as a general and orthogonal property of data types, data structures, and algorithms. We begin a systematic exploration of basic variational data structures, exploring the tradeoffs among different implementations. Finally, we retrospectively analyze the design decisions in our own previous work where we have independently encountered problems requiring variational data structures.

- An Abstract Representation of Variational Graphs[Abstract, PDF]Int. Workshop on Feature-Oriented Software Development (FOSD), 25–32, 2013
In the context of software product lines, there is often a need to represent graphs containing variability. For example, extending traditional modeling techniques or program analyses to variational software requires a corresponding notion of variational graphs. In this paper, we introduce a general model of variational graphs and a theoretical framework for discussing variational graph algorithms. Specifically, we present an abstract syntax based on tagging for succinctly representing variational graphs and other data types relevant to variational graph algorithms, such as variational sets and paths. We demonstrate how (non-variational) graph algorithms can be generalized to operate on variational graphs, to accept variational inputs, and produce variational outputs. Finally, we discuss a filtering operation on variational graphs and how this interacts with variational graph algorithms.