Marcin Kowalczyk:
Me: 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 original type.
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.
Does f x y = (x, x + y) has type 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 separately. Oops!
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 above.
(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. Björn Lisper