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.

翻译：关于函数对其输入的敏感性推理在差分隐私等多个领域具有有趣的应用。为了检查并强制实施敏感性，已有多种方法被提出，特别是敏感性类型系统。在这些系统中，敏感性可被视为一种效应，即Gifford和Lucassen最初提出的类型-效应系统中的效应。由于类型-效应系统可能使某些有用的编程模式变得繁琐或过度保守，因此将渐进类型化的优势引入这些领域以促进其采纳具有重要价值。本研究对渐进敏感性类型化进行了动机阐述、形式化定义和原型实现。语言GSoul支持无限制的未知敏感性和以区间形式表示的有界不精确性。渐进敏感性类型化允许程序员平滑地将缺乏任何静态敏感性信息的类型化程序演化为包含静态与动态敏感性检查混合的强化程序。特别地，我们证明渐进敏感性支持完全静态检查会过于保守的递归函数，从而无缝实现精确的运行时敏感性检查。GSoul同时满足渐进保证和敏感性类型健全性（即度量保持）。我们确立了一般的渐进度量保持是终止不敏感的，并且通过将规范强化为有界不精确性可以实现对终止敏感的渐进度量保持。我们实现了一个原型，为渐进敏感性类型化提供了交互式测试平台。本研究为其他依赖于函数敏感性的类型化规范（如差分隐私）以及基于类型的定量推理技术迈向渐进化开辟了道路。