I see. So you can transform arbitrary function of type a->b->c to a function of type [a]->b->[c], by applying \f x y -> map (\z -> f z y) x and similarly a->b->c to a->[b]->[c]. But then there are two ways of transforming a->b->c to [a]->[b]->[[c]
There should be no transformation to type [a]->[b]->[[c]] in this case.
Wait wait wait. You told that a->b->c is convertible to [a]->b->[c] for *any* a,b,c. Now I have x = [a], y = b, z = [c] and use the transformation x->y->z to x->[y]->[z] and obtain [a]->[b]->[[c]].
Both steps are legal, so their composition must be legal, or I don't like this Haskell-like language anymore.
(You never seem to have liked it much ... :-) 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. Let us write [a]^n for the type of n-deep lists of lists of a. If f :: a -> b -> c, x :: [a]^m, and y :: [b]^n, then f x y is transformed into a term with type [c]^max(m,n). This is the minimal lifting necessary to obtain the correct elementwise application of f. If m < n then promotion will take place on the first argument, if m > n on the second, and if m = n then there will be an elementwise application without promotion.
Unless you say that a->b->c is convertible to a->[b]->[c] *except* when a is a list. Then it's bad again. There should be no negative conditions in the type system! Moreover, in a polymorphic function you don't know yet if a will be a list or not.
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. Such dependencies could possibly occur in recursive calls in function definitions. Consider, for instance the (somewhat meaningless) definition f x y = head (f [x,x] y) During type inference, f will first be assigned the type a -> b -> c. In the recursive call, f will be called on arguments with types [a] and b. This causes a lifting to occur, where f is elementwise applied to [x,x] with promotion of y. The transformed definition becomes f x y = head (zipWith f [x,x] (repeat y)) On the other hand, if f somewhere else is applied to some other arguments, with types not containing a, then no transformation of that call will occur.
There are no full and partial applications because of currying. It's impossible to say when you should consider a function as a multiparameter function. There are only single-argument functions. So you would have to say that some rule apply only *unless* the result has a function type, which does not work again.
Touché! To keep the discussion simple I have kept multiparameter functions curried, but you nailed me. Yes, there will be ambiguities if you allow overloading on other than the first argument in a curried definition (since there really is only one argument). So for a function f :: a -> b -> c we should only allow elementwise overloadings corresponding to functions of types [a]^n -> [b -> c]^n. Elementwise overloading on multiparameter functions must appear only on their uncurried forms, so only if f :: (a,b) -> c then we can allow transformations of calls corresponding to type signature ([a]^m,[b]^n) -> [c]^max(m,n). (This would give problems with elementwise overloading of arithmetic operators in Haskell, since these are curried. But, as I said earlier, I'm not proposing to actually extend Haskell with this overloading, I'm only discussing the concept as such in the Haskell context.)
With your rules a programmer writes code which is meant to implicitly convert a value to a single-element list, because something tries to iterate over it like on a list. Unfortunately the element happens to be a string, and he gets iteration over its characters. And if it works the other way, another programmer meant iteration over characters and got iteration over a single string. You can't tell which was meant.
I don't think there will be any ambiguities here. The overloading is resolved statically, at compile-time, for each call to the function. Calls to polymorphic functions are not transformed (except for cases like I showed above).
Of course the type/term transformation system must have the property that if different transformations can yield the "best" type (wrt liftedness), then the transformed expressions should be semantically equivalent.
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. Each call is transformed statically, separately. The liftedness ordering is used only to direct the resolution of the overloading, so we pick the minimal lifting (the others are not interesting). The overloaded function itself will have the same type everywhere. Björn Lisper