[Haskell-cafe] Re: [Haskell] Typing in haskell and mathematics

[Iavor Diatchki]

Hello,

On Fri, 28 Jan 2005 10:01:33 -0500, Jacques Carette <carette at mcmaster.ca> wrote:
> The previous post on record syntax reminded me of some 'problems' I had noticed where Haskell and mathematics have a
> (deep) usage mismatch.
It is interesting that my sentiment is exactly the opposite.
Mathematicians (the applied kind, not the pure) tend to be quite
sloppy about their notation relaying _a lot_ on the context and the
fact that people know what they are talking about.   I find that this
makes their explanations harder to  understand rather than easier.

> 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) :-)
I am not sure what you mean, but you can define exactly that (except
for the @ sign which is special syntax already):
(f,g) `ap2` (x,y) = (f x, g y)

> Yes, I am aware that this untypeable in Haskell, because polymorphism is straight-jacketed by structural rules. 
What do you mean by this:
ap2 :: (a -> b, c - d) -> (a,c) -> (b,d)

 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)
I don't think subtyping is what you are thinking of.  Perhaps you are referring
to the correspondance between b-expressions with a free a-variable,
and functions a->b.   In Haskell we don't have expressions with free
variables as
first class values.  There might be some interesting things to work
out for such beasts.

> 2) to consider every 'natural transformation' available and use it (tuples of functions <-> obvious function on
> tuples)
Are you suggesting that natural transformations should be applied automatically?
There are many problems with this:  which operations should happen
automatically?
Type inference (if it works at all) will be hard to do, but perhaps
these are technical details.
Fundamentally the "sloppy" math notation assumes that what the author
wrote is correct and should simply be given "the obvious" meaning. 
This is pretty much the idea with dynamic typing.  I find the
restrictions of static typing very convenient (well most of the time
:-) as they capture "stupid' errors.

> 
> 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.
Apart from the fact that this does not seem like a good idea,
you can already do things like this in Haskell:
liftOp op f g x = f x `op` f x
This is all you need, especially if you are prepared to stick to the
"usual" mathematical convention of not using curried functions, but
instead using tuples to pass multiple arguments.

> 
> 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.
There are many interesting things one could do if application was to
be overloaded
but this hardly seems like a motivating example.  You can already use
the 'ap2' combinator from above.  I can see that it is annoying to
have ap2, ap3, etc.
You can define a generic "ap_n" using dependent types, or using the
encoding tomasz posted, but that hardly seems to be a "deep" problem.

> 
> 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).  
Is this really true? Consider:
data T a = T (a -> Int)
What shoud apply_T do?
applyT :: (essentially) ((a -> b) -> Int) -> a -> (b -> Int)
perhaps: applyT (T f) a = T (\b -> f (const b))
but that probably does not behave as you would like it.
Of course you could restrict the datatypes for which apply_T can be derived.

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.
I agree that it would be nice to automatically derive functions such
as apply_T, etc.
This (as you point out) is the idea of generic programming.  
This however does not suggest that we should replace application...

> 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?
I think it is already possible to do simillar things.  
I am sure there is room for improvement, but it is important that the
consequences of changing a language are worked out in details.
It is time for me to go to school :-)
bye
Iavor