Marcin Kowalczyk:
Me:
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 function.
Int -> [a] -> Int, since this is the type it will get in the original type system. 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