Oops, I forgot to reply to part of your email. On Mon, Jul 21, 2014 at 12:07 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Sun, Jul 20, 2014 at 11:43 PM, Matt Oliveri <[email protected]> wrote: >> >> So what you're saying is that given complete typings, the complete >> types are unique? > > This is axiomatically true. Suppose the complete types were not unique. Then > there must be two types, each maximally inclusive (because it's complete). > But if neither includes the other, neither can be maximally inclusive.
Yes, other than a gripe about "maximal" versus "maximum" (maximal elements don't generally have to be unique). I'm glad we agree that's obvious. But that means I still don't know what you meant by complete typing implies unique typing. > You can arrive at situations where you get two complete types. In effect, > you have two [possibly local] maxima in the type search space. But HM-style > typing requires that you get one type for each expression. So in other words, the HM approach demands that every well-typed expression have a unique maximally-inclusive type, called the complete type. And by maximally-inclusive, we essentially mean most informative, right? But more informative types have fewer elements, so "inclusive" seems misleading. If not, can you give a simple example of one type being more "inclusive" than another? >> This is not to say types are unique, just that all >> the other types an expression has are not complete. > > I think you're looking at this incorrectly. If you have a situation where > there is a choice between a more inclusive and a less inclusive type, and > the type rules are otherwise satisfied, then you necessarily have a > subtyping relationship (of sorts) and it is not possible to arrive at a > unique typing. The only question at that point is whether you want the > maximally inclusive type. That was precisely my original point. Complete types are only interesting when you do _not_ have unique typing. Hence my confusion with you saying complete typing implies unique typing. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
