Re: Overloaded unification

On Jan 28, 11:29 pm, "David B. Benson" <dben...@[EMAIL PROTECTED]
> wrote:
>
> Nor will my approach destroy principle typing, I believe.
> In detail, each overloaded symbol is unified (in all
> possible ways) via a non-overloaded instantiation.  This
> results in, for one overloaded symbol with two possible
> 'meanings', 2^k different typings for k occurances of the
> symbol. [This is what I meant by exponential time, by the
> way.]  This results in 0, 1 or more correct typings: if none
> re****t error, if one fine, if more than one I have yet to
> decide what ought to be done.

Well, what you wrote is basically the long version of "there are no
principal types". ;-) A principal type is a *single* most general
type, not a set of type (unless you have intersection types, which
induce their own class of problems). The existence of principal types
implies a number of good properties that make type inference well-
behaved and tractable. It also makes error messages much more
pleasant.

Aside: note also that there is a difference between principal types
(the existence of a most general type given an expression and a fixed
environment) and principal typings (the existence of a most general
type and environment given just an expression). I don't think the
latter can possibly exist in the presence of overloading.

- Andreas