Type constraint solving for parametric and ad-hoc polymorphism
Bart Demoen, María García de la Banda, Peter J. Stuckey · Lirias · 1999
. Unification has long been used as a mechanism for type checking and type inference for Hindley-Milner types in functional programming. The programmer defines the possible types, and the compiler uses unification to check and infer types for function definitions. In constraint logic programming it is natural to extend the functional programming case by allowing overloading of predicate and function definitions, that is, ad-hoc polymorphism. Mycroft and O'Keefe showed how to check predicate type declarations under these assumptions. In this paper, we show how to infer predicate types, by translating a constraint logic program with given types into a logic program over types. The program can then be used to check and infer the possible types for the predicates and variables appearing in the original program. Since executing the translated program can be inefficient when there are highly disjunctive type definitions, we use methods of propagation based constraint solving and memoing to ...