Gradual Sensitivity Typing
Damian Arquez, Matías Toro, Éric Tanter
TL;DR
This work introduces GSoul, a functional language that blends static sensitivity typing with gradual, runtime-checked precision to reason about function sensitivity and differential privacy. It develops a core calculus GS and a runtime language GSCheck with evidences to support consistent subtyping, followed by a syntactic elaboration from GS to GSCheck that preserves type safety and gradual guarantees. The authors formalize termination-insensitive and termination-sensitive metric preservation, leveraging bounded imprecision (intervals) to obtain stronger privacy guarantees and robust DP reasoning, including Gradual Laplace Mechanism and Gradual Above Threshold. The framework enables pay-as-you-go static/dynamic analysis, supports recursive and higher-order patterns, and lays groundwork for gradualizing other quantitative typing disciplines while contributing practical prototype tooling. Overall, GSoul provides a principled, flexible approach to integrating gradualness into sensitivity analysis and differential privacy reasoning.
Abstract
Reasoning about the sensitivity of functions with respect to their inputs has interesting applications in various areas, such as differential privacy. In order to check and enforce sensitivity, several approaches have been developed, notably sensitivity type systems. In these systems, sensitivity can be seen as an effect in the sense of type-and-effects systems as originally proposed by Gifford and Lucassen. Because type-and-effect systems can make certain useful programming patterns tedious or overly conservative, there is value in bringing the benefits of gradual typing to these disciplines in order to ease their adoption. In this work, we motivate, formalize, and prototype gradual sensitivity typing. The language GSoul supports both the unrestricted unknown sensitivity and bounded imprecision in the form of intervals. Gradual sensitivity typing allows programmers to smoothly evolve typed programs without any static sensitivity information towards hardened programs with a mix of static and dynamic sensitivity checking. In particular, we show that gradual sensitivity supports recursive functions for which fully static checking would be overly conservative, seamlessly enabling exact runtime sensitivity checks. GSoul satisfies both the gradual guarantees and sensitivity type soundness, known as metric preservation. We establish that, in general, gradual metric preservation is termination insensitive, and that one can achieve termination-sensitive gradual metric preservation by hardening specifications to bounded imprecision. We implement a prototype that provides an interactive test bed for gradual sensitivity typing. This work opens the door to gradualizing other typing disciplines that rely on function sensitivity such as differential privacy, as well as other quantitative type-based reasoning techniques.