Weak subsumption Constraints for Type Diagnosis: An Incremental Algorithm
<|reference_start|>Weak subsumption Constraints for Type Diagnosis: An Incremental Algorithm: We introduce constraints necessary for type checking a higher-order concurrent constraint language, and solve them with an incremental algorithm. Our constraint system extends rational unification by constraints x$\subseteq$ y saying that ``$x$ has at least the structure of $y$'', modelled by a weak instance relation between trees. This notion of instance has been carefully chosen to be weaker than the usual one which renders semi-unification undecidable. Semi-unification has more than once served to link unification problems arising from type inference and those considered in computational linguistics. Just as polymorphic recursion corresponds to subsumption through the semi-unification problem, our type constraint problem corresponds to weak subsumption of feature graphs in linguistics. The decidability problem for \WhatsIt for feature graphs has been settled by D\"orre~\cite{Doerre:WeakSubsumption:94}. \nocite{RuppRosnerJohnson:94} In contrast to D\"orre's, our algorithm is fully incremental and does not refer to finite state automata. Our algorithm also is a lot more flexible. It allows a number of extensions (records, sorts, disjunctive types, type declarations, and others) which make it suitable for type inference of a full-fledged programming language.<|reference_end|>
@article{mueller1995weak,
    title={Weak subsumption Constraints for Type Diagnosis: An Incremental
  Algorithm},
    author={Martin Mueller, Joachim Niehren (German Research Center for Artificial
  Intelligence (DFKI), Saarbr"ucken, mmueller)},
    journal={arXiv preprint arXiv:cmp-lg/9506002},
    year={1995},
    archivePrefix={arXiv},
    eprint={cmp-lg/9506002},
    primaryClass={cmp-lg cs.CL}
}