How to type this function?

Nick Kallen phantom@earthlink.net
Thu, 16 Apr 1998 20:56:07 -0700


Suppose you have some function f : a -> a -> a -> ... -> a. And you want to
apply a list l as arguments to the function, as in:

apply f [a, b, c, ..., z] = f a b c ... z

I tried the following function, but for somewhat obvious reasons, it wont
type check.

apply f [p:ps] = apply (f p) ps
apply f [] = f

OK, first-off, I know this is nearly identical to Marco Pil's addArgument's
in his November 1997 email to this list containing module OpSys. The thing
is, I don't think dynamics are necessary to do this function; atleast they
shouldn't be. Perhaps I'm making an error, but I think you can infer a type
from this (namely that specified above).
    Perhaps a solution to this is to come up with some notation indicating a
product space. If we use cartesian product notation to symbolized a regular
curried function: f : a * a * a * a * ... * a. This is often symbolized in
textbooks as just a* (where the * should look like an exponent). Thus f :
a*. Some sort of notation to express this would be very useful in Clean, I
think, because it allows functions like the above. There are other
situations where it'd be useful too. Consider a formal definition of a
bitmap operation <*>:

:: B = bitmap definition....

<*> : B* -> B

That is, a bitmap operation <*> is a function mapping an arbitrary number of
bitmaps to another bitmap. Consider:

Zero : -> B
Complement : B -> B
Insert : B B -> B

I also want to generalize this to the case where f : a1  -> a2 -> a3 ->
... -> an. (This is what Mr. Pil's dynamic function does.) A simple product
space wouldn't work here, but it seems that the representation is a trivial
extention of product spaces. Perhaps a similar notation to product spaces
could be employed.
    Another thing: even if I could express f : a1 -> ... -> an, the list
would now not be typable. Even if I used existential types for the list,
there would be no way to get at the elements because their type information
is unknown. *Sigh.* At this point, I must concede that Dynamics are the only
concievable situation.
(    And speaking of existentials, can Clean get rid of the "E.a:" construct
and just use the "all free variables in an algebraic type definition are
existentially quantified" method?)