[TYPES] Basic principal type terminology

[Sean McDirmid]

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