[Haskell] Dependent types, was:2-D Plots, graphical representation of massive data

[Jacques Carette]

> I think Jacques possibly means the ability to do static checking of matrix
> and vector extents, to make sure that you don't try to perform operations
> like matrix-vector multiply on operands whose extents do not match. If you
> want to have this ability on your language, then you will have to restrict
> the way you are allowed to construct array bounds so the equations that
> arise can be solved. Possibly a dependent type system can be helpful for
> this.

This is indeed what I meant.

If one is going to move from a dynamically typed language (like Matlab,
Maple, Mathematica, etc) to something statically typed, then the expectation
is that this is going to truly help.  And, for many applications, it does
[this is partly why I have an MSc student coding a reverse engineering
application in Haskell].

Since the claim of static typing is that things cannot go wrong at run-time,
one start to think (incorrectly, but optimistically) that this means that
'nonsense' cannot happen at run-time.  And multiplying matricies with
non-matching sizes is nonsense, so it is rather disappointing that, without
tricks, this is not caught at compilation time.

Matrix length are one of many commonly occuring dependent types in
mathematics.  Variable names for polynomials, expansion point and 'scale'
for generalized series expansions, coefficient ring for normalization and
factorization of polynomials, and so on up the food chain.  The dependencies
get quite interesting when one is dealing with modelling mixed PDEs and
recurrence equations as ideals in rings of Ore polynomials!  

Jacques