[Haskell] Typing in haskell and mathematics
Jacques Carette
carette at mcmaster.ca
Fri Jan 28 10:01:33 EST 2005
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
More information about the Haskell
mailing list