Seminal: searching for ML type-error messages

ABSTRACT

We present a new way to generate type-error messages in a polymorphic, implicitly, and strongly typed language (specifically Caml). Our method separates error-message generation from type-checking by taking a fundamentally new approach: we present to programmers small term-level modifications that cause an ill-typed program to become well-typed. This approach aims to improve feedback to programmers with no change to the underlying type-checker nor the compilation of well-typed programs.We have added a prototype implementation of our approach to the Objective Caml system by intercepting type-checker error messages and using the type-checker on candidate changes to see if they succeed. This novel front-end architecture naturally decomposes into (1) enumerating local changes to the abstract syntax tree that may remove type errors, (2) searching for places to try the changes, (3) using the type-checker to evaluate the changes, and (4) ranking the changes and presenting them to the user.

REFERENCES

• 1: David T. Barnard, Gwen Clarke, and Nicolas Duncan. Tree-to-tree correction for document trees. Technical Report 95--372, Department of Computing and Information Science, Queen's University, Kingston, January 1995.
• 2: 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]
• 3: Karen Bernstein and Eugene Stark. Debugging type errors (full version). Technical report, State University of New York at Stony Brook, 1995.
• 4: Philip Bille. Tree edit distance, alignment distance and inclusion. Technical report, IT University of Copenhagen, April 2003.
• 5: Olaf Chitil, Frank Huch, and Axel Simon. Typeview: a tool for understanding type errors. In M. Mohnen and P. Koopman, editors, 12th International Workshop on Implementation of Functional Languages, Aachner Informatik-Berichte, pages 63--69, 2000.
• 6: V. Choppella and C. T. Haynes. Diagnosis of ill-typed programs. Technical Report 426, Indiana University, December 1994.
• 7: Dominic Duggan. Correct type explanation. In ACM Workshop on ML, pages 49--58, 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: Bastiaan J. Heeren. Top Quality Type Error Messages. PhD thesis, Universiteit Utrecht, The Netherlands, September 2005.
• 12: Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512649]
• 13: Yang Jun, Greg Michaelson, and Phil Trinder. Explaining polymorphic types. The Computer Journal, 45(4):436--452, 2002.
• 14: 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]
• 15: Bruce J. McAdam. On the unification of substitutions in type inference. In Kevin Hammond, Anthony J.T. Davie, and Chris Clack, editors, Implementation of Functional Languages (IFL~'98), volume 1595 of LNCS, pages 139--154. Springer-Verlag, September 1998.
• 16: Bruce J. McAdam. Repairing Type Errors in Functional Programs. PhD thesis, Laboratory for Foundatations of Computer Science, The University of Edinburgh, 2001.
• 17: B. J. Oommen , K. Zhang , W. Lee, Numerical Similarity and Dissimilarity Measures Between Two Trees, IEEE Transactions on Computers, v.45 n.12, p.1426-1434, December 1996 [doi>10.1109/12.545972]
• 18: 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]
• 19: 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]
• 20: Robert A. Wagner , Michael J. Fischer, The String-to-String Correction Problem, Journal of the ACM (JACM), v.21 n.1, p.168-173, Jan. 1974 [doi>10.1145/321796.321811]
• 21: 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]

INDEX TERMS

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

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

General Terms:
Design, Languages

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