Safe typing of functional logic programs with opaque patterns and local bindings. (English) Zbl 1358.68058
Summary: Type systems are widely used in programming languages as a powerful tool providing safety to programs. 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 two variants of a Damas-Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety. The considered formal framework is that of programs without extra variables and using let-rewriting as reduction mechanism. The other aspect addressed 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.
References:
| [1] | Damas, L.; Milner, R., Principal type-schemes for functional programs, (Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’82 (1982), ACM), 207-212 |
| [2] | López-Fraguas, F.; Sánchez-Hernández, J., Toy: A multiparadigm declarative system, (Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Proceedings of the 10th International Conference on Rewriting Techniques and Applications, RTA ’99. Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Proceedings of the 10th International Conference on Rewriting Techniques and Applications, RTA ’99, Lect. Notes Comput. Sci., vol. 1631 (1999), Springer), 244-247 |
| [3] | Hanus, M., Curry: An integrated functional logic language (2006), (version 0.8.2), available at |
| [4] | Hanus, M., Multi-paradigm declarative languages, (Proceedings of the 23rd International Conference on Logic Programming. Proceedings of the 23rd International Conference on Logic Programming, ICLP ’07. Proceedings of the 23rd International Conference on Logic Programming. Proceedings of the 23rd International Conference on Logic Programming, ICLP ’07, Lect. Notes Comput. Sci., vol. 4670 (2007), Springer), 45-75 · Zbl 1213.68162 |
| [7] | Martin-Martin, E., Type classes in functional logic programming, (Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’11 (2011), ACM), 121-130 |
| [8] | González-Moreno, J.; Hortalá-González, T.; Rodríguez-Artalejo, M., A higher order rewriting logic for functional logic programming, (Proceedings of the 14th International Conference on Logic Programming. Proceedings of the 14th International Conference on Logic Programming, ICLP ’97 (1997), MIT Press), 153-167 |
| [9] | López-Fraguas, F.; Rodríguez-Hortalá, J.; Sánchez-Hernández, J., Rewriting and call-time choice: the HO case, (Proceedings of the 9th International Symposium on Functional and Logic Programming. Proceedings of the 9th International Symposium on Functional and Logic Programming, FLOPS ’08. Proceedings of the 9th International Symposium on Functional and Logic Programming. Proceedings of the 9th International Symposium on Functional and Logic Programming, FLOPS ’08, Lect. Notes Comput. Sci., vol. 4989 (2008), Springer), 147-162 · Zbl 1137.68338 |
| [10] | Caballero, R.; López-Fraguas, F., A functional-logic perspective on parsing, (Proceedings of the 4th International Symposium on Functional and Logic Programming. Proceedings of the 4th International Symposium on Functional and Logic Programming, FLOPS ’99 (1999), Springer), 85-99 · Zbl 0988.68524 |
| [11] | Caballero, R.; García-Ruiz, Y.; Sáenz-Pérez, F., Integrating xpath with the functional-logic language toy, (Rocha, R.; Launchbury, J., Proceedings of the 13th International Symposium on Practical Aspects of Declarative Languages. Proceedings of the 13th International Symposium on Practical Aspects of Declarative Languages, PADL ’11. Proceedings of the 13th International Symposium on Practical Aspects of Declarative Languages. Proceedings of the 13th International Symposium on Practical Aspects of Declarative Languages, PADL ’11, Lect. Notes Comput. Sci., vol. 6539 (2011), Springer), 145-159 |
| [12] | Fischer, S., Call-time choice and extensionality - post to the Curry mailing list (2011) |
| [13] | González-Moreno, J.; Hortalá-González, T.; Rodríguez-Artalejo, M., Polymorphic types in functional logic programming, J. Funct. Logic Program., 2001 (2001) · Zbl 0971.68081 |
| [14] | Brassel, B., Two to three ways to write an unsafe type cast without importing unsafe - post to the Curry mailing list (2008) |
| [15] | López-Fraguas, F.; Martin-Martin, E.; Rodríguez-Hortalá, J., Liberal typing for functional logic programs, (Proceedings of the 8th Asian Symposium on Programming Languages and Systems. Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS ’10. Proceedings of the 8th Asian Symposium on Programming Languages and Systems. Proceedings of the 8th Asian Symposium on Programming Languages and Systems, APLAS ’10, Lect. Notes Comput. Sci., vol. 6461 (2010), Springer), 80-96 |
| [16] | Lux, W., Münster Curry user’s guide, release 0.9.11 (2007) |
| [17] | Wright, A. K., Simple imperative polymorphism, LISP Symb. Comput., 8, 343-355 (1995) |
| [18] | Hudak, P.; Hughes, J.; Peyton Jones, S.; Wadler, P., A history of Haskell: Being lazy with class, (Proceedings of the 3rd ACM SIGPLAN Conference on History of Programming Languages. Proceedings of the 3rd ACM SIGPLAN Conference on History of Programming Languages, HOPL III (2007), ACM), 12-1-12-55 |
| [19] | Mitchell, J. C.; Plotkin, G. D., Abstract types have existential type, ACM Trans. Program. Lang. Syst., 10, 470-502 (1988) |
| [20] | Läufer, K.; Odersky, M., Polymorphic type inference and abstract data types, ACM Trans. Program. Lang. Syst., 16, 1411-1430 (1994) |
| [21] | Xi, H.; Chen, C.; Chen, G., Guarded recursive datatype constructors, SIGPLAN Not., 38, 224-235 (2003) · Zbl 1321.68161 |
| [22] | Cheney, J.; Hinze, R., First-class phantom types (2003), Cornell University, Technical Report TR2003-1901 |
| [23] | Damas, L., Type assignment in programming languages (1985), University of Edinburgh, Also appeared as Technical report CST-33-85 |
| [24] | Peyton Jones, S., The Implementation of Functional Programming Languages, Prentice-Hall International Series in Computer Science (1987) · Zbl 0712.68017 |
| [25] | Mycroft, A., Polymorphic type schemes and recursive definitions, (Proceedings of the 6th Colloquium on International Symposium on Programming (1984), Springer), 217-228 · Zbl 0548.68010 |
| [26] | Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P., Type reconstruction in the presence of polymorphic recursion, ACM Trans. Program. Lang. Syst., 15, 290-311 (1993) |
| [27] | Tarjan, R., Depth-first search and linear graph algorithms, SIAM J. Comput., 1, 146-160 (1972) · Zbl 0251.05107 |
| [28] | Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, ACM Comput. Surv., 17, 471-522 (1985) |
| [29] | Perry, N., The implementation of practical functional programming languages (1991), Imperial College, PhD thesis |
| [30] | Reynolds, J. C., Types, abstraction and parametric polymorphism, Inf. Process., 513-523 (1983) |
| [31] | Wadler, P., Theorems for free!, (Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture. Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture, FPCA ’89 (1989), ACM), 347-359 |
| [32] | Seidel, D.; Voigtländer, J., Automatically generating counterexamples to naive free theorems, (Proceedings of 10th International Symposium on Functional and Logic Programming. Proceedings of 10th International Symposium on Functional and Logic Programming, FLOPS ’10. Proceedings of 10th International Symposium on Functional and Logic Programming. Proceedings of 10th International Symposium on Functional and Logic Programming, FLOPS ’10, Lect. Notes Comput. Sci., vol. 6009 (2010), Springer), 175-190 · Zbl 1284.68200 |
| [33] | Johann, P.; Voigtländer, J., Free theorems in the presence of seq, (Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’04 (2004), ACM), 99-110 · Zbl 1325.68047 |
| [34] | Christiansen, J.; Seidel, D.; Voigtländer, J., Free theorems for functional logic programs, (Proceedings of the 4th ACM SIGPLAN Workshop on Programming Languages Meets Program Verification. Proceedings of the 4th ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, PLPV ’10 (2010), ACM), 39-48 |
| [35] | Schrijvers, T.; Peyton Jones, S.; Sulzmann, M.; Vytiniotis, D., Complete and decidable type inference for GADTs, (Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP ’09 (2009), ACM), 341-352 · Zbl 1302.68190 |
| [36] | Odersky, M.; Sulzmann, M.; Wehr, M., Type inference with constrained types, Theory Pract. Object Syst., 5, 35-55 (1999) |
| [37] | Antoy, S.; Hanus, M., Overlapping rules and logic variables in functional logic programs, (Proceedings of the 22nd International Conference on Logic Programming. Proceedings of the 22nd International Conference on Logic Programming, ICLP ’06. Proceedings of the 22nd International Conference on Logic Programming. Proceedings of the 22nd International Conference on Logic Programming, ICLP ’06, Lect. Notes Comput. Sci., vol. 4079 (2006), Springer), 87-101 · Zbl 1131.68364 |
| [38] | de Dios Castro, J.; López-Fraguas, F. J., Extra variables can be eliminated from functional logic programs, Electron. Notes Theor. Comput. Sci., 188, 3-19 (2007) · Zbl 1278.68063 |
| [39] | Antoy, S.; Hanus, M., Functional logic programming, Commun. ACM, 53, 74-85 (2010) |
| [40] | Antoy, S.; Tolmach, A., Typed higher-order narrowing without higher-order strategies, (Proceedings of the 4th International Symposium on Functional and Logic Programming. Proceedings of the 4th International Symposium on Functional and Logic Programming, FLOPS ’99. Proceedings of the 4th International Symposium on Functional and Logic Programming. Proceedings of the 4th International Symposium on Functional and Logic Programming, FLOPS ’99, Lect. Notes Comput. Sci., vol. 1722 (1999), Springer), 335-352 · Zbl 0988.68091 |
| [41] | López-Fraguas, F.; Martin-Martin, E.; Rodríguez-Hortalá, J., Well-typed narrowing with extra variables in functional-logic programming, (Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’12 (2012), ACM), 83-92 |
| [42] | López-Fraguas, F.; Martin-Martin, E.; Rodríguez-Hortalá, J., New results on type systems for functional logic programming, (18th International Workshop on Functional and (Constraint) Logic Programming. 18th International Workshop on Functional and (Constraint) Logic Programming, WFLP ’09. 18th International Workshop on Functional and (Constraint) Logic Programming. 18th International Workshop on Functional and (Constraint) Logic Programming, WFLP ’09, Lect. Notes Comput. Sci., vol. 5979 (2010), Springer), 128-144 · Zbl 1274.68045 |
| [43] | Martin-Martin, E., Advances in type systems for functional logic programming (2009), Universidad Complutense de Madrid, available at |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
