Improving Error Messages with Algebraic Subtyping
Good type errors are an important tool to improve programmer productivity. Ideally, they can help to quickly localize and fix problems and help programmers to not only better understand the error, but also the underlying program.
Type inference in ML-like languages is often implemented in terms of unification. If not treated with great care, this can lead to error messages like
11:5 Cannot unify Int with String
which at most are helpful because they indicate the position and the involved types, but do not carry additional insight.
Algebraic subtyping is a new approach for type inference for ML-like languages with subtyping. Implementations of algebraic subtyping are based on bi-unification, maintaining additional information.
The goal of this thesis is to use this additional information for a language without subtyping to generate improved error messages for ML-like languages.
This thesis is co-supervised with David Binder.
Additional Material
- Algebraic Subtyping (Stephen Dolan, PhD Thesis)
- The simple essence of algebraic subtyping (Lionel Parreaux, research paper)