On the complexity of type inference with coercion

Publisher Website
Google Scholar
Abstract
We consider the following problem: Given a partial order (C, 2) of base types and coercions between them, a set of constants with types generated from C, and a term M in the lambda calculus with these constants, does M have a typing with this set of types? This problem abstracts the problem of typability over a fixed set of base types and coercions (e.g. int < real, or a fixed set of coercions between opaque data types). We show that in general, the problem of typability r of lambda-terms over a given partially-ordered set of base types is NP-complete. However, if the partial order is known to be a tree, then the satisfiability problem is solvable in (low-order) polynomial time. The latter result is of practical importance, aa trees correspond to the coercion structure of single-inheritance object systems.

This publication has 0 references indexed in Scilit: