Re: [Haskell-cafe] Vectors, vector spaces and type-level Haskell

On Mon, Oct 4, 2021 at 6:45 PM Branimir Maksimovic wrote:

On 04.10.2021., at 09:38, Stuart Hungerford wrote:

On Mon, 4 Oct 2021 at 4:25 pm, Branimir Maksimovic wrote:

...

2d vector space is generated by two base vectors, if, which are orthogonal, that is normalised. They generate any other vector in that space.

Yes, so I would be looking to somehow tie the 2 basis vectors back to a 2D vector space. Or indeed n basis vectors to an n-vector space.

Space is generated by base vectors, think in that way… With vector addition and scalar multiplication you get third vector. so dimension is number of different directions of base vectors. So, easy...

Thanks Branimir I appreciate you taking the time to reply to what could be a silly question. Perhaps I haven't explained what I'm looking for very well. I know about the vector and scalar operations the vector space inherits from the underlying abelian group and field of scalars. Including the basis of linearly independent vectors that generates all vectors in the space. What I'd like to do is use the Haskell type system to encode those operations so I can't--for example--use a two dimensional and three dimensional vector in the same operation, or "ask" a vector what its "ambient" vector space is and have those operations checked at compile time. I've avoided learning about type-level programming in Haskell so far, but it may be time to delve deeper... Thanks again, Stu