Principle and Practice of OCaml Type Debugger
It is not always easy to correct a type error especially for novice
programmers. When a type error occurs, the compiler shows a type error
message, but often, it does not show the true cause of the type error. Why?
Because it is impossible in general. Without knowing the intention of the
programmer, the compiler cannot choose a single cause among multiple possible
causes of the type error.
To locate the true cause of a type error, we have built an interactive type
debugger for OCaml that incorporates programmer's intention. When a type
error occurs, the type debugger asks a series of questions to the programmer.
By correctly answering these questions, we are lead to the true source of the
type error.
In this talk, I will first introduce the principle of the type debugger and
show how a simple but crucial idea leads to a practicable type debugger. I
then describe requirements and challenges for such a tool to be effective
in the real use cases, such as in a classroom.