Abstract
Type systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. Functional logic languages have inherited Damas & Milner type system from their functional part due to its simplicity and popularity. In this paper we address a couple of aspects that can be subject of improvement. One is related to a problematic feature of functional logic languages not taken under consideration by standard systems: it is known that the use of opaque HO patterns in left-hand sides of program rules may produce undesirable effects from the point of view of types. We re-examine the problem, and propose a Damas & Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety, as proved by a subject reduction result that uses HO-let-rewriting, a recently proposed reduction mechanism for HO functional logic programs. The other aspect is the different ways in which polymorphism of local definitions can be handled. At the same time that we formalize the type system, we have made the effort of technically clarifying the overall process of type inference in a whole program.
This work has been partially supported by the Spanish projects Merit-Forms-UCM (TIN2005-09207-C03-03), STAMP (TIN2008-06622-C03-01), Promesas-CAM (S-0505/TIC/0407) and GPD-UCM (UCM-BSCH-GR58/08-910502).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Antoy, S., Tolmach, A.P.: Typed higher-order narrowing without higher-order strategies. In: Middeldorp, A. (ed.) FLOPS 1999. LNCS, vol. 1722, pp. 335–353. Springer, Heidelberg (1999)
Brassel, B.: Two to three ways to write an unsafe type cast without importing unsafe - Post to the Curry mailing list (May 2008), http://www.informatik.uni-kiel.de/~curry/listarchive/0705.html
Damas, L.: Type Assignment in Programming Languages. PhD thesis, University of Edinburgh (April 1985)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proc. Symposium on Principles of Programming Languages (POPL 1982), pp. 207–212 (1982)
González-Moreno, J., Hortalá-González, T., Rodríguez-Artalejo, M.: A higher order rewriting logic for functional logic programming. In: Proc. International Conference on Logic Programming (ICLP 1997), pp. 153–167. MIT Press, Cambridge (1997)
González-Moreno, J., Hortalá-González, T., Rodríguez-Artalejo, M.: Polymorphic types in functional logic programming. Journal of Functional and Logic Programming 2001/S01, 1–71 (2001)
Hanus, M.: Multi-paradigm declarative languages. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 45–75. Springer, Heidelberg (2007)
Hanus, M. (ed.): Curry: An integrated functional logic language (version 0.8.2) (March 2006), http://www.informatik.uni-kiel.de/~curry/report.html
Jones, S.L.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for gadts. In: Proc. 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, pp. 50–61. ACM, New York (2006)
Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst. 15(2), 290–311 (1993)
López-Fraguas, F.J., Rodríguez-Hortalá, J., Sánchez-Hernández, J.: Rewriting and call-time choice: the HO case. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 147–162. Springer, Heidelberg (2008)
López-Fraguas, F., Sánchez-Hernández, J.: \(\mathcal{TOY}\): A multiparadigm declarative system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 244–247. Springer, Heidelberg (1999)
Martin-Martin, E.: Advances in type systems for functional-logic programming. Master’s thesis, Universidad Complutense de Madrid (July 2009), http://gpd.sip.ucm.es/enrique/publications/master/masterThesis.pdf
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10(3), 470–502 (1988)
Moreno-Navarro, J.J., Mariño, J., del Pozo-Pietro, A., Herranz-Nieva, Á., García-Martín, J.: Adding type classes to functional-logic languages. In: 1996 Joint Conf. on Declarative Programming, APPIA-GULP-PRODE 1996, pp. 427–438 (1996)
Mycroft, A.: Polymorphic type schemes and recursive definitions. In: Paul, M., Robinet, B. (eds.) Programming 1984. LNCS, vol. 167, pp. 217–228. Springer, Heidelberg (1984)
Peyton Jones, S.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)
Pierce, B.P.: Advanced topics in types and programming languages. MIT Press, Cambridge (2005)
Reade, C.: Elements of Functional Programming. Addison-Wesley, Reading (1989)
Sedgewick, R.: Algorithms in C++, Part 5: Graph Algorithms, pp. 205–216. Addison-Wesley Professional, Reading (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
López-Fraguas, F.J., Martin-Martin, E., Rodríguez-Hortalá, J. (2010). New Results on Type Systems for Functional Logic Programming . In: Escobar, S. (eds) Functional and Constraint Logic Programming. WFLP 2009. Lecture Notes in Computer Science, vol 5979. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11999-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-11999-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11998-9
Online ISBN: 978-3-642-11999-6
eBook Packages: Computer ScienceComputer Science (R0)