Really Natural Linear Indexed Type Checking

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 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.