Revamping the numeric classes

Bjorn Lisper
Thu, 8 Feb 2001 00:32:18 +0100 (MET)

Marcin Kowalczyk:
>> A natural principle to adopt is that an already typeable expression should
>> not be transformed. This will for instance resolve the ambiguity in the list
>> of list example: if l :: [[a]] then length l is already well-typed and
>> should not be transformed into map length l.

>So there are ways to interpret an expression which are not chosen
>only because some other way is a better match? This is very dangerous
>in principle.

>Two interpretations of a code are "correct", but one is "more correct"
>than the other.

It is quite similar in spirit to the concept of principal type in
Hindley-Milner type systems. An expression can have many types but only one
"best" (most general) type in that system.

>Also, what is the inferred type of, for example
>    f x y = x + length y
>? It can be
>    Int -> [a] -> Int
>    [Int] -> [a] -> [Int]
>and neither is more general than the other. And this is a simple

Int -> [a] -> Int, since this is the type it will get in the original type

The types you mention are incomparable w.r.t. the usual "more
general"-ordering on types, but one could consider also other orderings. For
the types you give, the second is more "lifted" than the first in that it
contains [Int] in places where the first type has Int. One can define a
"liftedness" order on types in this vein.

(OK, so one would need to go through the formalities and prove that there
are "principal types" w.r.t. this relation between types, and that this new
principal type concept is not in conflict with the old one. I cannot say for
sure that it works.)

I should be more specific about what a type system could look like that
implements this kind of overloading. It could be a coercive type system,
with judgements of the form

t -> t':a

where t, t' are terms, a is a type, and t:a is a correct judgement in the
original type system. So the type system not only gives a type but also a
transformation that resolves the overloading into a well-typed term.

>> >Again, Haskell does not have subtyping. It is not compatible with type
>> >inference - it can only work in poor languages which require an operation
>> >to be fully applied where it is used, and either don't have static types
>> >or require them to be specified explicitly.
>> I am not so sure about this. Could you exemplify?

>Sorry, I don't have a concrete example in mind. How to infer types when
>implicit conversions are possible anywhere? The above function f can
>be applied even to two numbers (because the second would be promoted
>to a list of length = 1), so what is its inferred most general type?

Int -> [a] -> Int. If f is applied to some arguments with other types for
which the overloading is defined, say f l1 l2 where l1 :: [Int] and
l2 :: [a], then the term f l1 l2 would be transformed into a well-typed term
but the type of f itself would not change.

>Again, arbitrarily choosing one of the alternatives basing on some
>set of weighting rules is dangerous, because a programmer might mean
>the other alternative - there is no simple way to ensure that the
>compiler interprets it in the same way as I wanted. It's not enough
>to check that all types match modulo conversions - I must carefully
>check that no "better" interpretation is possible.

I surely agree that this kind of overloading should be used only when it is
in accordance with the intuition of the programmer. This could, for
instance, imply restrictions to certain types or operators.

Björn Lisper