Liberal Typing for Functional Logic Programs
| dc.book.title | Programming Languages and Systems | |
| dc.contributor.author | López Fraguas, Francisco Javier | |
| dc.contributor.author | Martín Martín, Enrique | |
| dc.contributor.author | Rodríguez Hortalá, Juan | |
| dc.contributor.editor | Ueda, K. | |
| dc.date.accessioned | 2023-06-15T07:49:06Z | |
| dc.date.available | 2023-06-15T07:49:06Z | |
| dc.date.issued | 2010 | |
| dc.description.abstract | We propose a new type system for functional logic programming which is more liberal than the classical Damas-Milner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from Damas-Milner typing of expressions we propose a new notion of well-typed program that adds support for type-indexed functions, existential types, opaque higher-order patterns and generic functions-as shown by an extensive collection of examples that illustrate the possibilities of our proposal. In the negative side, the types of functions must be declared, and therefore types are checked but not inferred. Another consequence is that parametricity is lost, although the impact of this flaw is limited as "free theorems" were already compromised in functional logic programming because of non-determinism. | |
| dc.description.department | Sección Deptal. de Sistemas Informáticos y Computación | |
| dc.description.department | Depto. de Sistemas Informáticos y Computación | |
| dc.description.faculty | Fac. de Ciencias Matemáticas | |
| dc.description.faculty | Fac. de Informática | |
| dc.description.refereed | TRUE | |
| dc.description.sponsorship | Comunidad de Madrid | |
| dc.description.sponsorship | Ministerio de Economía y Competitividad (MINECO) | |
| dc.description.status | pub | |
| dc.eprint.id | https://eprints.ucm.es/id/eprint/35957 | |
| dc.identifier.doi | 10.1007/978-3-642-17164-2_7 | |
| dc.identifier.isbn | 978-3-642-17163-5 | |
| dc.identifier.issn | 0302-9743 | |
| dc.identifier.officialurl | http://www.springerlink.com/content/u5q8016158402754/fulltext.pdf | |
| dc.identifier.relatedurl | http://www.springerlink.com/ | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/174.1 | |
| dc.issue.number | 6461 | |
| dc.journal.title | Lecture Notes in Computer Science | |
| dc.language.iso | eng | |
| dc.page.final | 96 | |
| dc.page.initial | 80 | |
| dc.publication.place | Berlin | |
| dc.publisher | Springer | |
| dc.relation.ispartofseries | Lecture Notes in Computer Science | |
| dc.relation.projectID | Prometidos-CM (S2009/TIC-1465) | |
| dc.relation.projectID | STAMP (TIN2008-06622-C03-01) | |
| dc.relation.projectID | UCM-BSCH-GR58/08-910502. | |
| dc.rights.accessRights | restricted access | |
| dc.subject.cdu | 004.43 | |
| dc.subject.keyword | Type systems | |
| dc.subject.keyword | functional logic programming | |
| dc.subject.keyword | generic functions | |
| dc.subject.keyword | type-indexed functions | |
| dc.subject.keyword | existential types | |
| dc.subject.keyword | higher-order patterns. | |
| dc.subject.ucm | Lenguajes de programación | |
| dc.subject.unesco | 1203.23 Lenguajes de Programación | |
| dc.title | Liberal Typing for Functional Logic Programs | |
| dc.type | journal article | |
| dcterms.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) van Bakel, S., Fernández, M.: Normalization Results for Typeable Rewrite Systems. Information and Computation 33(2), 73–116 (1997) Cheney, J., Hinze, R.: First-class phantom types. Tech. Rep. TR2003-1901, Cornell University (2003) Christiansen, J., Seidel, D., Voigtländer, J.: Free theorems for functional logic programs. In: Proc. PLPV 2010, pp. 39–48. ACM, New York (2010) Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proc. POPL 1982, pp. 207–212. ACM, New York (1982) González-Moreno, J.C., Hortalá-González, T., López-Fraguas, F., Rodríguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40(1), 47–87 (1999) González-Moreno, J., Hortalá-González, M., Rodríguez-Artalejo, M.: A higher order rewriting logic for functional logic programming. In: Hill, P.M., Warren, D.S. (eds.) Proc. ICLP 1997, pp. 153–167. MIT Press, Cambridge (1997) Gonzalez-Moreno, J.C., Hortala-Gonzalez, M.T., Rodriguez-Artalejo, M.: Polymorphic types in functional logic programming. Journal of Functional and Logic Programming 2001(1) (2001) 96 F. López-Fraguas, E. Martin-Martin, and J. Rodríguez-Hortalá 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 (2006), http://www.informatik.uni-kiel.de/~curry/report.html Hinze, R.: Generics for the masses. J. Funct. Program. 16(4-5), 451–483 (2006) Hinze, R., Löh, A.: Generic programming, now! In: Backhouse, R., Gibbons, J., Hinze, R., Jeuring, J. (eds.) SSDGP 2006. LNCS, vol. 4719, pp. 150–208. Springer, Heidelberg (2007) Hudak, P., Hughes, J., Jones, S.P., Wadler, P.: A History of Haskell: being lazy with class. In: Proc. HOPL III, pp. 12-1–12-55. ACM, New York (2007) Läufer, K., Odersky,M.: Polymorphic type inference and abstract data types. ACM Transactions on Programming languages and Systems 16. ACM (1994) Löh, A., Hinze, R.: Open data types and open functions. In: Proc. PPDP 2006, pp. 133–144. ACM, New York (2006) López-Fraguas, F.J., Martin-Martin, E., Rodríguez-Hortalá, J.: Liberal Typing for Functional Logic Programs (long version). Tech. Rep. SIC-UCM, Universidad Complutense de Madrid (August 2010), http://gpd.sip.ucm.es/enrique/publications/liberalTypingFLP/long.pdf López-Fraguas, F.J., Martin-Martin, E., Rodríguez-Hortalá, J.: New results on type systems for functional logic programming. In: Escobar, S. (ed.) Functional and Constraint Logic Programming. LNCS, vol. 5979, pp. 128–144. Springer, Heidelberg (2010) López-Fraguas, F., 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.: T OY: A multiparadigm declarative system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 244–247. Springer, Heidelberg (1999) Lux, W.: Adding haskell-style overloading to curry. In: Workshop ofWorking Group 2.1.4 of the German Computing Science Association GI, pp. 67–76 (2008) Martin-Martin, E.: Implementing type classes using type-indexed functions. To appear in TPF 2010 (2010), http://gpd.sip.ucm.es/enrique/publications/implementingTypeClasses/implementingTypeClasses.pdf Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 348–375 (1978) Moreno-Navarro, J.J., Mariño, J., del Pozo-Pietro, A., Herranz-Nieva, A., García-Martín, J.: Adding type classes to functional-logic languages. In: Proc. APPIAGULP-PRODE 1996, pp. 427–438 (1996) Peyton Jones, S., Vytiniotis, D., Weirich, S.: Simple unification-based type inference for GADTs. Tech. Rep. MS-CIS-05-22, Univ. Pennsylvania (2006) Schrijvers, T., Peyton Jones, S., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for GADTs. In: Proc. ICFP 2009, pp. 341–352. ACM, New York (2009) Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proc.POPL 1989, pp. 60–76. ACM, New York (1989) Wadler, P.: Theorems for free! In: Proc. FPCA 1989, pp. 347–359. ACM, New York (1989) Wright, A.K., Felleisen, M.: A Syntactic Approach to Type Soundness. Information and Computation 115, 38–94 (1992) | |
| dspace.entity.type | Publication | |
| relation.isAuthorOfPublication | 9f1acb56-806e-4ab4-b939-8b692d5629bd | |
| relation.isAuthorOfPublication | 8c7dbac8-1093-454e-a0cf-e7b2f316cf09 | |
| relation.isAuthorOfPublication | 19b4fb29-4f3e-4062-a5bd-59e19e25c448 | |
| relation.isAuthorOfPublication.latestForDiscovery | 8c7dbac8-1093-454e-a0cf-e7b2f316cf09 |
