Gradual sensitivity types

Abstract

Sensitivity type systems are used to reason about the sensitivity of computations. This is of particular interest in the fields of privacy, specially differential privacy. One caveat of sensitivity types is that, being a typing discipline, they constrain programmers to statically deal with sometimes complex and often conservative restrictions imposed by types. This can quickly lead to a cumbersome developer experience. Gradual typing is an effective approach to provide the programmer with a smooth transition between the flexibility of dynamically-typed languages and the safety of statically-typed ones. This is achieved by allowing optimistic assumptions during typechecking that are later monitored and checked during runtime. For instance, in a gradually-typed language, a programmer can start with a program that is checked in a full dynamic discipline, and as the code becomes stable the programmer can add type information in order to take advantage of the guarantees provided by static typechecking. We hypothesize that gradual typing, and its advantages, can be applied in a sensitivity types setting. Gradual sensitivity types would allow the programmer to range from a program with simple types to a fully-annotated one by adding sensitivity information. In this work, we explore the introduction of gradual typing in the sensitivity information encoded in sensitivity types. In particular, we explore how the Abstracting Gradual Typing (AGT) methodology can be used to achieve this task. We first present a statically-typed sensitivity language as a preamble to the introduction of gradual typing. We discuss the particularities of the language and establish type safety and soundness in a sensitivity setting. We then derive a gradual sensitivity language by following step-by-step the AGT methodology and explore whether it satisfies (1) the properties already satisfied by its static counterpart, specially soundness with respect to sensitivity, and (2) a crucial property known as gradual guarantee.