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

[Stuart Hungerford]

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