Benjamin Lerner
Dan Grossman
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.
- 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.Google Scholar
- Mike Beaven and Ryan Stansifer. Explaining type errors in polymorphic languages. ACM Letters on Programming Languages and Systems, 2(1-4):17--30, 1993. Google ScholarDigital Library
- Karen Bernstein and Eugene Stark. Debugging type errors (full version). Technical report, State University of New York at Stony Brook, 1995.Google Scholar
- Philip Bille. Tree edit distance, alignment distance and inclusion. Technical report, IT University of Copenhagen, April 2003.Google Scholar
- 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.Google Scholar
- V. Choppella and C. T. Haynes. Diagnosis of ill-typed programs. Technical Report 426, Indiana University, December 1994.Google Scholar
- Dominic Duggan. Correct type explanation. In ACM Workshop on ML, pages 49--58, 1998.Google Scholar
- Dominic Duggan and Frederick Bent. Explaining type inference. Science of Computer Programming, 27(1):37--83, July 1996. Google ScholarDigital Library
- Milind Gandhe, G. Venkatesh, and Amitabha Sanyal. Correcting errors in the Curry system. In 16th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 347--358, London, UK, 1996. Springer-Verlag. Google ScholarDigital Library
- Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Science of Computer Programming, 50(1-3):189--224, 2004. Google ScholarDigital Library
- Bastiaan J. Heeren. Top Quality Type Error Messages. PhD thesis, Universiteit Utrecht, The Netherlands, September 2005.Google Scholar
- Gregory F. Johnson and Janet A. Walz. A maximum-flow approach to anomaly isolation in unification-based incremental type inference. In 13th ACM Symposium on Principles of Programming Languages, pages 44--57, St. Petersburg Beach, Florida, January 1986. Google ScholarDigital Library
- Yang Jun, Greg Michaelson, and Phil Trinder. Explaining polymorphic types. The Computer Journal, 45(4):436--452, 2002.Google ScholarCross Ref
- Oukseh Lee and Kwangkeun Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):707--723, 1998. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Bruce J. McAdam. Repairing Type Errors in Functional Programs. PhD thesis, Laboratory for Foundatations of Computer Science, The University of Edinburgh, 2001.Google Scholar
- B. J. Oommen, K. Zhang, and W. Lee. Numerical similarity and dissimilarity measures between two trees. IEEE Transactions on Computers, 45(12):1426--1434, 1996. Google ScholarDigital Library
- Peter J. Stuckey, Martin Sulzmann, and Jeremy Wazny. Interactive type debugging in Haskell. In ACM Workshop on Haskell, pages 72--83, Uppsala, Sweden, 2003. Google ScholarDigital Library
- F. Tip and T. B. Dinesh. A slicing-based approach for locating type errors. ACM Transactions on Software Engineering and Methodology, 10(1):5--55, 2001. Google ScholarDigital Library
- Robert A. Wagner and Michael J. Fischer. The string-to-string correction problem. Journal of the ACM, 21(1):168--173, 1974. Google ScholarDigital Library
- Mitchell Wand. Finding the source of type errors. In 13th ACM Symposium on Principles of Programming Languages, pages 38--43, St. Petersburg Beach, Florida, January 1986. Google ScholarDigital Library
Index Terms
- Seminal: searching for ML type-error messages
Recommendations
Searching for type-error messages
Proceedings of the 2007 PLDI conferenceAdvanced 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 ...
Searching for type-error messages
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationAdvanced 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-safe distributed programming for OCaml
ML '06: Proceedings of the 2006 workshop on MLExisting ML-like languages guarantee type-safety, ensuring memory safety and protecting the invariants of abstract types, but only within single executions of single programs. Distributed programming is becoming ever more important, and should benefit ...
Comments