Really Natural Linear Indexed Type Checking

Abstract

Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy. A natural way to enhance the expressiveness of this approach is by allowing the indices to depend on runtime information, in the spirit of dependent types. This approach is used in DFuzz, a language for differential privacy. The DFuzz type system relies on an index language supporting real and natural number arithmetic over constants and variables. Moreover, DFuzz uses a subtyping mechanism to make types more flexible. By themselves, linearity, dependency, and subtyping each require delicate handling when performing type checking or type inference; their combination increases this challenge substantially, as the features can interact in non-trivial ways. In this paper, we study the type-checking problem for DFuzz. We show how we can reduce type checking for (a simple extension of) DFuzz to constraint solving over a first-order theory of naturals and real numbers which, although undecidable, can often be handled in practice by standard numeric solvers.

Cited by in corpus (9)

• Synthesizing Coupling Proofs of Differential Privacy
• Proving Expected Sensitivity of Probabilistic Programs
• Approximate Span Liftings
• Bidirectional Type Checking for Relational Properties
• Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy
• Numerical Fuzz: A Type System for Rounding Error Analysis
• Probabilistic Relational Reasoning via Metrics
• Bean: A Language for Backward Error Analysis
• Bunched Fuzz: Sensitivity for Vector Metrics