Advances in type systems for functional logic programming

Abstract

Los lenguajes declarativos proporcionan un nivel de programación más alto y abstracto que los lenguajes imperativos tradicionales. Los lenguajes funcionales y los lógicos son los dos paradigmas declarativos más importantes, y su combinación ha sido un tema de investigación en las últimas dos décadas. Los lenguajes lógico funcionales han heredado el clásico sistema Damas & Milner [20] de su parte funcional, debido a su simplicidad y popularidad, pero esta aproximación directa no funciona correctamente en todos los casos. Es conocido que los patrones de orden superior en los lados izquierdos de las reglas de programa pueden producir efectos no deseados desde el punto de vista de los tipos. En particular algunas expresiones pueden perder su tipo tras un paso de cómputo. En este trabajo proponemos una extensión del clásico sistema de tipos Damas & Milner que arregla esta situación. Este problema fue detectado por primera vez en [24], y la solución propuesta fue prohibir los patrones de orden superior opacos. Nosotros proponemos una forma más relajada de abordar este problema, haciendo una distinción entre variables transparentes y opacas. Una variable es transparente en un patrón si su tipo está unívocamente determinado por el tipo del patrón, y es opaca en otro caso. Nosotros prohibimos solamente la aparición de variables opacas cuando son usadas en los lados derechos de las reglas. Hemos desarrollado el sistema de tipos tratando de clarificar el comportamiento (desde el punto de vista de los tipos) que las declaraciones locales tienen en diferentes implementaciones de lenguajes funcionales y lógico funcionales. Éste es un aspecto que varía mucho, y usualmente no está bien documentado ni formalizado. Aparte del sistema de tipos presentamos algoritmos de inferencia de tipos para expresiones y programas, y proporcionamos un prototipo de implementación en Prolog que será integrado próximamente en el compilador de T OY [45, 69]. Hemos prestado especial atención a los aspectos formales del trabajo. Por ello hemos desarrollado demostraciones detalladas de las propiedades del sistema de tipos, en particular de la propiedad de preservación del tipo o subject reduction (las expresiones mantienen su tipo tras la evaluación), y la corrección y completitud de los algoritmos de inferencia con respecto al sistema de tipos. [ABSTRACT] Declarative languages provide a higher and more abstract level of programming than traditional imperative languages. Functional and logic languages are the two most important declarative programming paradigms, and their combination has been a topic of research in the last two decades. Functional logic languages have inherited the classical Damas & Milner type system [20] from their functional part, due to its simplicity and popularity, but this naive approach does not work properly in all cases. It is known that higher order patterns (HO) in left-hand sides of program rules may produce undesirable effects from the point of view of types. In particular some expressions can lose their type after a step of computation. In this work we propose an extension to the classical Damas & Milner type system that fixes this situation. This problem was first detected in [24], and the proposed solution was forbidding opaque HO patterns. We propose a more relaxed way of tackle this problem, making a distinction between transparent and opaque variables. A variable is transparent in a pattern if its type is univocally fixed by the type of the pattern, and opaque otherwise. We prohibit only the occurrence of opaque variables when they are used in the right-hand side of the rules. We have developed the type system trying to clarify the behavior (from the point of view of types) that local definitions have in different implementations of functional and functional logic languages. This is an issue that varies greatly, and it is not usually well documented or formalized. Apart from the type system we also present type inference algorithms for expressions and programs, and provide a prototype of implementation in Prolog that will be soon integrated into the T OY [45, 69] compiler. We have paid special attention to the formal aspects of the work. Therefore we have developed detailed proofs of the properties of the type system, in particular the subject reduction property (expressions keep their type after evaluation), and the soundness and completeness of the inference algorithms wrt. the type system.