Peter J. Stuckey
Martin Sulzmann
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.
- 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.]]Google Scholar
Digital Library
- Abdennadher, S. and Frühwirth, T. 1998. On completion of constraint handling rules. In Proceedings of the 4th International Conference on Principles and Practice of Constraint Programming (CP98). Lecture Notes in Computer Science, vol. 1520. Springer-Verlag, New York, 25--39.]] Google ScholarDigital Library
- Abdennadher, S. and Schütz, H. 1998. CHRˇ : A flexible query language. In Proceedings of Flexible Query Answering Systems. Lecture Notes in Artificial Intelligence, vol. 1495. Springer-Verlag, New York, 1--14.]] Google ScholarDigital Library
- Augustsson, L. 1998. Cayenne---A language with dependent types. In Proceedings of the International Conference on Functional Programming (ICFP 1998). 239--250.]] Google ScholarDigital Library
- Breazu-Tannen, V., Gunter, C. A., and Scedrov, A. 1990. Computing with coercions. In Proceedings of the Conference on LISP and Functional Programming (Nice, France) ACM, New York, 44--60.]] Google ScholarDigital Library
- Camarao, C. and Figueiredo, L. 1999. Type inference for overloading without restrictions, declarations or annotations. In Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming. Lecture Notes in Computer Science, vol. 1722, Springer-Verlag, New York, 37--52.]] Google ScholarDigital Library
- Chen, K., Hudak, P., and Odersky, M. 1992. Parametric type classes. In Proceedings of the ACM Conference on LISP and Functional Programming. ACM, New York, 170--191.]] Google ScholarDigital Library
- Demoen, B., García de la Banda, M., Harvey, W., Marriott, K., and Stuckey, P. 1999. An overview of HAL. In Proceedings of the 4th International Conference on Principles and Practices of Constraint Programming. Lecture Notes in Computer Science, Springer-Verlag, New York, 174--188.]] Google ScholarDigital Library
- Duggan, D. and Ophel, J. 2002a. Open and closed scopes for constrained genericity. Theoret. Comput. Sci. 275, 1--2, 215--258.]] Google ScholarDigital Library
- Duggan, D. and Ophel, J. 2002b. Type-checking multi-parameter type classes. J. Funct. Prog. 12, 2, 133--158.]] Google ScholarDigital Library
- Fridlender, D. and Indrika, M. 2000. Do we need dependent types? J. Funct. Prog. 10, 4, 409--415.]] Google ScholarDigital Library
- Frühwirth, T. 1995. Constraint handling rules. In Constraint Programming: Basics and Trends. Lecture Notes in Computer Science, vol. 910. Springer-Verlag, NewYork.]]Google Scholar
- Frühwirth, T. 1998a. A declarative language for constraint systems: Habilitation. Institut für Informatik, Ludwig-Maximilians-University Munich, Germany, July.]]Google Scholar
- Frühwirth, T. 1998b. Theory and practice of constraint handling rules. J. Logic Prog. 37, 1--3, 95--138.]]Google ScholarCross Ref
- Gasbichler, M., Neubauer, M., Sperber, M., and Thiemann, P. 2002. Functional logic overloading. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, OR). ACM, New York, 233--244.]] Google ScholarDigital Library
- GHC 2003. Glasgow Haskell Compiler Home Page. http://www.haskell.org/ghc/.]]Google Scholar
- 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.]]Google Scholar
- Hanus, M. 1994. The integration of functions into logic programming: From theory to practice. J. Logic Prog. 19&20, 583--628.]]Google Scholar
- Henglein, F. 1993. Type inference with polymorphic recursion. Trans. Prog. Lang. Syst. 15, 1 (April), 253--289.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Jones, M. P. 1992. Qualified types: Theory and practice. Ph.D. dissertation, Oxford University.]] Google ScholarDigital Library
- Jones, M. P. 1993a. Coherence for qualified types. Research Report YALEU/DCS/RR-989, Yale University, Department of Computer Science. September.]]Google Scholar
- Jones, M. P. 1993b. A system of constructor classes: Overloading and implicit higher-order polymorphism. In FPCA '93: Proceedings of the Conference on Functional Programming Languages and Computer Architecture. ACM, New York, 52--61.]] Google ScholarDigital Library
- Jones, M. P. 2000. Type classes with functional dependencies. In Proceedings of the 9th European Symposium on Programming Languages and Systems, ESOP 2000. Lecture Notes in Computer Science, vol. 1782, Springer-Verlag, New York.]] Google ScholarDigital Library
- Jones, S. P., Jones, M. P., and Meijer, E. 1997. Type classes: An exploration of the design space. In Haskell Workshop.]]Google Scholar
- Kaes, S. 1988. Parametric overloading in polymorphic programming languages. In ESOP'88. In Proceedings of the Programming Languages and Systems. Lecture Notes in Computer Science, vol. 300. Springer-Verlag, New York, 131--141.]] Google ScholarDigital Library
- Lewis, J., Shields, M., Meijer, E., and Launchbury, J. 2000. Implicit parameters: Dynamic scoping with static types. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Boston, MA). ACM, New York, 108--118.]] Google ScholarDigital Library
- Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.]]Google ScholarCross Ref
- Nipkow, T. and Prehofer, C. 1995. Type reconstruction for type classes. J. Funct. Prog. 5, 2, 201--224.]]Google ScholarCross Ref
- Odersky, M., Sulzmann, M., and Wehr, M. 1999. Type inference with constrained types. Theory Pract. Obj. Syst. 5, 1, 35--55.]] Google ScholarDigital Library
- Odersky, M., Wadler, P., and Wehr, M. 1995. A second look at overloading. In Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture (FPCA'95) (La Jolla, CA). ACM, New York, 135--146.]] Google ScholarDigital Library
- Peyton Jones, S. 2003. Haskell 98 Language and Libraries: the Revised Report. Cambridge University Press. (Also see http://www.haskell.org/definition/.)]]Google Scholar
- 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.]]Google Scholar
- Shields, M. and Jones, S. P. 2001. Object-oriented overloading for Haskell. In Proceedings of the Workshop on Multi-Language Infrastructure and Interoperability.]]Google Scholar
- Shoenfield, J. 1967. Mathematical Logic. Addison-Wesley, Reading, MA.]]Google Scholar
- 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.]]Google ScholarCross Ref
- Stuckey, P. J. and Sulzmann, M. 2002. A theory of overloading. In Proceedings of ICFP'02. 167--178.]] Google ScholarDigital Library
- Sulzmann, M. 2000. A general framework for Hindley/Milner type systems with constraints. Ph.D. dissertation, Yale University.]] Google ScholarDigital Library
- Sulzmann, M. and Wazny, J. 2003. The Chameleon system. http://www.comp.nus.edu.sg/~sulzmann/chameleon.]]Google Scholar
- Wadler, P. and Blott, S. 1989. How to make ad-hoc polymorphism less ad-hoc. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages (POPL). ACM, New York, 60--76.]] Google ScholarDigital Library
- Yang, Z. 1998. Encoding types in ML-like languages. In Proceedings of ACM SIGPLAN International Conference on Functional Programming. ACM, New York, 289--300.]] Google ScholarDigital Library
Index Terms
- A theory of overloading
Recommendations
A theory of overloading
We present a minimal extension of the Hindley/Milner system to allow for overloading of identifiers. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling Rules (CHRs). CHRs are a declarative language for ...
Interactive type debugging in Haskell
Haskell '03: Proceedings of the 2003 ACM SIGPLAN workshop on HaskellIn 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 ...
A theory of overloading
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programmingWe present a minimal extension of the Hindley/Milner system to allow for overloading of identifiers. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling Rules (CHRs). CHRs are a declarative language for ...
Reviews
Dachuan Yu
Overloading, also know as ad hoc polymorphism, is a powerful programming feature that allows one named function to be dispatched to different implementations based on the argument types. For instance, a "+" operator could be overloaded to work not only on integers as addition, but also on strings as concatenation. In general, overloading is useful when one wishes to define a function on multiple argument types with specialized implementations. This contrasts with parametric polymorphism, where a function is written generically to work for arguments of all types. Overloading has been studied in the context of the Hindley/Milner system, and, in particular, in the style of Haskell type classes. This paper proposes a general framework for overloading based on user-definable constraint handling rules (CHRs), and provides a common foundation for handling many previous systems in the area. It identifies some sufficient conditions on the CHRs for achieving decidable type inference and coherent semantic meaning of programs, and presents a complete type inference algorithm and a semantic meaning to programs under these CHRs. The ideas have been implemented as part of the Chameleon system. This paper mainly targets programming language theorists, and provides a novel approach and formal basis for understanding and enhancing overloading in the spirit of type classes. It also sheds light on encoding logic programs in the type language of type class systems. Although substantial background in the area is needed to appreciate the complete details, intermediate readers will benefit, with the help of a series of examples given throughout the paper. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments