Revamping the numeric classes

[Marcin 'Qrczak' Kowalczyk]

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