Navegación

Búsqueda

Búsqueda avanzada

El autor Juan Rodríguez-Hortalá ha publicado 2 artículo(s):

1 - A liberal type system for functional logic programs

We propose a new type system for functional logic programming which is more liberal than the classical DamasMilner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from DamasMilner typing of expressions, we propose a new notion of well-typed program that adds support for type-indexed functions, a particular form of existential types, opaque higherorder 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.

Autores: Francisco J. López-Fraguas / Enrique Martin-Martin / Juan Rodríguez-Hortalá / 
Palabras Clave:

2 - Polymorphic Types in Erlang Function Specifications

Erlang is a concurrent functional programming language developed by Ericsson, well suited for implementing distributed systems. Although Erlang is dynamically typed, the Dialyzer static analysis tool can be used to extract implicit type information from the programs, both for documentation
purposes and for finding errors that will definitively arise at program execution. Dialyzer is based on the notion of success types, that correspond to safe over-approximations for the semantics of expressions. Erlang also supports user given function specifications (or just specs), that are contracts
providing more information about the semantics of functions. Function specs are useful not only as documentation, but also can be employed by Dialyzer to improve the precision of the analysis. Even though specs can have a polymorphic shape, in practice Dialyzer is not able to exploit all their potential. One reason for that is that extending the notion of success type to a polymorphic setting is not trivial, and several interpretations are possible. In this work [1] we propose a precise formulation for a novel interpretation of function specs as polymorphic success types, and a program transformation that allows us to apply this new interpretation on the call sites of functions with a declared spec. This results on a significant improvement in the number of definite errors that Dialyzer is able to detect.

Autores: Francisco Javier López-Fraguas, / Manuel Montenegro / Juan Rodríguez-Hortalá / 
Palabras Clave: