Constraint-set satisfiability for overloading

ABSTRACT

This article discusses the problem of constraint-set satisfiability (CSSAT) --- that is, the problem of determining whether a given constraint-set is satisfiable in a given typing context --- in the context of systems with support for overloading and parametric polymorphism. The paper reviews previous works on constraint-set satisfiability, showing that overloading policies used in order to guarantee decidability of CSSAT have been generally too restrictive. An algorithm is proposed that does not impose a severe restriction on possible overloadings and decides CSSAT in an expectedly vast majority of cases of practical interest. In cases for which satisfiability cannot be decided, a configurable limit on the number of iterations is used to guarantee termination.

REFERENCES

• 1: 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
• 2: 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
• 3: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 4: Lucília Figueiredo, Carlos Camarão and Cristiano Vasconcellos. Constraint-set Satisfiability for Overloading. Technical report, UFMG, 2003.
• 5: Fergus Henderson, David Jeffery and Zoltan Zomogyi. Type Classes in Mercury. Technical Report 98/13, University of Melbourne, 1998.
• 6: Bart Demoen, María García de la Banda, and Peter J. Stuckey. Type Constraint Solving for Parametric and Ad-hoc Polymorphism. In Proceedings of the 22nd Australasian Computer Science Conference, 1999.
• 7: Dominic Duggan , Gordon Cormack , John Ophel, Kinded type inference for parametric overloading, Acta Informatica, v.33 n.1, p.21-68, 1996 [doi>10.1007/s002360050035]
• 8: 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]
• 9: 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]
• 10: Cordelia V. Hall , Kevin Hammond , Simon L. Peyton Jones , Philip L. Wadler, Type classes in Haskell, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.2, p.109-138, March 1996 [doi>10.1145/227699.227700]
• 11: 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]
• 12: Daan Leijen and Erik Meijer. Parsec: Direct Style Monadic Parser Combinators for the Real World. Technical Report UU-CS-2001-35, Department of Computer Science, Universiteit Utrecht, 2001. http://www.cs.uu.nl/~daan/parsec.html.
• 13: Mark Jones. Qualified Types. Cambridge University Press, 1994.
• 14: Mark Jones. A system of constructor classes: overloading and higher-order polymorphism. Journal of Functional Programming, 5(1):1--36, 1995.
• 15: Mark P. Jones, Simplifying and improving qualified types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.160-169, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224198]
• 16: Mark Jones. Typing Haskell in Haskell. In Proceedings of the 1999 Haskell Workshop. Published in Technical Report UU-CS-1999-28, Department of Computer Science, University of Utrecht. Available at http://www.cse.ogi.edu/~mpj/thih/
• 17: Stefan Kaes, Parametric Overloading in Polymorphic Programming Languages, Proceedings of the 2nd European Symposium on Programming, p.131-144, March 21-24, 1988
• 18: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, 1978.
• 19: John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
• 20: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 21: Tobias Nipkow and Christian Prehofer. Type Reconstruction for Type Classes. Journal of Functional Programming, 1(1):1--100, 1993.
• 22: 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]
• 23: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 24: Helmut Seidl, Haskell overloading is DEXPTIME-complete, Information Processing Letters, v.52 n.2, p.57-60, Oct. 28, 1994 [doi>10.1016/0020-0190(94)00130-8]
• 25: Mark Shields and Simon Peyton Jones. Object-oriented style overloading for Haskell. In Workshop on Multi-Language Infrastructure and Interoperability (BABEL'01), 2001. Available at http://haskell.readscheme.org/lang_sem.html.
• 26: Geoffrey Seward Smith, Polymorphic type inference for languages with overloading and subtyping, Cornell University, Ithaca, NY, 1992
• 27: Geoffrey S. Smith, Principal type schemes for functional programs with overloading and subtyping, Science of Computer Programming, v.23 n.2-3, p.197-226, Dec. 1994
• 28: 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
• 29: Cristiano Vasconcellos, Lucília Figueiredo, and Carlos Camarão. A Practical Type Inference for Polymorphic Recursion using Haskell. Journal of Universal Computer Science, 9(8):873--890, 2003.
• 30: Dennis Volpano. Haskell-style Overloading is NP-hard. In Proceedings of the 1994 International Conference on Computer Languages, pages 88--95, 1994.
• 31: Dennis M. Volpano, Lower bounds on type checking overloading, Information Processing Letters, v.57 n.1, p.9-13, Jan. 15, 1996 [doi>10.1016/0020-0190(95)00184-0]
• 32: Dennis M. Volpano , Geoffrey Smith, On the Complexity of ML Typability with Overloading, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, p.15-28, August 26-30, 1991
• 33: 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]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages

Keywords:
ad-hoc polymorphism, constrained polymorphism, constraint-set satisfiability, overloading, type constraints