## A question about subtypes inference

Hi

I am looking for information on subtype inference.

Consider a type system with a sub rule:

E,C|- e:sigma C|-sigma :sigma'
----------------------------------------
E,C|- e:sigma'

Here E is the type environment and C is the (initially empty) subtype constraint set.
And I use : to denote the smaller than relation on types for lack of a better symbol.

And a set of rules for infering constrainst from sigma:sigma' depending on the underlying type of sigma. (it is a structural type system).

My question is, after my type inference assigns type sigmaâ€™ to e, how do I choose sigmaâ€™, as to find the correct underlying constraints.

I looked and asked around. Some suggested using a copy of sigma, I find this odd because I donâ€™t see why, and how this would produce the needed type constraints.

I would be grateful for either a article explaining this matter or pointers to the underlying idea.

R.K.

BTW this is the article Iâ€™m working on
http://citeseer.ist.psu.edu/cache/papers/cs/18011/http:zSzzSzresearch.microsoft.comzSz~mafzSzpopl01.pdf/rehof01typebased.pdf

## Comment viewing options

### look at F sub

I'd suggest reading the papers on F sub as a start, and possibly the papers that cite those in turn. I do believe you can find some on Benjamin Pierce's webpage.

### What is sigma'

The papaers on Pierce's webpage are interesting, but I still can't find the solution to my problem. It is driving me mad because I feel It is something rather simple that I overlook and obsess about.

My question is simply, given a expression e of type sigma', and a subtype rule as defined above, what is the value of sigma ? Since it does not apear in the conclusion, I cannot do inference, unless I try to guess a possible value to sigma try to see if it is a subtype to sigma under to subtype relation.

I've looked and looked for info on this, as I cannot beilive that I am the first to worry about it. In some places I have found indications that sigma prime would be a copy of sigma, but then I cannot see how any subtyping can be done since the types are essentialy the same.

### Sigma' is any supertype of si

Sigma' is any supertype of sigma. The rule says that if e has the type sigma and sigma's a subtype of sigma' then e also has the (less specific) type sigma'.

You aren't intended to start with sigma' and go looking for a sigma - the rule throws away information, so it's not particularly useful applying it backwards.

### No unique candidate

Your sigma can be any subtype of sigma'. Hence you cannot use this rule to "simplify" your sigma' during inference. The canonical constraint you have to infer is sigma<sigma' - and you cannot do any better without losing completeness.

In fact, that's precisely the reason why subtyping inference is not very practical in general: instead of equality constraints you have to deal with inequalities. You have to collect a large set of such inequality constraints, and you can almost never simplify any type occuring in them.