Using Standard Typing Algorithms Incrementally

TL;DR

This paper introduces a schema for creating incremental type checking algorithms that reuse existing standard algorithms, improving efficiency for large and evolving codebases.

Contribution

It presents a generic, grey-box schema for deriving incremental typing algorithms from standard ones without modifications, demonstrated on multiple language types.

Findings

Incremental type checking is generally more efficient.

The schema can be instantiated for different language paradigms.

Experiments confirm the practical benefits of incremental type checking.

Abstract

Modern languages are equipped with static type checking/inference that helps programmers to keep a clean programming style and to reduce errors. However, the ever-growing size of programs and their continuous evolution require building fast and efficient analysers. A promising solution is incrementality, so one only re-types those parts of the program that are new, rather than the entire codebase. We propose an algorithmic schema driving the definition of an incremental typing algorithm that exploits the existing, standard ones with no changes. Ours is a grey-box approach, meaning that just the shape of the input, that of the results and some domain-specific knowledge are needed to instantiate our schema. Here, we present the foundations of our approach and we show it at work to derive three different incremental typing algorithms. The first two implement type checking and inference for a functional language. The last one type-checks an imperative language to detect information flow and non-interference. We assessed our proposal on a prototypical implementation of an incremental type checker. Our experiments show that using the type checker incrementally is (almost) always rewarding.