Revamping the numeric classes

[Tom Pledger]

Marcin 'Qrczak' Kowalczyk writes:
 | Fri, 9 Feb 2001 17:29:09 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
 | 
 | >     (x + y) + z
 | > 
 | > we know from the explicit type signature (in your question that I was
 | > responding to) that x,y::Int and z::Double.  Type inference does not
 | > need to treat x or y up, because it can take the first (+) to be Int
 | > addition.  However, it must treat the result (x + y) up to the most
 | > specific supertype which can be added to a Double.
 | 
 | Approach it differently. z is Double, (x+y) is added to it, so
 | (x+y) must have type Double.

That's a restriction I'd like to avoid.  Instead: ...so the most
specific common supertype of Double and (x+y)'s type must support
addition.

 | This means that x and y must have type Double.  This is OK, because
 | they are Ints now, which can be converted to Double.
 | 
 | Why is your approach better than mine?

It used a definition of (+) which was a closer fit for the types of x
and y.

 :
 | > h:: (Subtype a b, Subtype Int b, Eq b) => (Int -> a) -> Bool
 | 
 | This type is ambiguous: the type variable b is needed in the
 | context but not present in the type itself, so it can never be
 | determined from the usage of h.

Yes, I rashly glossed over the importance of having well-defined most
specific common supertype (MSCS) and least specific common subtype
(LSCS) operators in a subtype lattice.  Here's a more respectable
version:

    h :: Eq (MSCS a Int) => (Int -> a) -> Bool

 | > That can be inferred by following the structure of the term.
 | > Function terms do seem prone to an accumulation of deferred
 | > subtype constraints.
 | 
 | When function application generates a constraint, the language gets
 | ambiguous as hell. Applications are found everywhere through the
 | program! Very often the type of the argument or result of an
 | internal application does not appear in the type of the whole
 | function being defined, which makes it ambiguous.
 | 
 | Not to mention that there would be *LOTS* of these constraints.
 | Application is used everywhere. It's important to have its typing
 | rule simple and cheap. Generating a constraint for every
 | application is not an option.

These constraints tend to get discharged whenever the result of an
application is not another function.  The hellish ambiguities can be
substantially tamed by insisting on a properly constructed subtype
lattice.

Anyway, since neither of us is about to have a change of mind, and
nobody else is showing an interest in this branch of the discussion,
it appears that the most constructive thing for me to do is return to
try-to-keep-quiet-about-subtyping-until-I've-done-it-in-THIH mode.

Regards,
Tom