Mechanical incrementalization of typing algorithms

The ever-growing size of programs and their continuous evolution require building fast and efficient analyzers. Here we focus on the static ones, in particular on type systems, for both checking and inference. Just as programs change by incrementally changing or inserting pieces of code, called diffs, also type systems should be incremental and re-type the diffs, only. An algorithmic schema is proposed that mechanically derives an incremental version of existing, standard typing algorithms. Ours is a grey-box approach: just the shape of the typing rules, that of the types and some domain-specific knowledge are needed to instantiate our schema. Here, we present the foundations of our approach and the conditions for its correctness. Our schema is applied to derive four incremental typing and inference algorithms for languages in different programming paradigms. We implemented an OCaml module that inputs a type system and outputs its incrementalized version. Experimental results show that our approach is effective, and prove its usage beneficial.