Re: [TYPES] Basic principal type terminology

[ 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 <[email protected]> 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
>