Really Natural Linear Indexed Type Checking

Recent works have shown the power of linear indexed type systems for capturing complex safety properties. These systems combine linear type systems with a language of indices that appear in the types, allowing more fine-grained analysis. For example, linear indexed types have been fruitfully applied to verify differential privacy in the Fuzz type system. 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, an extension of Fuzz. The DFuzz type system relies on an index-level language supporting real and natural number arithmetic over con-stants and dependent variables. Moreover, DFuzz uses a subtyping mechanism to semantically manipulate indices. By themselves, lin-earity, 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. Categories and Subject Descriptors F.3.3 [Studies of Program Constructs]: Type structur