From Identity to Difference: A Quantitative Interpretation of the Identity Type

TL;DR

This paper introduces difference type theory (dTT), a quantitative extension of intuitionistic type theory that models program differences and errors, enabling reasoning about approximate equivalence and error propagation.

Contribution

It develops dTT as a new logical framework for quantitative reasoning in programming, connecting it to existing models and applications like differential privacy and program differentiation.

Findings

dTT captures compositional reasoning with errors

Semantics of dTT relate to weak factorization systems

dTT models are applicable to privacy and incremental computing

Abstract

We explore a quantitative interpretation of 2-dimensional intuitionistic type theory (ITT) in which the identity type is interpreted as a "type of differences". We show that a fragment of ITT, that we call difference type theory (dTT), yields a general logical framework to talk about quantitative properties of programs like approximate equivalence and metric preservation. To demonstrate this fact, we show that dTT can be used to capture compositional reasoning in presence of errors, since any program can be associated with a "derivative" relating errors in input with errors in output. Moreover, after relating the semantics of dTT to the standard weak factorization systems semantics of ITT, we describe the interpretation of dTT in some quantitative models developed for approximate program transformations, incremental computing, program differentiation and differential privacy.