Type inference with subtypes

摘要: We extend polymorphic type inference to include subtypes. This paper describes the following results: •We prove existence of (i) principal property and (ii) syntactic completeness checker, for with result is developed only minimal assumptions on underlying theory subtypes. •For a particular “structured” subtypes, those engendered by coercions between constants only, we that types are compactly expressible. suggests practical checker structured subtypes feasible. •We develop efficient algorithms such checker. There two main algorithms: MATCH CONSISTENT. The first can be thought as an extension unification algorithm. second, which has no analogue in conventional inference, determines whether set consistent.