Types from values using existential types?
Sun, 11 Feb 2001 00:34:26 +0100 (MET)
>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.