Type Inference for First-Class Messages with Feature Constraints

Author: Martin Müller and Susumu Nishimura

Editor: Jieh Hsiang and Atsushi Ohori

We present a constraint system OF of feature trees that is appropriate to specify and implement type inference for first-class messages. OF extends traditional systems of feature constraints by a selection constraint ``by first-class feature tree'' $x \langle y \rangle z$, in contrast to the standard selection constraint $x[f]y$ ``by fixed feature'' $f$. We investigate the satisfiability problem of OF and show that it can be solved in polynomial time, and even in quadratic time in an important special case. We compare OF with Treinen's constraint system EF of feature constraints with first-class features, which has an NP-complete satisfiability problem. This comparison yields that the satisfiability problem for OF with negation is NP-hard. Based on OF we give a simple account of type inference for first-class messages in the spirit of Nishimura's recent proposal, and show that it has polynomial time complexity: We also highlight an immediate extension that is desirable but makes type inference NP-hard.