Type Error Debugging in Hazel

# Notes

Completed as part of a Bachelor of Arts in Computer Science at Cambridge university over the 2024-2025 year. Won the 2nd place prize with a score of 92.5%.

I am grateful for help provided by my supervisors (Anil Madhavapeddy and Patrick Ferris) throughout this project. Especially Patrick's creation of a basic OCaml to Hazel transpiler, that supported translation of both well-typed and ill-typed OCaml code.

# Original Aims

This project seeks to explore ways to improve type error debugging. Traces to dynamic type errors can provide better intuition to why static type errors were found. Additionally, dynamic errors do not often point directly back to source code, or do so only incompletely. This project aimed to create a source code highlighting system for dynamic errors and an automated search procedure for dynamic errors. The Hazel language was chosen, allowing the project to explore both static and dynamic errors and their interaction. Only a subset of Hazel was expected to be supported, but enough to demonstrate the methods’ promise.

# Work Completed

The project successfully supports almost all of Hazel. Hazel is an intensely active research project so significant work went into staying up to date and producing a corpus of Hazel programs. Four searching methods were implemented, the best failing to find existing dynamic errors for only 2% of the corpus. Dynamic error highlighting had no prescribed basis to build upon. Therefore, a very significant part was devising novel formalisations for type-directed highlighting systems which propagate information throughout evaluation; further extended to explain static errors also. Both error highlighting implementations were found to be concise and demonstrated to be effective.

# Continued Work

Work on the type slicing aspect of this project has been continued. Including a progress/summary paper accepted to the HATRA 2025 workshop with my corresponding talk.