An Embedded Type Debugger

This paper presents how to build a type debugger without implementing any dedicated type inferencer. Previous type debuggers required their own type inferencers apart from the compiler's type inferencer. The advantage of our approach is threefold. First, by not implementing a type inferencer, it is guaranteed that the debugger's type inference never disagrees with the compiler's type inference. Secondly, we can avoid the pointless reproduction of a type inferencer that should work precisely as the compiler's type inferencer. Thirdly, our approach is robust to updates of the underlying language. The key observation of our approach is that the interactive type debugging, as proposed by Chitil, does not require a type inference tree but only a tree with a certain simple property. We identify the property and present how to construct a tree that satisfies this property using the compiler's type inferencer. The property guides us how to build a type debugger for various language constructs. In this paper, we describe our idea and first apply it to the simply-typed lambda calculus. After that, we extend it with let-polymorphism and objects to see how our technique scales.