TL;DR
This paper investigates the type-checking problem for DFuzz, a language with dependent, linear, and subtyping features, by reducing it to constraint solving over naturals and reals, enabling practical handling despite theoretical undecidability.
Contribution
It provides a reduction of DFuzz's type checking to constraint solving, facilitating practical type inference in complex dependent linear type systems.
Findings
Type checking for DFuzz can be reduced to constraint solving.
Standard numeric solvers can often handle the resulting constraints.
The approach manages the complexity of combining linearity, dependency, and subtyping.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
