Thu, 8 Feb 2001 00:32:18 +0100 (MET), Bjorn Lisper <lisper@it.kth.se> pisze:
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.
But other are its instances! The point of HM is that I can forget that something is more general and treat a definition f xs = [] : xs as of type [[Int]] -> [[Int]]. Once I determine a possible meaning of a code, I know it's correct, no matter if it's the most general meaning or not. (Well, this is not exactly true when classes come. Two uses of f don't unify types of their arguments to the same type, where they would do that if f had type [[Int]] -> [[Int]]. Fortunately it's very rarely a problem I would say. Overloading should not be abused because it easily leads to ambiguous types.)
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.
So I can't apply f to lists, but I could if I inline its body. This means that I cannot arbitrarily refactor a piece of code by moving parts of it into separate definitions: subexpressions are given some extra meanings only if they are physically placed in certain contexts. This is bad.
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.
Argh, Haskell's type system is complex enough. This is going to be horror for people trying to understand it. I'm not saying that we should not think about extending the type system at all, but this is IMHO too ugly.
(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.)
Here other types are not instances of the principal type! So it's not principal: it's just an arbitrary ordering.
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.
Ah, so what uses of f are correct depends on its definition, not type! Sorry, this is way to radical. Types exist to formalize possible ways a value can be used. HM allows to determine most general types variables in a let-block (or: of a module) before their uses, so separate compilation is possible. In your system typechecking of a function's definition is done each time it is used! -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK