David J Lillie, Peter G. Harrison
We present an intuitive model of polymorphic recursive types and subtypes based on a metric space of projections. We show this model to be semantically equivalent to types as strong ideals although requiring less structure in the semantic framework and allowing a more concise analysis. We present a new set of type inference rules for a combinatorial language and prove the rules correct with respect to our model. An algorithm embodying these rules has been implemented.
Information from pubs.doc.ic.ac.uk/projection-model-types.