Eliminating bugs in type inference algorithms by describing them with precise types

Abstract

Static type systems ensure code correctness by aligning implementations with defined type signatures. Despite their benefits in preventing common errors, complex type systems increase the likelihood of bugs within type checkers. Correct-by-Construction (CbC) programming offers a solution by using precise types to create intrinsically verified type checkers, ensuring soundness and potentially completeness. This paper evaluates the use of CbC programming for implementing type inference for the simply typed λ-calculus, focusing on Hindley-Milner (HM) and bidirectional type inference. Implementations in Agda, a dependently typed language, reveal that while CbC programming can eliminate bugs, it introduces significant complexity. HM type inference proves challenging in terms of soundness and completeness, whereas bidirectional type inference is easier to implement but still complex to prove complete. The study highlights the trade-offs of CbC programming, suggesting it is more suited for research and in-depth understanding rather than pragmatic programming.