To help data scientists visualize raw data that are exploding in quantity, there has been growing interest in using program synthesis to automatically generate visualization programs from user demonstrations. One flavor of such demonstrations is input-output (IO) examples: the user provides tabular input data and demonstrate how to visualize a small number of data points. However, for more complex visualizations, concrete examples are often insufficient for fully expressing user intent, leading to \emph{overfitting}. Moreover, they require the user to provide the exact values (e.g. height of a bar) via laborious manual calculation.

To address those challenges, we propose a new paradigm of visualization synthesis based on \emph{refinement types}. Besides IO examples, the user 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. We develop an efficient bi-directional algorithm to synthesize data transformation and visualization programs that are consistent with refinement type specification.