Refinement Types for Visualization

Visualizations have become crucial in the contemporary data-driven world as they aid in exploring, verifying, and sharing insights obtained from data. In this paper, we propose a new paradigm of visualization synthesis based on refinement types. Besides input-output examples, users can optionally use refinement-type annotations to constrain the range of valid values in the example visualization or to express complex interactions between different visual components. Our system's outputs include both data transformation and visualization programs that are consistent with refinementtype specifications. To mitigate the scalability challenge during the synthesis process, we introduce a new visualization synthesis algorithm that uses lightweight bidirectional type checking to prune the search space. As we demonstrate experimentally, this new synthesis algorithm results in significant speed-up compared to prior work. We have implemented the proposed approach in a tool called Calico and evaluated it on 40 visualization tasks collected from online forums and tutorials. Our experiments show that Calico can solve 98% of these benchmarks and, among those benchmarks that can be solved, the desired visualization is among the top-1 output generated by Calico. Furthermore, Calico takes an average of 1.56 seconds to generate the visualization, which is 50 times faster than Viser, a state-of-the-art synthesizer for data visualization.