Henning Thielemann wrote:
I'm also aware of that I mean different objects when I write uniformly '1'. But I know that they are somehow different.
Since '1' can safely be used to denote the unit of any monoid, it does indeed have a lot of applications. And of course the syntactic artifact should not be confused with its denotation.
I'm also ok with not writing a conversion from say the integer 1 to the fraction 1/1, but I know that there had to be one. We should be aware of such abbreviations before adding them to a programming language.
But there is a difference here that is worth exploring. There is a canonical embedding of Z into Q. This embedding preserves the properties of Z as much as possible. It is even possible to directly ``see'' Z in Q. There is also an embedding of the representable integers into the floating point domain - but it does not have nice properties. It most definitely does not allow one to see the integers in amongst the floats (you just have to consider any representable integer with more significant bits than your float representation to see that). It seems safe to ignore canonical embeddings that preserve properties, but not the others.
But the multiplication in A*x already needs multi-parameter type classes. :-)
The matrix A already needs dependent types :-) Even simpler things do - see the work on Automath done in the late 60s.
Note that the one giant try at a statically typed mathematics system (Axiom w/ programming language Aldor) never caught on,
You mean I should have a closer look on it?
By all means! Axiom (http://page.axiom-developer.org/zope/mathaction/FrontPage) and Aldor (http://www.aldor.org) are extremely elegant, and contain many interesting ideas that are still ahead of other so-called ``research'' languages. They can both slice and dice through algebraic problems like few other systems can, at least on the elegance front. Magma (http://magma.maths.usyd.edu.au/magma/) comes close, with the added advantage that it is *fast*. Of course, don't try to symbolically solve a differential equation, do a Laplace transform, compute a closed form for a definite sum or a definite integral in any of those systems -- those facilities don't even exist. But that might have something to do with the problem that ``symbolic'' mathematics (especially in analysis) works on intensional representations directly, while most type theories are purely extensional. But see Oleg's message http://www.mail-archive.com/haskell@haskell.org/msg15686.html to see how Haskell can support intensional representations (indirectly). It is worth comparing that solution with similar functionality in Scheme to see the distance that still needs to be covered. Jacques