Finding the source of type errors

ABSTRACT

It is a truism that most bugs are detected only at a great distance from their source. Although polymorphic type-checking systems like those in ML help greatly by detecting potential run-time type errors at compile-time, such systems are still not very helpful for locating the source of a type error. Typically, an error is reported only when the type-checker can proceed no further, even though the programmer's actual error may have occurred much earlier in the text. We describe an algorithm which appears to be quite helpful in isolating and explaining the source of type errors. The algorithm works by keeping track of the <i>reasons</i> the checker makes deductions about the types of variables.

REFERENCES

• 1: {Boyer &amp; Moore 72} Boyer, R. S., and Moore, J. S. "The Sharing of Structure in Theorem-Proving Programs," in <i>Machine Intelligence 7</i> (B. Meltzer &amp; D. Michie, eds), Edinburgh University Press (1972), 101--116.
• 2: {Friedman <i>et al.</i> 84} Friedman, D. P., Haynes, C. T., Kohlbecker, E., and Wand, M. "The Scheme 84 Reference Manual" Indiana University Computer Science Department Technical Report No. 153 (March, 1984; revised, June, 1985).
• 3: M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512773]
• 4: {Milner 78} Milner, R. "A Theory of Type Polymorphism in Programming," <i>J. Comp. &amp; Sys. Sci. 17</i> (1978), 348--375.
• 5: Mitchell Wand, A semantic prototyping system, Proceedings of the 1984 SIGPLAN symposium on Compiler construction, p.213-221, June 17-22, 1984, Montreal, Canada