Thu, 8 Feb 2001 13:39:51 +0100 (MET), Bjorn Lisper <lisper@it.kth.se> pisze:
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. 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.
Here (3) is "full" elementwise application, and (1) and (2) are "partial" elementwise applications where the unlifted argument can be seen as promoted.
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. 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. Generally the concept of treating a single element as a list (promoting it when necessary) is ambiguous in its nature and it should not be used in any general purpose language. It might work in a poor language which operates only on numbers, vectors and matrices, but not in Haskell in which lists are perfectly first class objects, and similarly functions, and whose type system is polymorphic, so operations can be applied to values which are lists or not, functions or not, not statically known.
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. There is no most general answer, so these rules are ambiguous and cannot be designed well. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK