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

[Michael Manti]

I recognize that I'm far out of my depth here--both in Haskell and in mathematics--but I'll ask anyway. In what ways are dependent types (http://haskell.org/hawiki/FunDeps, http://www.cse.ogi.edu/~mpj/pubs/fundeps.html) insufficient to address these issues? 
 
On Friday, August 27, 2004, at 10:04AM, Jacques Carette <carette at mcmaster.ca> wrote:

>> 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
>
>_______________________________________________
>Haskell mailing list
>Haskell at haskell.org
>http://www.haskell.org/mailman/listinfo/haskell
>
>


Michael Manti
mmanti at mac.com