Hostname: page-component-7c8c6479df-24hb2 Total loading time: 0 Render date: 2024-03-29T11:56:22.677Z Has data issue: false hasContentIssue false

On Termination, Confluence and Consistent CHR-based Type Inference

Published online by Cambridge University Press:  21 July 2014

GREGORY J. DUCK
Affiliation:
Department of Computer Science, National University of Singapore (e-mail: gregory@comp.nus.edu.sg)
RÉMY HAEMMERLÉ
Affiliation:
Universidad Politécnica de Madrid & IMDEA Software Institute (e-mail: Remy.Haemmerle@imdea.org)
MARTIN SULZMANN
Affiliation:
Hochschule Karlsruhe - Technik und Wirtschaft (e-mail: Martin.Sulzmann@hs-karlsruhe.de)

Abstract

We consider the application of Constraint Handling Rules (CHR) for the specification of type inference systems, such as that used by Haskell. Confluence of CHR guarantees that the answer provided by type inference is correct and consistent. The standard method for establishing confluence relies on an assumption that the CHR program is terminating. However, many examples in practice give rise to non-terminating CHR programs, rendering this method inapplicable. Despite no guarantee of termination or confluence, the Glasgow Haskell Compiler (GHC) supports options that allow the user to proceed with type inference anyway, e.g. via the use of the UndecidableInstances flag. In this paper we formally identify and verify a set of relaxed criteria, namely range-restrictedness, local confluence, and ground termination, that ensure the consistency of CHR-based type inference that maps to potentially non-terminating CHR programs.

Type
Regular Papers
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abdennadher, S., Frühwirth, T., and Meuss, H. 1999. Confluence and semantics of Constraint Simplification Rules. Constraints 4, 2, 133165.CrossRefGoogle Scholar
Duck, G. 2012. SMCHR: Satisfiability modulo Constraint Handling Rules. Theory and Practice of Logic Programming, Proceedings of the 28th International Conference on Logic Programming Special Issue 12, 4-5, 601618.CrossRefGoogle Scholar
Duck, G., Jaffar, J., and Koh, N. 2013. Constraint-based program reasoning with heaps and separation. In Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming. LNCS, vol. 8124. Springer, 282298.CrossRefGoogle Scholar
Duck, G., Stuckey, P., and Sulzmann, M. 2007. Observable confluence for Constraint Handling Rules. In Proceedings of the 23rd International Conference on Logic Programming. LNCS, vol. 4670. Springer, 224239.Google Scholar
Frühwirth, T. 2000. Proving termination of constraint solver programs. In New Trends in Constraints. LNCS, vol. 1865. Springer, 298317.CrossRefGoogle Scholar
Frühwirth, T. 2009. Constraint Handling Rules, 1st ed. Cambridge University Press.Google Scholar
GHC 2014. The Glasgow Haskell Compiler. http://www.haskell.org/ghc/.Google Scholar
Giesl, J., Schneider-Kamp, P., and Thiemann, R. 2006. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In Proceedings of the 3rd International Joint Conference on Automated Reasoning. LNCS, vol. 4130. Springer, 281286.CrossRefGoogle Scholar
Haemmerlé, R. 2011. (Co)-inductive semantics for Constraint Handling Rules. Theory and Practice of Logic Programming, Proceedings of the 27th International Conference on Logic Programming Special Issue 11, 4–5, 593609.Google Scholar
Haemmerlé, R. 2012. Diagrammatic confluence for Constraint Handling Rules. Theory and Practice of Logic Programming, Proceedings of the 28th International Conference on Logic Programming Special Issue 12, 4–5, 737753.CrossRefGoogle Scholar
Haemmerlé, R., Lopez-Garcia, P., and Hermenegildo, M. 2011. CLP projection for Constraint Handling Rules. In Proceedings of the 13th International Symposium on Principles and Practices of Declarative Programming. ACM, 137148.Google Scholar
Hallgren, T. 2001. Fun with functional dependencies. In Proceedings of the Joint CS/CE Winter Meeting. Department of Computing Science, Chalmers, Sweden, 135145.Google Scholar
Jones, M. P. 2000. Type classes with functional dependencies. In Proceedings of the 9th European Symposium on Programming. LNCS, vol. 1782. Springer, 230244.Google Scholar
Jones, S. P., Ed. 2003. Haskell 98 Language and Libraries – The Revised Report. Cambridge University Press.Google Scholar
Newman, M. H. A. 1942. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics 43, 2, 223243.CrossRefGoogle Scholar
Pilozzi, P. and Schreye, D. D. 2008. Termination analysis of CHR revisited. In Proceedings of the 24th International Conference on Logic Programming. LNCS, vol. 5366. Springer, 501515.Google Scholar
Schrijvers, T., Jones, S. P., Chakravarty, M., and Sulzmann, M. 2008. Type checking with open type functions. In Proceedings of the 13th International Conference on Functional Programming. ACM, 5162.Google Scholar
Sneyers, J., Weert, P. V., Schrijvers, T., and Koninck, L. D. 2010. As time goes by: Constraint Handling Rules. Theory and Practice of Logic Programming 10, 1, 147.CrossRefGoogle Scholar
Somogyi, Z., Henderson, F., and Conway, T. 1996. The execution algorithm of mercury, an efficient purely declarative logic programming language. Journal of Logic Programming 29, 1–3, 1764.CrossRefGoogle Scholar
Stuckey, P. and Sulzmann, M. 2005. A theory of overloading. Transactions on Programming Languages and Systems 27, 6, 12161269.CrossRefGoogle Scholar
Sulzmann, M., Duck, G., Jones, S. P., and Stuckey, P. 2007. Understanding functional dependencies via Constraint Handling Rules. Journal of Functional Programming 17, 1, 83129.Google Scholar
Wadler, P. and Blott, S. 1989. How to make ad-hoc polymorphism less ad-hoc . In Proceedings of the 17th Symposium on Principles of Programming Languages. ACM, 6076.Google Scholar