Transparent Function Types: Clearing up Opacity

摘要

Functional logic programming (FLP) is a paradigm that comes from the integration of lazy functional programming and logic programming. Although most FLP systems use static typing by means of a direct adaptation of Damas-Milner type system, it is well-known that some FLP features like higher-order patterns or the equality operator lead to so-called opacity situations that are not properly handled by Damas-Milner type system, thus leading to the loss of type preservation. Previous works have addressed this problem either directly forbidding those HO patterns that are opaque or restricting its use. In this paper we propose a new approach that is based on eliminating the unintended opacity created by HO patterns and the equality operator by extending the expressiveness of the type language with decorations in the arrows of the functional types. We study diverse possibilities, which differ in the amount of information included in the decorations. The obtained type systems have different properties and expressiveness, but each of them recovers type preservation from simple extensions of Damas-Milner.