[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Mar 5, 2015, at 02:50 , Sean McDirmid <[email protected]> wrote: > > 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: Sounds to me like you are looking for principal typings, not principal types. /Andreas > > 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
