A liberal type system for functional logic programs

摘要

We propose a new type system for functional logic programming which is more liberal thanrnthe classical Damas–Milner usually adopted, but it is also restrictive enough to ensure typernsoundness. Starting from Damas–Milner typing of expressions, we propose a new notion ofrnwell-typed program that adds support for type-indexed functions, a particular form ofrnexistential types, opaque higher-order patterns and generic functions – as shown by anrnextensive collection of examples that illustrate the possibilities of our proposal. In thernnegative side, the types of functions must be declared, and therefore types are checked butrnnot inferred. Another consequence is that parametricity is lost, although the impact of thisrnflaw is limited as ‘free theorems’ were already compromised in functional logic programmingrnbecause of non-determinism.