Interactive type debugging in Haskell

ABSTRACT

In this paper we illustrate the facilities for type debugging of Haskell programs in the Chameleon programming environment. Chameleon provides an extension to Haskell supporting advanced and programmable type extensions. Chameleon maps the typing problem for a program to a system of constraints each attached to program code that generates the constraints. We use reasoning about constraint satisfiability and implication to find minimal justifications of type errors, and to explain unexpected types that arise. Through an interactive process akin to declarative debugging, a user can track down exactly where a type error occurs. The approach handles Hindley/Milner types with Haskell-style overloading. The Chameleon system provides a full implementation of our flexible type debugging scheme which can be used as a front-end to any existing Haskell system.

REFERENCES

• 1: S. Abdennadher. Operational semantics and confluence of constraint propagation rules. In Proc. of CP'97, volume 1330 of LNCS, pages 252--266. Springer-Verlag, 1997.
• 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: Olaf Chitil, Compositional explanation of types and algorithmic debugging of type errors, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy
• 4: B. Demoen, M. Garcia de la Banda, and P. J. Stuckey. Type constraint solving for parametric and ad-hoc polymorphism. In Proc. of the 22nd Australian Computer Science Conference, pages 217--228. Springer-Verlag, 1999.
• 5: 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]
• 6: Thom W. Frühwirth, Constraint Handling Rules, Selected Papers from Constraint Programming: Basics and Trends, p.90-107, May 16-20, 1994
• 7: Maria Garcia de la Banda , Peter J. Stuckey , Jeremy Wazny, Finding all minimal unsatisfiable subsets, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.32-43, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888256]
• 8: K. Glynn, P. J. Stuckey, and M. Sulzmann. Type classes and constraint handling rules. In Workshop on Rule-Based Constraint Reasoning and Programming, 2000. http://xxx.lanl.gov/abs/cs.PL/0006034.
• 9: C. Haack and J. B. Wells. Type error slicing in implicitly typed, higher-order languages. In Proc. of ESOP'03, volume 2618 of LNCS, pages 284--301. Springer-Verlag, 2003.
• 10: Haskell 98 language report. http://research.microsoft.com/Users/simonpj/haskell98-revised/haskell98-report-html/.
• 11: B. Heeren and J. Hage. Parametric type inferencing for Helium. Technical Report UU-CS-2002-035, Utrecht University, 2002.
• 12: B. Heeren, J. Hage, and D. Swierstra. Generalizing Hindley-Milner type inference algorithms. Technical Report UU-CS-2002-031, Utrecht University, 2002.
• 13: Helium home page. http://www.cs.uu.nl/~afie/helium/.
• 14: F. Huch, O. Chitil, and A. Simon. Typeview: a tool for understanding type errors. In M. Mohnen and P. Koopman, editors, Proceedings of 12th International Workshop on Implementation of Functional Languages, pages 63--69. Aachner Informatik-Berichte,, 2000.
• 15: Hugs home page. haskell.org/hugs/.
• 16: M. P. Jones. Coherence for qualified types. Research Report YALEU/DCS/RR-989, Yale University, Department of Computer Science, September 1993.
• 17: O. Lee and K. Yi. A generalized let-polymorphic type inference algorithm. Technical Memorandum ROPAS-2000-5, National Creative Research Center, Korea Advanced Institute of Science and Technology, March 2000.
• 18: K. Marriott and P.J. Stuckey. Programming with Constraints: an Introduction. MIT Press, 1998.
• 19: B.J. McAdam. Graphs for recording type information. Technical Report ECS-LFCS-99-415, The University of Edinburgh, 1999.
• 20: Bruce J. McAdam, Generalising Techniques for Type Debugging, Selected papers from the 1st Scottish Functional Programming Workshop (SFP99), p.50-58, August 29-September 01, 1999
• 21: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, Dec 1978.
• 22: Martin Odersky , Martin Sulzmann , Martin Wehr, Type inference with constrained types, Theory and Practice of Object Systems, v.5 n.1, p.35-55, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4]
• 23: Ehud Y. Shapiro, Algorithmic Program DeBugging, MIT Press, Cambridge, MA, 1983
• 24: Peter J. Stuckey , Martin Sulzmann, A theory of overloading, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.167-178, October 04-06, 2002, Pittsburgh, PA, USA
• 25: Martin Franz Sulzmann , Paul Hudak, A general framework for hindley/milner type systems with constraints, 2000
• 26: M. Sulzmann and J. Wazny. Chameleon. http://www.comp.nus.edu.sg/~sulzmann/chameleon.
• 27: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]
• 28: 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]
• 29: J. Yang, J. Wells, P. Trinder, and G. Michaelson. Improved type error reporting. In Proceedings of 12th International Workshop on Implementation of Functional Languages, pages 71--86, 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism; Constraints

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
Hindley/Milner, constraints, overloading, type classes, type debugging, type inference