[Haskell] Typing in haskell and mathematics

[Jacques Carette]

The previous post on record syntax reminded me of some 'problems' I had noticed where Haskell and mathematics have a 
(deep) usage mismatch.

First, consider a syntax for other component-wise function application?  For example, it would be convenient to have 
(f,g) @ (x,y)
be (f x, g y).  In some languages [with dynamic typing], one can even do (f,g) (x,y) :-)  

Yes, I am aware that this untypeable in Haskell, because polymorphism is straight-jacketed by structural rules.  But 
in mathematics, it is convenient and extremely common to:
1) look at the type a -> b as being a *subtype* of b (though I have never seen it phrased that way in print)
2) to consider every 'natural transformation' available and use it (tuples of functions <-> obvious function on 
tuples)

Seeing a -> b as a subtype of b allows one to take any function f : b -> b -> c (like + ) and 'lift' it to 
ff : (a -> b) -> (a -> b) -> (a -> c)
via the obvious definition
ff g h = \x -> f (g x) (h x)
This is done routinely in mathematics.  The meaning of the expression (sin + cos) should be immediately obvious.  Such 
'lifting' is used even in first-year calculus courses, but not in Haskell.

The "same" phenomenon is what allows one to 'see' that there is an obvious function
apply_tuple:: (a->b,c->d) -> (a,c) -> (b,d)
so that
(f,g) (a,b)
only has one possible meaning, if the built-in apply function were to be overloaded.

Similarly, there are "obvious" maps
apply_T :: T (a->b) -> a -> T b
for any datatype constructor T (as has been noticed by all who do 'generic' programming).  This means that
[f, g, h] x == [f x, g x, h x]
but also (in mathematics at least)
{f, g, h} x == {f x, g x, h x}
where {} denotes a set, and the equality above is extensional equality, and so on.

Note that some computer algebra systems use #1 and #2 above all the time to define the operational meaning of a lot of 
syntactic constructs [where I personally extended the use of such rules in the implementation & operational semantics 
of Maple].  What hope is there to be able to do something 'similar' in a Haskell-like language?

Jacques