Types from values using existential types?

[Bjorn Lisper]

>I recently had an idea to allow one to create types from values.  This
>would have many uses in Haskell; e.g., it would be very nice to have a
>type of nxn matrices for n that are not necessarily statically
>determined.  (It is easy to create a type of matrices and check that
>the sizes are compatible at run time; the point is to do more checks
>at compile time.)  Of course, one has to be careful to preserve
>decidability of type checking.
.....
>Are there any pointers to previous work I should look at?

If type systems for matrices are of interest for you then I think you should
check out Barray Jay's work on the language FiSH.

Björn Lisper