[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I think you need to be more precise about the typing of assignment and method calls. Assuming that A.DoHousePetThing() requires A to have trait HousePet to be well-typed, Mammal cannot be the principal type of A because it is not a valid type for A (A.DoHousePetThing() is not well-typed if we only have (A : Mammal)). Conversely, (Mammal + Housepet) does not seem to be a valid type for A, because intuitively (A = C) would not be well-typed. In usual type system, there is a strong relation between what you call "types of a term" and "required types for a time": if a type T is required (imposed by a usage context) for a term A, then any "type for A" should be instantiable into T, otherwise the whole program is not well-typed. In particular, the principal type should be instantiable into any "required type": the two notions you distinguish are equivalent. (I suspect you've got the order reversed when you say "a type for a term such that it is an instance of all types required of this term", my understanding is that you rather talk about "a type which is *instantiable* into all types required for this term". These ordering questions are always tricky, but I think both required types HousePet and Mammal are instances of your candidate HousePet+Mammal, not the other way around.) On Thu, Mar 5, 2015 at 2:50 AM, Sean McDirmid <smcd...@microsoft.com> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hi, > > A principal type is defined in wiki as "a type for a term such that all > other types for this term are an instance of it." What about a type defined > as "a type for a term such that it is an instance of all types required of > this term?" Whereas a principal type seems to be an intersection over > bindings, such a "usage" type is a union over uses. Please forgive this OO > example, but it is the best I could think of to exemplify the difference in > my head: > > trait HousePet > def DoHousePetThing() > trait Mammal: > def DoMammalThing() > trait Dog : Mammal > trait Cat : Mammal > > val B : Dog > val C : Cat > A = B > A = C > // the principal type of A is Mammal > A.DoHousePetThing() > A.DoMammalThing() > // the usage type of A is HousePet + Mammal > > The principal type of A is the intersection of Dog and Cat (say Mammal). > The X type I'm computing in my system is based on usage, so it is just > "HousePet" + "Mammal." So while a principle type starts at top and becomes > more specific with each bind (top -> Dog -> Mammal), a usage type starts at > bottom and becomes more general with each use (bottom -> HousePet -> > HousePet + Mammal). > > Could this "usage" type be the opposite of a principal type, and if so, > what has it been called in the literature? Or maybe I'm just looking at > this all wrong: would such the usage type "HousePet + Mammal" still be a > principle type if it was propagated backwards during type inference to > bindings so that B is "Dog + HousePet" and C is "Cat + HousePet?" > > Thanks, > > Sean >
