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

Dear Stuart, The V2 and V3 etc. types provided by the linear package (which you already found) model vectors in 2- and 3-dimensional real vector spaces, over the field given by their 'a' type parameter. Wanting to add a vector from a 2-dimensional vector space over 'a' and a vector from a 3-dimensional vector space over 'b' entails adding a 'V2 a' and 'V3 b'; those are distinct types. The vector space of 'V2 a' is morally 'a^2'. It seems this satisfies what you want. Are there other guarantees you want enforced at compile time that this cannot give you? - Tom On 04/10/2021 09:55, Stuart Hungerford wrote:

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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.