ABSTRACT
To improve the quality of type error messages in functional programming languages,we propose four techniques which influence the behaviour of constraint-based type inference processes. These techniques take the form of externally supplied type inference directives, precluding the need to make any changes to the compiler. A second advantage is that the directives are automatically checked for soundness with respect to the underlying type system. We show how the techniques can be used to improve the type error messages reported for a combinator library. More specifically, how they can help to generate error messages which are conceptually closer to the domain for which the library was developed. The techniques have all been incorporated in the Helium compiler, which implements a large subset of Haskell.
- A. Aiken and E. Wimmers. Type inclusion constraints and type inference. In Proceedings of Functional Programming Languages and Computer Architecture, pages 31--41, 1993. Google ScholarDigital Library
- M. Beaven and R. Stansifer. Explaining type errors in polymorphic languages. In ACM Letters on Programming Languages, volume 2, pages 17--30, December 1993. Google ScholarDigital Library
- O. Chitil. Compositional explanation of types and algorithmic debugging of type errors. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, pages 193--204, September 2001. Google ScholarDigital Library
- L. Damas and R. Milner. Principal type schemes for functional programs. In Principles of Programming Languages, pages 207--212, 1982. Google ScholarDigital Library
- D. Duggan and F. Bent. Explaining type inference. In Science of Computer Programming 27, pages 37--83, 1996. Google ScholarDigital Library
- C. Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. In Proceedings of the 12th European Symposium on Programming, pages 284--301, April 2003. Google ScholarDigital Library
- B. Heeren, J. Hage, and S. D. Swierstra. Generalizing Hindley-Milner type inference algorithms. Technical Report UU-CS-2002-031, Institute of Information and Computing Science, University Utrecht, Netherlands, July 2002.Google Scholar
- A. van IJzendoorn, D. Leijen, and B. Heeren. The Helium compiler. http://www.cs.uu.nl/helium.Google Scholar
- J. Yang. Explaining type errors by finding the sources of type conflicts. In G. Michaelson, P. Trindler, and H.-W. Loidl, editors, Trends in Functional Programming, pages 58--66. Intellect Books, 2000. Google ScholarDigital Library
- O. Lee and K. Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transanctions on Programming Languages and Systems, 204):707--723, July 1998. Google ScholarDigital Library
- O. Lee and K. Yi. A generalized let-polymorphic type inference algorithm. Technical Memorandum ROPAS-2000-5, Research on Program Analysis System, Korea Advanced Institute of Science and Technology, March 2000.Google Scholar
- B. J. McAdam. How to repair type errors automatically. In 3rd Scottish Workshop on Functional Programming, pages 121--135. Stirling, U.K., August 2001. Google ScholarDigital Library
- M. Sulzmann, M. Odersky, and M. Wehr. Type inference with constrained types. Research Report YALEU/DCS/RR-1129, Yale University, Department of Computer Science, April 1997.Google Scholar
- S. D. Swierstra. Combinator parsers: From toys to tools. In G. Hutton, editor, Electronic Notes in Theoretical Computer Science, volume~41. Elsevier Science Publishers, 2001.Google Scholar
- J. A. Walz and G. F. Johnson. A maximum flow approach to anomaly isolation in unification-based incremental type inference. In Conference Record of the 13th Annual ACM Symposium on Principles of Programming Languages, pages 44--57, St. Petersburg, FL, January 1986. Google ScholarDigital Library
Index Terms
- Scripting the type inference process
Recommendations
Scripting the type inference process
To improve the quality of type error messages in functional programming languages,we propose four techniques which influence the behaviour of constraint-based type inference processes. These techniques take the form of externally supplied type inference ...
Type inference with simple selftypes is NP-complete
The metavariable self is fundamental in object-oriented languages. Typing self in the presence of inheritance has been studied by Abadi and Cardelli, Bruce, and others. A key concept in these developments is the notion of selftype, which enables ...
Discriminative sum types locate the source of type errors
We propose a type system for locating the source of type errors in an applied lambda calculus with ML-style polymorphism. The system is based on discriminative sum types---known from work on soft typing---with annotation subtyping and recursive types. ...
Comments