Searching for type-error messages

ABSTRACT

Advanced type systems often need some form of type inference to reduce the burden of explicit typing, but type inference often leads to poor error messages for ill-typed programs. This work pursues a new approach to constructing compilers and presenting type-error messages in which the type-checker itself does not produce the messages. Instead, it is an oracle for a search procedure that finds similar programs that do type-check. Our two-fold goal is to improve error messages while simplifying compiler construction. Our primary implementation and evaluation is for Caml, a language with full type inference. We also present a prototype for C++ template functions, where type instantiation is implicit. A key extension is making our approach robust even when the program has multiple independent type errors.

REFERENCES

• 1: Mike Beaven , Ryan Stansifer, Explaining type errors in polymorphic languages, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.17-30, March–Dec. 1993 [doi>10.1145/176454.176460]
• 2: K. Bernstein and E. Stark. Debugging type errors (full version). Technical report, State University of New York at Stony Brook, 1995.
• 3: Michael G. Burke , Gerald A. Fisher, A practical method for LR and LL syntactic error diagnosis and recovery, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.2, p.164-197, April 1987 [doi>10.1145/22719.22720]
• 4: O. Chitil, F. Huch, and A. Simon. Typeview: a tool for understanding type errors. In MMohnen and PKoopman, editors, 12th International Workshop on Implementation of Functional Languages, Aachner Informatik-Berichte, 2000.
• 5: V. Choppella and C.T. Haynes. Diagnosis of ill-typed programs. Technical Report 426, Indiana University, December 1994.
• 6: Holger Cleve , Andreas Zeller, Locating causes of program failures, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062522]
• 7: D. Duggan. Correct type explanation. In ACM SIGPLAN Workshop on ML, 1998.
• 8: Dominic Duggan , Frederick Bent, Explaining type inference, Science of Computer Programming, v.27 n.1, p.37-83, July 1996 [doi>10.1016/0167-6423(95)00007-0]
• 9: Milind Gandhe , G. Venkatesh , Amitabha Sanyal, Correcting Errors in the Curry System, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, p.347-358, December 18-20, 1996
• 10: Christian Haack , J. B. Wells, Type error slicing in implicitly typed higher-order languages, Science of Computer Programming, v.50 n.1-3, p.189-224, March 2004 [doi>10.1016/j.scico.2004.01.004]
• 11: B.J. Heeren. Top Quality Type Error Messages. PhD thesis, Universiteit Utrecht, The Netherlands, Sept. 2005.
• 12: Jaakko Järvi , Douglas Gregor , Jeremiah Willcock , Andrew Lumsdaine , Jeremy Siek, Algorithm specialization in generic programming: challenges of constrained generics in C++, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 13: Y. Jun, G. Michaelson, and P. Trinder. Explaining polymorphic types. The Computer Journal, 45(4):436--452, 2002.
• 14: Shriram Krishnamurthi , Yan-David Erlich , Matthias Felleisen, Expressing Structural Properties as Language Constructs, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.258-272, March 22-28, 1999
• 15: Oukseh Lee , Kwangkeun Yi, Proofs about a folklore let-polymorphic type inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.707-723, July 1998 [doi>10.1145/291891.291892]
• 16: Benjamin Lerner , Dan Grossman , Craig Chambers, Seminal: searching for ML type-error messages, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA [doi>10.1145/1159876.1159887]
• 17: Bruce J. McAdam, On the Unification of Substitutions in Type Interfaces, Selected Papers from the 10th International Workshop on 10th International Workshop, p.137-152, September 09-11, 1998
• 18: B.J. McAdam. Repairing Type Errors in Functional Programs. PhD thesis, Laboratory for Foundatations of Computer Science, The University of Edinburgh, 2001.
• 19: Gabriel Dos Reis , Bjarne Stroustrup, Specifying C++ concepts, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.295-308, January 11-13, 2006, Charleston, South Carolina, USA
• 20: Peter J. Stuckey , Martin Sulzmann , Jeremy Wazny, Interactive type debugging in Haskell, Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, p.72-83, August 28-28, 2003, Uppsala, Sweden [doi>10.1145/871895.871903]
• 21: F. Tip , T. B. Dinesh, A slicing-based approach for locating type errors, ACM Transactions on Software Engineering and Methodology (TOSEM), v.10 n.1, p.5-55, Jan. 2001 [doi>10.1145/366378.366379]
• 22: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 23: Andreas Zeller, Yesterday, my program worked. Today, it does not. Why?, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.253-267, September 06-10, 1999, Toulouse, France
• 24: L. Zolman. STLFilt: An STL error message decryptor for C++. http://www.bdsoft.com/tools/stlfilt.html, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Design, Languages

Keywords:
error messages, objective Caml, seminal, type-checking, type-inference