A theory of overloading

ABSTRACT

We present a novel approach to allow for overloading of identifiers in the spirit of type classes. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling Rules (CHRs). CHRs are a declarative language for writing incremental constraint solvers, that provide our scheme with a form of programmable type language. CHRs allow us to precisely describe the relationships among overloaded identifiers. Under some sufficient conditions on the CHRs we achieve decidable type inference and the semantic meaning of programs is unambiguous. Our approach provides a common formal basis for many type class extensions such as multiparameter type classes and functional dependencies.

REFERENCES

• 1: Abdennadher, S. 1997. Operational semantics and confluence of constraint propagation rules. In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming, CP'97. Lecture Notes in Computer Science, Springer-Verlag, New York, 252--266.
• 2: Slim Abdennadher , Thom W. Frühwirth, On Completion of Constraint Handling Rules, Proceedings of the 4th International Conference on Principles and Practice of Constraint Programming, p.25-39, October 26-30, 1998
• 3: Slim Abdennadher , Heribert Schütz, CHRv: A Flexible Query Language, Proceedings of the Third International Conference on Flexible Query Answering Systems, p.1-14, May 13-15, 1998
• 4: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 5: V. Breazu-Tannen , C. A. Gunter , A. Scedrov, Computing with coercions, Proceedings of the 1990 ACM conference on LISP and functional programming, p.44-60, June 27-29, 1990, Nice, France [doi>10.1145/91556.91590]
• 6: Carlos Camarão , Lucília Figueiredo, Type Inference for Overloading without Restrictions, Declarations or Annotations, Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming, p.37-52, November 11-13, 1999
• 7: Kung Chen , Paul Hudak , Martin Odersky, Parametric type classes, Proceedings of the 1992 ACM conference on LISP and functional programming, p.170-181, June 22-24, 1992, San Francisco, California, United States
• 8: Bart Demoen , Maria J. García de la Banda , Warwick Harvey , Kim Marriott , Peter J. Stuckey, An Overview of HAL, Proceedings of the 5th International Conference on Principles and Practice of Constraint Programming, p.174-188, October 11-14, 1999
• 9: Dominic Duggan , John Ophel, Open and closed scopes for constrained genericity, Theoretical Computer Science, v.275 n.1-2, p.215-258, March 28 2002 [doi>10.1016/S0304-3975(01)00129-3]
• 10: Dominic Duggan , John Ophel, Type-checking multi-parameter type classes, Journal of Functional Programming, v.12 n.2, p.133-158, March 2002 [doi>10.1017/S0956796801004233]
• 11: Daniel Fridlender , Mia Indrika, Do we need dependent types?, Journal of Functional Programming, v.10 n.4, p.409-415, July 2000 [doi>10.1017/S0956796800003658]
• 12: Frühwirth, T. 1995. Constraint handling rules. In Constraint Programming: Basics and Trends. Lecture Notes in Computer Science, vol. 910. Springer-Verlag, NewYork.
• 13: Frühwirth, T. 1998a. A declarative language for constraint systems: Habilitation. Institut für Informatik, Ludwig-Maximilians-University Munich, Germany, July.
• 14: Frühwirth, T. 1998b. Theory and practice of constraint handling rules. J. Logic Prog. 37, 1--3, 95--138.
• 15: Matthias Neubauer , Peter Thiemann , Martin Gasbichler , Michael Sperber, Functional logic overloading, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-244, January 16-18, 2002, Portland, Oregon
• 16: GHC 2003. Glasgow Haskell Compiler Home Page. http://www.haskell.org/ghc/.
• 17: Glynn, K., Stuckey, P., and Sulzmann, M. 2000. Type classes and constraint handling rules. In Proceedings of the 1st Workshop on Rule-Based Constraint Reasoning and Programming.
• 18: Hanus, M. 1994. The integration of functions into logic programming: From theory to practice. J. Logic Prog. 19&20, 583--628.
• 19: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 20: Jeffery, D., Henderson, F., and Somogyi, Z. 2000. Type classes in Mercury. In Proceedings of the 23rd Australasian Computer Science Conference. Australian Computer Science Communications, vol. 22. IEEE Computer Society Press, Los Alamitos, CA, 128--135.
• 21: Mark Philip Jones, Qualified types: theory and practice (ordering relation), 1992
• 22: Jones, M. P. 1993a. Coherence for qualified types. Research Report YALEU/DCS/RR-989, Yale University, Department of Computer Science. September.
• 23: Mark P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism, Proceedings of the conference on Functional programming languages and computer architecture, p.52-61, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165190]
• 24: Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
• 25: Jones, S. P., Jones, M. P., and Meijer, E. 1997. Type classes: An exploration of the design space. In Haskell Workshop.
• 26: Stefan Kaes, Parametric Overloading in Polymorphic Programming Languages, Proceedings of the 2nd European Symposium on Programming, p.131-144, March 21-24, 1988
• 27: Jeffrey R. Lewis , John Launchbury , Erik Meijer , Mark B. Shields, Implicit parameters: dynamic scoping with static types, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.108-118, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325708]
• 28: Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.
• 29: Nipkow, T. and Prehofer, C. 1995. Type reconstruction for type classes. J. Funct. Prog. 5, 2, 201--224.
• 30: 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]
• 31: Martin Odersky , Philip Wadler , Martin Wehr, A second look at overloading, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.135-146, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224195]
• 32: Peyton Jones, S. 2003. Haskell 98 Language and Libraries: the Revised Report. Cambridge University Press. (Also see http://www.haskell.org/definition/.)
• 33: Plasmeijer, M. and van Eekelen, M. 1998. Language report Concurrent Clean. Tech. Rep. CSI-R9816, Computing Science Institute, University of Nijmegen, Nijmegen, The Netherlands. June. ftp://ftp.cs.kun.nl/pub/Clean/Clean13/doc/refman13.ps.gz.
• 34: Shields, M. and Jones, S. P. 2001. Object-oriented overloading for Haskell. In Proceedings of the Workshop on Multi-Language Infrastructure and Interoperability.
• 35: Shoenfield, J. 1967. Mathematical Logic. Addison-Wesley, Reading, MA.
• 36: Somogyi, Z., Henderson, F., and Conway, T. 1996. The execution algorithms of Mercury: An efficient purely declarativelogic programming language. J. Logic Prog. 29, 1--3, 17--64.
• 37: 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
• 38: Martin Franz Sulzmann , Paul Hudak, A general framework for hindley/milner type systems with constraints, 2000
• 39: Sulzmann, M. and Wazny, J. 2003. The Chameleon system. http://www.comp.nus.edu.sg/~sulzmann/chameleon.
• 40: 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]
• 41: Zhe Yang, Encoding types in ML-like languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.289-300, September 26-29, 1998, Baltimore, Maryland, United States

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

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

Keywords:
Constraints, coherence, evidence translation, overloading, type classes, type inference