Reasoning about type errors is very difficult, and requires shifting between static and dynamic types. In OCaml, the type checker asserts ill-typedness but provides little in the way of understanding why the type checker inferred such types. These direct error messages are difficult to understand even for experienced programmers working on larger codebases.
This project will explore how to use gradual types to reason more effectively about such ill-typed programs, by introducing more dynamic types to help some users build an intuition about the problem in their code. The intention is to enable a more exploratory approach to constructing well-typed programs.
Some relevant reading:
- Refined Criteria for Gradual Typing
- Dynamic Type Inference for Gradual Hindley-Milner Typing
- Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)
1 Links
The project was completed successfully by Max Carroll, who wrote it up as (:2025-decomposable-type-highlighting) and presented it at the HATRA workshop colocated with ICFP 2025, complete with a live demo of type-level debugging in Hazel. There are more details in my What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP writeup from the conference. Max Carroll went on to extend this work in his Part III project on (:bidirectional-type-slicing).