Revamping the numeric classes

[Bjorn Lisper]

>> >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