On Thu, 7 Jul 2005, Conal Elliott wrote:
Maybe we could solve this problem in a simple and general way by working with a more abstract notion of linear maps, rather than the matrices commonly used to represent linear maps. Instead of "Matrix n m", where n and m are either integers (requiring something like dependent types) or type encodings of integers, use "LMap u v", where u and v are vector spaces, e.g., R^n and R^m. This change would eliminate the need for dependent types or integer encodings.
I would also dislike integer encodings in the matrix type because it is very sensible to have other types of indices. I would just do it how it is solved for Arrays: Two index types for a matrix but the actual matrix size is not coded in the type. E.g. I would like to multiply a matrix of type Matrix (Bool, Char) Double with a vector of type Vector Char Double obtaining a result of type Vector Bool Double.
Also, it's clear that "LMap R R^n" and "LMap R^n R" are different types (for n/=1), so we can distinguish between "row" and "column" vectors without creating more types. Are there other reasons for orienting vectors?
My point was that vectors naturally do _not_ represent linear maps at all, but they are the objects linear maps act on. If I process an audio signal or an image I can consider it well as vector but why should I consider it as linear map?
I can't call these comments a concrete proposal, as it's not clear to me how to define LMap and what operations it supports.
The problem will be that there is no canonical representation for linear maps in general vector spaces. I consider a function of type (Double -> Double) as an approximation to a real function but we don't have a general representation for linear operators on real functions. The remaining problem is that Vector and Linear Map are relative terms. That is, as you point out, a Linear Map can be a Vector with respect to a higher order Linear Map. I think in contrast to real mathematics we have to distinct due to computational restrictions. On the one hand we can work with a vector space type class which only specifies what basic operations (namely add and scale) shall be supported by types that want to be called vectors. This type class has the full flexibility but no canonical representation for linear maps. On the other hand we define finite dimensional vectors (array like) and matrices as representations for linear maps. For the case of higher order linear maps there should be a conversion between Matrix and Vector.