Home » forums » LtU Forum

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

By kilrati at 2005-07-29 16:52 | LtU Forum | previous forum topic | next forum topic | other blogs | 6076 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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.

By carter at Fri, 2005-07-29 17:27 | login or register to post comments

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.

By kilrati at Wed, 2005-08-10 17:32 | login or register to post comments

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.

By Philippa Cowderoy at Wed, 2005-08-10 17:36 | login or register to post comments

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.

[Your paper link seems to be screwed.]

By Andreas Rossberg at Wed, 2005-08-10 17:51 | login or register to post comments

Ok I see, But if I'm doin

Ok I see,

But if I'm doing type inference in order to capture the constrainsts that occur in a given espression, then I have to use the values of sigma and sigma' to generate the antecedant (constraint).

But when I type an expression I have only one type for it. say e:sigma how do I use the rule? The constraint is what I want to infer.

By kilrati at Wed, 2005-08-10 17:53 | login or register to post comments

The only actual constraint at

The only actual constraint at that point is that e:sigma, and that comes from the environment. You need to see e being used for stuff to infer further constraints (eg that it's valid to apply a given function to it and everything that implies)

By Philippa Cowderoy at Wed, 2005-08-10 18:51 | login or register to post comments