A liberal type system for functional logic programs†. (May 2015)

• Record Type: Journal Article
• Authors: LÓPEZ-FRAGUAS, FRANCISCO JAVIER; MARTIN-MARTIN, ENRIQUE; RODRÍGUEZ-HORTALÁ, JUAN
• Is Part Of: Mathematical structures in computer science. Volume 25:Number 4(2015)
• Page Start: 942
• Page End: 977
• Publication Date: 2015-05
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129513000091
• Languages: English
• ISSNs: 0960-1295

Abstract

<abstract abstract-type="normal"> <title> <x content-type="archive" xml:space="preserve">Abstract</x> </title> <p>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, a particular form of 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.</p> </abstract>