[Haskell-cafe] matrix computations based on the GSL

[Frederik Eaton]

Hi,

I've just looked through this discussion, since I'm working on my own
library, I wanted to see what people are doing.

It's something like this, using the Prepose (Implicit Configurations)
paper:

data L n = L Int deriving (Show, Eq, Ord)

-- singleton domain
type S = L Zero

class (Bounded a, Ix a) => IxB a

instance ReflectNum n => Bounded (L n) where
    minBound = L 0
    maxBound = L $ reflectNum (__ :: n) - 1

mul :: (Num k, IxB a, IxB b, IxB c) => Matrix k a b -> Matrix k b c -> Matrix k a c
add :: (Num k, IxB a, IxB b) => Matrix k a b -> Matrix k a b -> Matrix k a b
vec :: (Num k, IxB a, IxB b) => Matrix k a b -> Matrix k (a,b) S

This way one can form a type "L n" which represents integers between 0
inclusive and n (rather, 'reflectNum (__ :: n)') exclusive, which can
serve to index the matrices and vectors... Of course, other index
types are allowed, such as "Either a b" - if we want to, say, take the
sum of two vector spaces, one indexed by "a" and the other by "b",
then the result should be indexed by "Either a b", etc. - we never
have to do anything with the type-level numerals other than assert
equality, i.e. we don't have to be able to add or multiply them in our
type-signatures, since structural operations will suffice.

I think having the ability to guarantee through the type system that
column and row dimensions are correct is of paramount importance to
those who would use a matrix library, but so far in this thread I
haven't seen any suggestions which would accomplish that. I'm sorry if
I didn't read carefully. Does my approach not work? I haven't filled
in the implementation yet, but it type-checks.

Frederik