Gradual Sensitivity Typing

TL;DR

This paper introduces GSoul, a language supporting gradual sensitivity typing, enabling flexible, mixed static and dynamic sensitivity analysis, which simplifies reasoning about function sensitivity especially in recursive functions and differential privacy applications.

Contribution

It formalizes and prototypes gradual sensitivity typing, combining static and dynamic checks, and demonstrates its benefits for recursive functions and differential privacy.

Findings

Supports recursive functions with static and dynamic sensitivity checks

Ensures gradual guarantees and metric preservation

Prototype implementation for testing gradual sensitivity typing

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.