[Haskell] Typing in haskell and mathematics

[Bjorn Lisper]

Jacques Carette:
....
>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.

I would like to remark that some array languages are doing this kind of
overloading (e.g., A + B means elementwise addition of A and B, when A and B
are arrays). If arrays are seen as functions from finite index domains, then
this is just a special case of your "math" overloading. Examples of such
languages are Fortran 90, HPF, and (the specified, but never implemented)
functional language Sisal 2.0.

All these languages are first-order, explicitly typed, and provide this
overloading only for a predefined set of builtin primitives. However, I
think this can be extended to functions in general, in higher-order
languages with Hindley-Milner (HM) type inference. I had a PhD student
working on this a couple of years ago. Alas, he dropped out before getting
his PhD, but we got as far as defining an extended inference system with
some nice properties, and I do believe that a reasonable inference algorithm
can be found. Rather than using subtyping, this system uses
"transformational" judgements of the form A |- e -> e':t, where e':t is
inferrable in the original HM type system. Thus, this system resolves the
overloading during type inference. For instance, with a proper assumption
set A, we would have A |- sin + cos -> (\x -> sin x + cos x).

Now, whether you would want to have this overloading unleashed in a higher
order language is another matter. I think it can be useful in some contexts,
but probably restricted in some way. Also, in Haskell there would be
potential conflicts with the overloading provided by the class system (Num
being a prime example).

Björn Lisper