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

[Tom Smeding]

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
> <branimir.maksimovic at gmail.com> wrote:
>
>> On 04.10.2021., at 09:38, Stuart Hungerford <stuart.hungerford at gmail.com> wrote:
>>
>> On Mon, 4 Oct 2021 at 4:25 pm, Branimir Maksimovic <branimir.maksimovic at gmail.com> 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.
>