Revamping the numeric classes
Mon, 12 Feb 2001 00:02:00 +0100 (MET)
>> No, the transformation is a single step procedure where a term
>> is transformed into a typeable term (if possible) with a minimal
>> amount of lifting. You don't compose transformations.
>So functions implicitly lifted can't be used in the same ways as
>functions originally defined as lifted (namely, they can't be lifted
>again)... This is bad.
Functions themselves are never lifted. They just appear to be lifted when
applied to arguments of certain types, and then the function application is
always statically resolved into an expression where the function has its
>> Due to the principle of minimal lifting (which implies already
>> well-typed terms should not be transformed) a call to a polymorphic
>> function should not be transformed unless there is a dependence
>> between the type variable(s) of the function and of the argument(s)
>> in the application.
> f x y = (x, x + y)
> Num a => a -> a -> (a, a)
>and thus it cannot be used on the type
> Int -> [Int] -> (Int, [Int])
>even though if its body was inlined into an expression requiring that
>type, it could (by lifting x+y to map (x+) y)?
Your function has its polymorphism constrained to the Num class. So we could
allow elemental overloading (on the uncurried form of f) as long as [Int] is
not an instance of Num.
Yes, if [Int] is made an instance of Num then the meaning of calls to f on
lists will change from the elemental meaning to the meaning defined through
the instance declarations for [Int]. This can surely be a problem in some
cases. But this is not a property of the elemental overloading mechanism per
se, but rather that we would have two different overloading mechanisms in
the language powerful enough to specify conflicting overloading.
BTW, the type signature for your "lifted f" (if it existed) should be
(Int,[Int]) -> [(Int, Int)]. See second example below.
>You can't lift arbitrary function of type Int -> Int -> (Int, Int)
>into Int -> [Int] -> (Int, [Int]) without knowing its defintion.
>Try it with g x y = (y, x).
Consider uncurried g: g (x,y) = (y,x) and assume it has an explicit type
declaration to (Int,Int) -> (Int, Int) (so it's not polymorphic).
if x :: Int and l :: [Int], then
g (x,l) -> zipWith (g.(,)) (repeat x) l :: [(Int,Int)].
The rewrite of the overloaded application is guided only by type
information. (Again note only the application of g is rewritten, neither g
itself nor its type does change.)
>Suppose there is a function
> fancyPrint :: Printable a => [a] -> IO ()
>which applies some fancy printing rules to a list of printable values.
>A programmer knows that this function can be used on lists as well
>as on single elements, because those elements will be promoted to
>single-element lists as necessary. So far so good.
The rules I have sketched so far only promote a value in connection with
elemental overloading. A good example is g (x,l) above. Here, g is
elementwise applied to l and in the process x becomes promoted into
(repeat x), similar to the original scaling example a*x where a is a scalar
and x a matrix. So with these rules alone fancyPrint 17 would not be
rewritten into fancyPrint (repeat 17). But the rules can of course be
extended to cover this case.
>Then he applies it to a single String. Guess what? It is not
>promoted to a single-element list, but each character is printed
Which is the original meaning of fancyPrint applied to a string. Why "oops"?
A programmer must be aware of the meaning of function he writes. fancyPrint
will always be a function over lists, no matter whether its use is
overloaded on arguments of other types or not.
>> >It's not enough, because the least lifted type is not the most general
>> >answer. Answers for different amounts of liftedness are incompatible
>> >with that answer - they are not its instances as in the HM typing.
>> It does not matter that they are not instances.
>It does. It's not enough to check that there exists a set of places
>to insert map or zipWith which transforms what is written to what I
>need. Because there can be a different, incompatible set of places,
>which is considered "better" by the compiler and my set is not
>obtainable from what the compiled has done. See the first example
(I think your example was broken, but in principle you're right.) Of course,
the use of the overloading I have described (and any kind of overloading) is
justified only if the overloading matches the intuition of the programmer.
If it misleads you then it is harmful. Regarding elemental overloading, my
experience is that data parallel programmers quickly develop a strong
intuition for it. What I have seen through examples is that elemental
overloading using the rules I have sketched and the "minimal lifting"
principle always seems to produce the intuitively correct meaning, also in a
language like Haskell. If the produced result is the "right" one, then the
fact that other possible transformations produce terms with incompatible
types is not a concern. I can give no stronger justification than that.