一句话：提出用参数性从类型检查直接导出函数敏感度，并在 Haskell 库 Spar 中实现。
针对差分隐私中程序敏感度推理问题，Fuzz、DFuzz、Duet 等依赖线性类型、模态类型和部分求值，往往需要从头设计新语言；近期工作表明仅用基类型静态敏感度标注也可行。本文改以参数性为核心：为基类型加入值之间度量关系的信息，利用参数性直接推导函数敏感度，从而把敏感度计算与证明归约为支持多态和类型级自然数的语言中的类型检查。作者形式化了一个演算并证明其可靠性，在 Haskell 中实现不足 500 行的库 Spar，对典型例子进行推理，利用宿主语言类型推断支持有限的敏感度推断，并加入 privacy monad 以构建差分隐私程序。
The work of Fuzz has pioneered the use of functional programming languages where types allow reasoning about the sensitivity of programs. Fuzz and subsequent work (e.g., DFuzz and Duet) use advanced technical devices like linear types, modal types, and partial evaluation. These features usually require the design of a new programming language from scratch—a significant task on its own! While these features are part of the classical toolbox of programming languages, they are often unfamiliar to non-experts in this field. Fortunately, recent studies (e.g., Solo ) have shown that linear and complex types in general, are not strictly needed for the task of determining programs’ sensitivity since this can be achieved by annotating base types with static sensitivity information. In this work, we take a different approach. We propose to enrich base types with information about the metric relation between values, and we present the novel idea of applying parametricity to derive direct proofs for the sensitivity of functions. A direct consequence of our result is that calculating and proving the sensitivity of functions is reduced to simply type-checking in a programming language with support for polymorphism and type-level naturals. We formalize our main result in a calculus, prove its soundness, and implement a software library in the programming language Haskell-where we reason about the sensitivity of canonical examples. We show that the simplicity of our approach allows us to exploit the type inference of the host language to support a limited form of sensitivity inference. Furthermore, we extend the language with a privacy monad to showcase how our library can be used in practical scenarios such as the implementation of differentially private programs, where the privacy guarantees depend on the sensitivity of user-defined functions. Our library, called Spar , is implemented in less than 500 lines of code.
@article{VesgaRGC24,
title = {Sensitivity by Parametricity},
author = {Elisabet Lobo-Vesga and Alejandro Russo and Marco Gaboardi and Carlos Tomé Cortiñas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689726}
}